src/HOL/MicroJava/BV/Product.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14265 95b42e69436c
child 15613 ab90e95ae02e
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:      HOL/MicroJava/BV/Product.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   2000 TUM
     5 
     6 Products as semilattices
     7 *)
     8 
     9 header {* \isaheader{Products as Semilattices} *}
    10 
    11 theory Product = Err:
    12 
    13 constdefs
    14  le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
    15 "le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
    16 
    17  sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop"
    18 "sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
    19 
    20  esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
    21 "esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
    22 
    23 syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
    24        ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
    25 translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
    26 
    27 lemma unfold_lesub_prod:
    28   "p <=(rA,rB) q == le rA rB p q"
    29   by (simp add: lesub_def)
    30 
    31 lemma le_prod_Pair_conv [iff]:
    32   "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"
    33   by (simp add: lesub_def le_def)
    34 
    35 lemma less_prod_Pair_conv:
    36   "((a1,b1) <_(Product.le rA rB) (a2,b2)) = 
    37   (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"
    38 apply (unfold lesssub_def)
    39 apply simp
    40 apply blast
    41 done
    42 
    43 lemma order_le_prod [iff]:
    44   "order(Product.le rA rB) = (order rA & order rB)"
    45 apply (unfold order_def)
    46 apply simp
    47 apply meson
    48 done 
    49 
    50 
    51 lemma acc_le_prodI [intro!]:
    52   "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
    53 apply (unfold acc_def)
    54 apply (rule wf_subset)
    55  apply (erule wf_lex_prod)
    56  apply assumption
    57 apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
    58 done
    59 
    60 
    61 lemma closed_lift2_sup:
    62   "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow> 
    63   closed (err(A<*>B)) (lift2(sup f g))";
    64 apply (unfold closed_def plussub_def lift2_def err_def sup_def)
    65 apply (simp split: err.split)
    66 apply blast
    67 done 
    68 
    69 lemma unfold_plussub_lift2:
    70   "e1 +_(lift2 f) e2 == lift2 f e1 e2"
    71   by (simp add: plussub_def)
    72 
    73 
    74 lemma plus_eq_Err_conv [simp]:
    75   "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk> 
    76   \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
    77 proof -
    78   have plus_le_conv2:
    79     "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
    80                  OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
    81     by (rule semilat.plus_le_conv [THEN iffD1])
    82   case rule_context
    83   thus ?thesis
    84   apply (rule_tac iffI)
    85    apply clarify
    86    apply (drule OK_le_err_OK [THEN iffD2])
    87    apply (drule OK_le_err_OK [THEN iffD2])
    88    apply (drule semilat.lub[of _ _ _ "OK x" _ "OK y"])
    89         apply assumption
    90        apply assumption
    91       apply simp
    92      apply simp
    93     apply simp
    94    apply simp
    95   apply (case_tac "x +_f y")
    96    apply assumption
    97   apply (rename_tac "z")
    98   apply (subgoal_tac "OK z: err A")
    99   apply (frule plus_le_conv2)
   100        apply assumption
   101       apply simp
   102       apply blast
   103      apply simp
   104     apply (blast dest: semilat.orderI order_refl)
   105    apply blast
   106   apply (erule subst)
   107   apply (unfold semilat_def err_def closed_def)
   108   apply simp
   109   done
   110 qed
   111 
   112 lemma err_semilat_Product_esl:
   113   "\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)"
   114 apply (unfold esl_def Err.sl_def)
   115 apply (simp (no_asm_simp) only: split_tupled_all)
   116 apply simp
   117 apply (simp (no_asm) only: semilat_Def)
   118 apply (simp (no_asm_simp) only: semilat.closedI closed_lift2_sup)
   119 apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
   120 apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
   121             simp add: lift2_def  split: err.split)
   122 apply (blast dest: semilat.orderI)
   123 apply (blast dest: semilat.orderI)
   124 
   125 apply (rule OK_le_err_OK [THEN iffD1])
   126 apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
   127 apply simp
   128 apply simp
   129 apply simp
   130 apply simp
   131 apply simp
   132 apply simp
   133 
   134 apply (rule OK_le_err_OK [THEN iffD1])
   135 apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat.lub)
   136 apply simp
   137 apply simp
   138 apply simp
   139 apply simp
   140 apply simp
   141 apply simp
   142 done 
   143 
   144 end