Theory Product

(*  Title:      HOL/MicroJava/BV/Product.thy
    ID:         $Id: Product.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2000 TUM

Products as semilattices
*)

header {* \isaheader{Products as Semilattices} *}

theory Product = Err:
 
constdefs
  le :: "'a ord => 'b ord => ('a × 'b) ord"
  "le rA rB ≡ λ(a1,b1) (a2,b2). a1 \<sqsubseteq>rA a2 ∧ b1 \<sqsubseteq>rB b2"

  sup :: "'a ebinop => 'b ebinop => ('a × 'b) ebinop"
  "sup f g ≡ λ(a1,b1)(a2,b2). Err.sup Pair (a1 \<squnion>f a2) (b1 \<squnion>g b2)"

  esl :: "'a esl => 'b esl => ('a × 'b ) esl"
  "esl ≡ λ(A,rA,fA) (B,rB,fB). (A × B, le rA rB, sup fA fB)"

(*<*)
syntax
  "@lesubprod" :: "'a × 'b => 'a ord => 'b ord => 'b => bool" 
  ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
(*>*)

syntax (xsymbols)
  "@lesubprod" :: "'a × 'b => 'a ord => 'b ord => 'b => bool" 
  ("(_ /\<sqsubseteq>'(_,_') _)" [50, 0, 0, 51] 50)

translations "p \<sqsubseteq>(rA,rB) q" == "p \<sqsubseteq>Product.le rA rB q"

lemma unfold_lesub_prod: "x \<sqsubseteq>(rA,rB) y ≡ le rA rB x y"
(*<*) by (simp add: lesub_def) (*>*)

lemma le_prod_Pair_conv [iff]: "((a1,b1) \<sqsubseteq>(rA,rB) (a2,b2)) = (a1 \<sqsubseteq>rA a2 & b1 \<sqsubseteq>rB b2)"
(*<*) by (simp add: lesub_def le_def) (*>*)

lemma less_prod_Pair_conv:
  "((a1,b1) \<sqsubset>Product.le rA rB (a2,b2)) = 
  (a1 \<sqsubset>rA a2 & b1 \<sqsubseteq>rB b2 | a1 \<sqsubseteq>rA a2 & b1 \<sqsubset>rB b2)"
(*<*)
apply (unfold lesssub_def)
apply simp
apply blast
done
(*>*)

lemma order_le_prod [iff]: "order(Product.le rA rB) = (order rA & order rB)"
(*<*)
apply (unfold order_def)
apply simp
apply safe
apply blast+
done 
(*>*)


lemma acc_le_prodI [intro!]:
  "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
(*<*)
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: "e1 \<squnion>lift2 f e2 ≡ lift2 f e1 e2"
(*<*) by (simp add: plussub_def) (*>*)


lemma plus_eq_Err_conv [simp]:
  "[| x∈A; y∈A; semilat(err A, Err.le r, lift2 f) |] 
  ==> (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 [THEN iffD1]) (*>*)
  case rule_context
  thus ?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 _ _ _ "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 order_refl)
   apply blast
  apply (erule subst)
  apply (unfold semilat_def err_def' closed_def)
  apply simp
  done
qed
(*>*)

lemma err_semilat_Product_esl:
  "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
(*<*)
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 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)
apply (blast dest: semilat.orderI)

apply (rule OK_le_err_OK [THEN iffD1])
apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
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)
apply simp
apply simp
apply simp
apply simp
apply simp
apply simp
done 
(*>*)

end