# Theory Jinja.Product

```(*  Title:      HOL/MicroJava/BV/Product.thy
Author:     Tobias Nipkow

Products as semilattices.
*)

section ‹Products as Semilattices›

theory Product
imports Err
begin

definition le :: "'a ord ⇒ 'b ord ⇒ ('a × 'b) ord"
where
"le r⇩A r⇩B = (λ(a⇩1,b⇩1) (a⇩2,b⇩2). a⇩1 ⊑⇘r⇩A⇙ a⇩2 ∧ b⇩1 ⊑⇘r⇩B⇙ b⇩2)"

definition sup :: "'a ebinop ⇒ 'b ebinop ⇒ ('a × 'b) ebinop"
where
"sup f g = (λ(a⇩1,b⇩1)(a⇩2,b⇩2). Err.sup Pair (a⇩1 ⊔⇩f a⇩2) (b⇩1 ⊔⇩g b⇩2))"

definition esl :: "'a esl ⇒ 'b esl ⇒ ('a × 'b ) esl"
where
"esl = (λ(A,r⇩A,f⇩A) (B,r⇩B,f⇩B). (A × B, le r⇩A r⇩B, sup f⇩A f⇩B))"

abbreviation
lesubprod :: "'a × 'b ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('b ⇒ 'b ⇒ bool) ⇒ 'a × 'b ⇒ bool"
("(_ /⊑'(_,_') _)" [50, 0, 0, 51] 50) where
"p ⊑(rA,rB) q == p ⊑⇘Product.le rA rB⇙ q"

(*<*)
notation
lesubprod  ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
(*>*)

lemma unfold_lesub_prod: "x ⊑(r⇩A,r⇩B) y = le r⇩A r⇩B x y"
(*<*) by (simp add: lesub_def) (*>*)

lemma le_prod_Pair_conv [iff]: "((a⇩1,b⇩1) ⊑(r⇩A,r⇩B) (a⇩2,b⇩2)) = (a⇩1 ⊑⇘r⇩A⇙ a⇩2 & b⇩1 ⊑⇘r⇩B⇙ b⇩2)"
(*<*) by (simp add: lesub_def le_def) (*>*)

lemma less_prod_Pair_conv:
"((a⇩1,b⇩1) ⊏⇘Product.le r⇩A r⇩B⇙ (a⇩2,b⇩2)) =
(a⇩1 ⊏⇘r⇩A⇙ a⇩2 & b⇩1 ⊑⇘r⇩B⇙ b⇩2 | a⇩1 ⊑⇘r⇩A⇙ a⇩2 & b⇩1 ⊏⇘r⇩B⇙ b⇩2)"
(*<*)
apply (unfold lesssub_def)
apply simp
apply blast
done
(*>*)

lemma order_le_prodI [iff]: "(order r⇩A  A & order r⇩B B) ⟹ order (Product.le r⇩A r⇩B) (A × B)"
apply (unfold order_def)
apply safe
apply blast+
done

lemma order_le_prodE: "A ≠ {} ⟹ B ≠ {} ⟹ order (Product.le r⇩A r⇩B) (A × B) ⟹ (order r⇩A  A & order r⇩B B)"
apply (unfold order_def)
apply simp
apply safe
apply blast+
done

lemma order_le_prod [iff]: "A ≠ {} ⟹ B ≠ {} ⟹ order(Product.le r⇩A r⇩B) (A × B) = (order r⇩A A & order r⇩B B)"
(*<*)
apply (unfold order_def)
apply simp
apply safe
apply blast+
done

(*>*)

lemma acc_le_prodI [intro!]:
"⟦ acc r⇩A; acc r⇩B ⟧ ⟹ acc(Product.le r⇩A r⇩B)"
(*<*)
apply (unfold acc_def)
apply (rule wf_subset)
apply (erule wf_lex_prod)
apply assumption
apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
done
(*>*)

lemma closed_lift2_sup:
"⟦ closed (err A) (lift2 f); closed (err B) (lift2 g) ⟧ ⟹
closed (err(A×B)) (lift2(sup f g))"
(*<*)
apply (unfold closed_def plussub_def lift2_def err_def' sup_def)
apply (simp split: err.split)
apply blast
done
(*>*)

lemma unfold_plussub_lift2: "e⇩1 ⊔⇘lift2 f⇙ e⇩2 = lift2 f e⇩1 e⇩2"
(*<*) by (simp add: plussub_def) (*>*)

lemma plus_eq_Err_conv [simp]:
assumes "x∈A"  "y∈A"  "semilat(err A, Err.le r, lift2 f)"
shows "(x ⊔⇩f y = Err) = (¬(∃z∈A. x ⊑⇩r z ∧ y ⊑⇩r z))"
(*<*)
proof -
have plus_le_conv2:
"⋀r f z. ⟦ z ∈ err A; semilat (err A, r, f); OK x ∈ err A; OK y ∈ err A;
OK x ⊔⇩f OK y ⊑⇩r z⟧ ⟹ OK x ⊑⇩r z ∧ OK y ⊑⇩r z"
(*<*) by (rule Semilat.plus_le_conv [OF Semilat.intro, THEN iffD1]) (*>*)
from assms show ?thesis
apply (rule_tac iffI)
apply clarify
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule OK_le_err_OK [THEN iffD2])
apply (drule Semilat.lub[OF Semilat.intro, of _ _ _ "OK x" _ "OK y"])
apply assumption
apply assumption
apply simp
apply simp
apply simp
apply simp
apply (case_tac "x ⊔⇩f y")
apply assumption
apply (rename_tac "z")
apply (subgoal_tac "OK z: err A")
apply (frule plus_le_conv2)
apply assumption
apply simp
apply blast
apply simp
apply (blast dest: Semilat.orderI [OF Semilat.intro] order_refl)
apply blast
apply (erule subst)
apply (unfold semilat_def err_def' closed_def)
apply simp
done
qed
(*>*)

lemma err_semilat_Product_esl:
"⋀L⇩1 L⇩2. ⟦ err_semilat L⇩1; err_semilat L⇩2 ⟧ ⟹ err_semilat(Product.esl L⇩1 L⇩2)"
(*<*)
apply (unfold esl_def Err.sl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp
apply (simp (no_asm) only: semilat_Def)
apply (simp (no_asm_simp) only: Semilat.closedI [OF Semilat.intro] closed_lift2_sup)
apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
apply(rule order_le_prodI)
apply (rule conjI)
apply (blast dest: Semilat.orderI [OF Semilat.intro])
apply (blast dest: Semilat.orderI [OF Semilat.intro])

apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp

apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst, subst OK_lift2_OK [symmetric], rule Semilat.lub [OF Semilat.intro])
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
done
(*>*)

end
```