(*  Title:      HOL/MicroJava/BV/Product.thy
    Author:     Tobias Nipkow
    Copyright   2000 TUM

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₁,b₁) (a₂,b₂). a₁ ⊑_A a₂ ∧ b₁ ⊑_B b₂)"

definition sup :: "'a ebinop → 'b ebinop → ('a × 'b) ebinop"
where
  "sup f g = (λ(a₁,b₁)(a₂,b₂). Err.sup Pair (a₁ ⊔_f a₂) (b₁ ⊔_g b₂))"

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 ⊑_{.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₁,b₁) ⊑(r_A,r_B) (a₂,b₂)) = (a₁ ⊑_A a₂ & b₁ ⊑_B b₂)"
(*<*) by (simp add: lesub_def le_def) (*>*)

lemma less_prod_Pair_conv:
  "((a₁,b₁) ⊏_{.le rA rB} (a₂,b₂)) =
  (a₁ ⊏_A a₂ & b₁ ⊑_B b₂ | a₁ ⊑_A a₂ & b₁ ⊏_B b₂)"
(*<*)
  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₁ ⊔ _f e₂ = lift2 f e₁ e₂"
(*<*) 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₁ L₂. [ err_semilat L₁; err_semilat L₂ ] ==> err_semilat(Product.esl L₁ L₂)"
(*<*)
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(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