tuned
authorkleing
Sun Jan 14 18:17:37 2001 +0100 (2001-01-14)
changeset 1089623386a5b63eb
parent 10895 79194f07d356
child 10897 697fab84709e
tuned
src/HOL/MicroJava/BV/JType.thy
     1.1 --- a/src/HOL/MicroJava/BV/JType.thy	Sun Jan 14 14:12:42 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/JType.thy	Sun Jan 14 18:17:37 2001 +0100
     1.3 @@ -160,22 +160,15 @@
     1.4    done
     1.5  
     1.6  
     1.7 -lemma err_semilat_JType_esl_lemma:
     1.8 -  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
     1.9 -  ==> err_semilat (esl G)"
    1.10 +lemma sup_subtype_greater:
    1.11 +  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
    1.12 +      is_type G t1; is_type G t2; sup G t1 t2 = OK s |] 
    1.13 +  ==> subtype G t1 s \<and> subtype G t2 s"
    1.14  proof -
    1.15 -  assume wf_prog:   "wf_prog wf_mb G"
    1.16 +  assume wf_prog:       "wf_prog wf_mb G"
    1.17    assume single_valued: "single_valued (subcls1 G)" 
    1.18 -  assume acyclic:   "acyclic (subcls1 G)"
    1.19 -  
    1.20 -  hence "order (subtype G)"
    1.21 -    by (rule order_widen)
    1.22 -  moreover
    1.23 -  from wf_prog single_valued acyclic
    1.24 -  have "closed (err (types G)) (lift2 (sup G))"
    1.25 -    by (rule closed_err_types)
    1.26 -  moreover
    1.27 -  
    1.28 +  assume acyclic:       "acyclic (subcls1 G)"
    1.29 + 
    1.30    { fix c1 c2
    1.31      assume is_class: "is_class G c1" "is_class G c2"
    1.32      with wf_prog 
    1.33 @@ -185,53 +178,31 @@
    1.34        by (blast intro: subcls_C_Object)
    1.35      with wf_prog single_valued
    1.36      obtain u where
    1.37 -      "is_lub ((subcls1 G)^* ) c1 c2 u"
    1.38 +      "is_lub ((subcls1 G)^* ) c1 c2 u"      
    1.39        by (blast dest: single_valued_has_lubs)
    1.40      with acyclic
    1.41 -    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
    1.42 +    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2 \<and>
    1.43 +          G \<turnstile> c2 \<preceq>C some_lub ((subcls1 G)^* ) c1 c2"
    1.44        by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
    1.45 -  } note this [intro]
    1.46 +  } note this [simp]
    1.47        
    1.48 -  { fix t1 t2 s
    1.49 -    assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"    
    1.50 -    hence "subtype G t1 s"
    1.51 -      by (unfold sup_def subtype_def) 
    1.52 -         (cases s, auto intro: widen.null 
    1.53 -                        split: ty.splits ref_ty.splits if_splits)
    1.54 -  } note this [intro]
    1.55 -  
    1.56 -  have
    1.57 -    "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y"
    1.58 -    by (auto simp add: lesub_def plussub_def le_def lift2_def split: err.split)
    1.59 -
    1.60 -  moreover
    1.61 +  assume "is_type G t1" "is_type G t2" "sup G t1 t2 = OK s"
    1.62 +  thus ?thesis
    1.63 +    apply (unfold sup_def subtype_def) 
    1.64 +    apply (cases s)
    1.65 +    apply (auto split: ty.split_asm ref_ty.split_asm split_if_asm)
    1.66 +    done
    1.67 +qed
    1.68  
    1.69 -  { fix c1 c2
    1.70 -    assume "is_class G c1" "is_class G c2"
    1.71 -    with wf_prog
    1.72 -    obtain 
    1.73 -      "G \<turnstile> c1 \<preceq>C Object"
    1.74 -      "G \<turnstile> c2 \<preceq>C Object"
    1.75 -      by (blast intro: subcls_C_Object)
    1.76 -    with wf_prog single_valued
    1.77 -    obtain u where
    1.78 -      "is_lub ((subcls1 G)^* ) c2 c1 u"
    1.79 -      by (blast dest: single_valued_has_lubs)
    1.80 -    with acyclic
    1.81 -    have "G \<turnstile> c1 \<preceq>C some_lub ((subcls1 G)^* ) c2 c1"
    1.82 -      by (simp add: some_lub_conv) (blast dest: is_lubD is_ubD)
    1.83 -  } note this [intro]
    1.84 -      
    1.85 -  have "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). 
    1.86 -    y <=_(le (subtype G)) x +_(lift2 (sup G)) y"
    1.87 -    by (auto simp add: lesub_def plussub_def le_def sup_def subtype_def lift2_def 
    1.88 -             split: err.split ty.splits ref_ty.splits if_splits intro: widen.null)
    1.89 -  moreover
    1.90 -    
    1.91 -  have [intro]: 
    1.92 -    "!!a b c. [| G \<turnstile> a \<preceq> c; G \<turnstile> b \<preceq> c; sup G a b = Err |] ==> False"
    1.93 -    by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def 
    1.94 -             split: ty.splits ref_ty.splits)
    1.95 +lemma sup_subtype_smallest:
    1.96 +  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G);
    1.97 +      is_type G a; is_type G b; is_type G c; 
    1.98 +      subtype G a c; subtype G b c; sup G a b = OK d |]
    1.99 +  ==> subtype G d c"
   1.100 +proof -
   1.101 +  assume wf_prog:       "wf_prog wf_mb G"
   1.102 +  assume single_valued: "single_valued (subcls1 G)" 
   1.103 +  assume acyclic:       "acyclic (subcls1 G)"
   1.104  
   1.105    { fix c1 c2 D
   1.106      assume is_class: "is_class G c1" "is_class G c2"
   1.107 @@ -261,18 +232,48 @@
   1.108      "!!C T. G \<turnstile> Class C \<preceq> T ==> \<exists>D. T=Class D \<and> G \<turnstile> C \<preceq>C D"
   1.109      by (frule widen_Class, auto)
   1.110  
   1.111 -  { fix a b c d
   1.112 -    assume "is_type G a" "is_type G b" "is_type G c" and
   1.113 -           "G \<turnstile> a \<preceq> c" "G \<turnstile> b \<preceq> c" and
   1.114 -           "sup G a b = OK d" 
   1.115 -    hence "G \<turnstile> d \<preceq> c"
   1.116 -      by (auto simp add: sup_def split: ty.splits ref_ty.splits if_splits)
   1.117 -  } note this [intro]
   1.118 +  assume "is_type G a" "is_type G b" "is_type G c"
   1.119 +         "subtype G a c" "subtype G b c" "sup G a b = OK d"
   1.120 +  thus ?thesis
   1.121 +    by (auto simp add: subtype_def sup_def 
   1.122 +             split: ty.split_asm ref_ty.split_asm split_if_asm)
   1.123 +qed
   1.124 +
   1.125 +lemma sup_exists:
   1.126 +  "[| subtype G a c; subtype G b c; sup G a b = Err |] ==> False"
   1.127 +  by (auto simp add: PrimT_PrimT PrimT_PrimT2 sup_def subtype_def
   1.128 +           split: ty.splits ref_ty.splits)
   1.129  
   1.130 +lemma err_semilat_JType_esl_lemma:
   1.131 +  "[| wf_prog wf_mb G; single_valued (subcls1 G); acyclic (subcls1 G) |] 
   1.132 +  ==> err_semilat (esl G)"
   1.133 +proof -
   1.134 +  assume wf_prog:   "wf_prog wf_mb G"
   1.135 +  assume single_valued: "single_valued (subcls1 G)" 
   1.136 +  assume acyclic:   "acyclic (subcls1 G)"
   1.137 +  
   1.138 +  hence "order (subtype G)"
   1.139 +    by (rule order_widen)
   1.140 +  moreover
   1.141 +  from wf_prog single_valued acyclic
   1.142 +  have "closed (err (types G)) (lift2 (sup G))"
   1.143 +    by (rule closed_err_types)
   1.144 +  moreover
   1.145 +
   1.146 +  from wf_prog single_valued acyclic 
   1.147 +  have
   1.148 +    "(\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). x <=_(le (subtype G)) x +_(lift2 (sup G)) y) \<and> 
   1.149 +     (\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). y <=_(le (subtype G)) x +_(lift2 (sup G)) y)"
   1.150 +    by (auto simp add: lesub_def plussub_def le_def lift2_def sup_subtype_greater split: err.split)
   1.151 +
   1.152 +  moreover    
   1.153 +
   1.154 +  from wf_prog single_valued acyclic 
   1.155    have
   1.156      "\<forall>x\<in>err (types G). \<forall>y\<in>err (types G). \<forall>z\<in>err (types G). 
   1.157      x <=_(le (subtype G)) z \<and> y <=_(le (subtype G)) z \<longrightarrow> x +_(lift2 (sup G)) y <=_(le (subtype G)) z"
   1.158 -    by (simp add: lift2_def plussub_def lesub_def subtype_def le_def split: err.splits) blast
   1.159 +    by (unfold lift2_def plussub_def lesub_def le_def)
   1.160 +       (auto intro: sup_subtype_smallest sup_exists split: err.split)
   1.161  
   1.162    ultimately
   1.163