header {* \isaheader{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 \<sqsubseteq>⇘r⇣A⇙ a⇣2 ∧ b⇣1 \<sqsubseteq>⇘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 \<squnion>⇩f a⇣2) (b⇣1 \<squnion>⇩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
lesubprod1 :: "'a × 'b => ('a => 'a => bool) => ('b => 'b => bool) => 'a × 'b => bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50) where
"p <=(rA,rB) q == p \<sqsubseteq>⇘Product.le rA rB⇙ q"
abbreviation (xsymbols)
lesubprod :: "'a × 'b => ('a => 'a => bool) => ('b => 'b => bool) => 'a × 'b => bool"
("(_ /\<sqsubseteq>'(_,_') _)" [50, 0, 0, 51] 50) where
"p \<sqsubseteq>(rA,rB) q == p \<sqsubseteq>⇘Product.le rA rB⇙ q"
lemma unfold_lesub_prod: "x \<sqsubseteq>(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) \<sqsubseteq>(r⇣A,r⇣B) (a⇣2,b⇣2)) = (a⇣1 \<sqsubseteq>⇘r⇣A⇙ a⇣2 & b⇣1 \<sqsubseteq>⇘r⇣B⇙ b⇣2)"
by (simp add: lesub_def le_def)
lemma less_prod_Pair_conv:
"((a⇣1,b⇣1) \<sqsubset>⇘Product.le r⇣A r⇣B⇙ (a⇣2,b⇣2)) =
(a⇣1 \<sqsubset>⇘r⇣A⇙ a⇣2 & b⇣1 \<sqsubseteq>⇘r⇣B⇙ b⇣2 | a⇣1 \<sqsubseteq>⇘r⇣A⇙ a⇣2 & b⇣1 \<sqsubset>⇘r⇣B⇙ b⇣2)"
apply (unfold lesssub_def)
apply simp
apply blast
done
lemma order_le_prod [iff]: "order(Product.le r⇣A r⇣B) = (order r⇣A & order r⇣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 \<squnion>⇘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 \<squnion>⇩f y = Err) = (¬(∃z∈A. x \<sqsubseteq>⇩r z ∧ y \<sqsubseteq>⇩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 \<squnion>⇩f OK y \<sqsubseteq>⇩r z|] ==> OK x \<sqsubseteq>⇩r z ∧ OK y \<sqsubseteq>⇩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 \<squnion>⇩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
simp add: lift2_def split: err.split)
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