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