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