src/HOL/Bali/Example.thy
changeset 13688 a0b16d42d489
parent 13524 604d0f3622d6
child 14030 cd928c0ac225
     1.1 --- a/src/HOL/Bali/Example.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -160,7 +160,8 @@
     1.4                \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
     1.5  	       mbody=\<lparr>lcls=[]
     1.6                       ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
     1.7 -       	                                                     Lit (Intg 1))\<rparr>
     1.8 +       	                                                     Lit (Intg 1)) ;;
     1.9 +                                Return (Lit Null)\<rparr>
    1.10  	      \<rparr>)"
    1.11  
    1.12  constdefs
    1.13 @@ -883,17 +884,44 @@
    1.14  
    1.15  declare member_is_static_simp [simp]
    1.16  declare wt.Skip [rule del] wt.Init [rule del]
    1.17 +ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
    1.18 +lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    1.19 +lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros
    1.20 +
    1.21  lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
    1.22  lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
    1.23 -ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
    1.24 -lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
    1.25 +
    1.26 +
    1.27 +
    1.28  
    1.29  lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
    1.30  apply (unfold Base_foo_defs )
    1.31 -apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
    1.32 +apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
    1.33              simp add: mhead_resTy_simp)
    1.34 +(* for definite assignment *)
    1.35 +apply (rule exI)
    1.36 +apply (simp add: parameters_def)
    1.37 +apply (rule conjI)
    1.38 +apply  (rule da.Comp)
    1.39 +apply     (rule da.Expr)
    1.40 +apply     (rule da.AssLVar)
    1.41 +apply       (rule da.AccLVar)
    1.42 +apply         (simp)
    1.43 +apply        (rule assigned.select_convs)
    1.44 +apply       (simp)
    1.45 +apply      (rule assigned.select_convs)
    1.46 +apply     (simp)
    1.47 +apply    (simp)
    1.48 +apply    (rule da.Jmp)
    1.49 +apply      (simp)
    1.50 +apply     (rule assigned.select_convs)
    1.51 +apply    (simp)
    1.52 +apply   (rule assigned.select_convs)
    1.53 +apply  (simp)
    1.54 +apply (simp)
    1.55  done
    1.56  
    1.57 +
    1.58  lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
    1.59  apply (unfold Ext_foo_defs )
    1.60  apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
    1.61 @@ -903,6 +931,37 @@
    1.62  apply    simp
    1.63  apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
    1.64  apply   (auto intro!: wtIs)
    1.65 +(* for definite assignment *)
    1.66 +apply (rule exI)
    1.67 +apply (simp add: parameters_def)
    1.68 +apply (rule conjI)
    1.69 +apply  (rule da.Comp)
    1.70 +apply     (rule da.Expr)
    1.71 +apply     (rule da.Ass)   
    1.72 +apply       simp
    1.73 +apply      (rule da.FVar)
    1.74 +apply      (rule da.Cast)
    1.75 +apply      (rule da.AccLVar)
    1.76 +apply        simp
    1.77 +apply       (rule assigned.select_convs)
    1.78 +apply      simp
    1.79 +apply     (rule da_Lit)
    1.80 +apply     (simp)
    1.81 +apply    (rule da.Comp)
    1.82 +apply       (rule da.Expr)
    1.83 +apply       (rule da.AssLVar)
    1.84 +apply         (rule da.Lit)                  
    1.85 +apply        (rule assigned.select_convs)
    1.86 +apply       simp
    1.87 +apply      (rule da.Jmp)
    1.88 +apply        simp
    1.89 +apply       (rule assigned.select_convs)
    1.90 +apply      simp
    1.91 +apply     (rule assigned.select_convs)
    1.92 +apply    (simp)
    1.93 +apply   (rule assigned.select_convs)
    1.94 +apply  simp
    1.95 +apply simp
    1.96  done
    1.97  
    1.98  declare mhead_resTy_simp [simp add]
    1.99 @@ -911,23 +970,35 @@
   1.100  lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
   1.101  apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
   1.102  apply (auto intro!: wf_Base_foo)
   1.103 -apply       (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
   1.104 -apply (auto intro!: wtIs)
   1.105 +apply        (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
   1.106 +apply   (auto intro!: wtIs)
   1.107 +(* for definite assignment *)
   1.108 +apply   (rule exI)
   1.109 +apply   (rule da.Expr)
   1.110 +apply  (rule da.Ass)
   1.111 +apply    (simp)
   1.112 +apply   (rule da.FVar)
   1.113 +apply   (rule da.Cast)
   1.114 +apply   (rule da_Lit)
   1.115 +apply   simp
   1.116 +apply  (rule da.NewA)
   1.117 +apply  (rule da.Lit)
   1.118  apply (auto simp add: Base_foo_defs entails_def Let_def)
   1.119  apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
   1.120 -apply   (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
   1.121 +apply (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
   1.122  done
   1.123  
   1.124  
   1.125  lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
   1.126  apply (unfold wf_cdecl_def ExtCl_def)
   1.127  apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
   1.128 -apply (auto simp add: entails_def snd_special_simp)
   1.129 -apply (insert Ext_foo_stat_override)
   1.130 -apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.131 -apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.132 -apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.133 -apply (insert Ext_foo_no_hide)
   1.134 +apply  (auto simp add: entails_def snd_special_simp)
   1.135 +apply      (insert Ext_foo_stat_override)
   1.136 +apply      (rule exI,rule da.Skip)      
   1.137 +apply     (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.138 +apply    (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.139 +apply   (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.140 +apply  (insert Ext_foo_no_hide)
   1.141  apply  (simp_all add: qmdecl_def)
   1.142  apply  blast+
   1.143  done
   1.144 @@ -935,6 +1006,7 @@
   1.145  lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
   1.146  apply (unfold wf_cdecl_def MainCl_def)
   1.147  apply (auto intro: ws_cdecl_Main)
   1.148 +apply (rule exI,rule da.Skip)
   1.149  done
   1.150  
   1.151  lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
   1.152 @@ -948,7 +1020,8 @@
   1.153  apply (unfold standard_classes_def Let_def 
   1.154         ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
   1.155  apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
   1.156 -apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
   1.157 +apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
   1.158 +            intro: da.Skip)
   1.159  apply (auto simp add: Object_def Classes_def standard_classes_def 
   1.160                        SXcptC_def SXcpt_def)
   1.161  done
   1.162 @@ -970,14 +1043,13 @@
   1.163  apply (rule conjI)
   1.164  apply (simp add: Object_mdecls_def)
   1.165  apply safe
   1.166 -apply  (cut_tac xn_cases_old)   (* FIXME (insert xn_cases) *)
   1.167 +apply  (cut_tac xn_cases)   
   1.168  apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
   1.169  apply  (insert wf_idecl_all)
   1.170  apply  (insert wf_cdecl_all)
   1.171  apply  auto
   1.172  done
   1.173  
   1.174 -
   1.175  section "max spec"
   1.176  
   1.177  lemma appl_methds_Base_foo: 
   1.178 @@ -998,7 +1070,6 @@
   1.179  apply auto
   1.180  done
   1.181  
   1.182 -
   1.183  section "well-typedness"
   1.184  
   1.185  lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
   1.186 @@ -1051,6 +1122,49 @@
   1.187  apply (rule wtIs (* Skip *))
   1.188  done
   1.189  
   1.190 +section "definite assignment"
   1.191 +
   1.192 +lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
   1.193 +                  \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
   1.194 +apply (unfold test_def arr_viewed_from_def)
   1.195 +apply (rule da.Comp)
   1.196 +apply    (rule da.Expr)
   1.197 +apply    (rule da.AssLVar)
   1.198 +apply      (rule da.NewC)
   1.199 +apply     (rule assigned.select_convs)
   1.200 +apply    (simp)
   1.201 +apply   (rule da.Try)
   1.202 +apply      (rule da.Expr)
   1.203 +apply      (rule da.Call)
   1.204 +apply       (rule da.AccLVar)
   1.205 +apply         (simp)   
   1.206 +apply        (rule assigned.select_convs)
   1.207 +apply       (simp)
   1.208 +apply      (rule da.Cons)
   1.209 +apply       (rule da.Lit)
   1.210 +apply      (rule da.Nil)
   1.211 +apply     (rule da.Loop)
   1.212 +apply        (rule da.Acc)
   1.213 +apply         (simp)
   1.214 +apply        (rule da.AVar)
   1.215 +apply         (rule da.Acc)
   1.216 +apply          simp
   1.217 +apply         (rule da.FVar)
   1.218 +apply         (rule da.Cast)
   1.219 +apply         (rule da.Lit)
   1.220 +apply        (rule da.Lit)
   1.221 +apply       (rule da_Skip)
   1.222 +apply       (simp)
   1.223 +apply      (simp,rule assigned.select_convs)
   1.224 +apply     (simp)
   1.225 +apply    (simp,rule assigned.select_convs)
   1.226 +apply   (simp)
   1.227 +apply  simp
   1.228 +apply  blast
   1.229 +apply simp
   1.230 +apply (simp add: intersect_ts_def)
   1.231 +done
   1.232 +
   1.233  
   1.234  section "execution"
   1.235  
   1.236 @@ -1212,7 +1326,7 @@
   1.237  apply   (simp)
   1.238  apply   (rule halloc.New)
   1.239  apply    (simp (no_asm_simp))
   1.240 -apply   (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
   1.241 +apply   (drule atleast_free_weaken,drule atleast_free_weaken)
   1.242  apply   (simp (no_asm_simp))
   1.243  apply  (simp add: upd_gobj_def)
   1.244        (* end init Ext *)
   1.245 @@ -1251,19 +1365,25 @@
   1.246  apply     (rule init_done, simp)
   1.247  apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
   1.248  apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
   1.249 -apply    (rule eval_Is (* Expr *))
   1.250 -apply    (rule eval_Is (* Ass *))
   1.251 -apply     (rule eval_Is (* FVar *))
   1.252 -apply       (rule init_done, simp)
   1.253 -apply      (rule eval_Is (* Cast *))
   1.254 -apply       (rule eval_Is (* Acc *))
   1.255 -apply       (rule eval_Is (* LVar *))
   1.256 -apply      (simp)
   1.257 -apply      (simp split del: split_if)
   1.258 +apply    (rule eval_Is (* Comp *))
   1.259 +apply     (rule eval_Is (* Expr *))
   1.260 +apply     (rule eval_Is (* Ass *))
   1.261 +apply      (rule eval_Is (* FVar *))
   1.262 +apply         (rule init_done, simp)
   1.263 +apply        (rule eval_Is (* Cast *))
   1.264 +apply         (rule eval_Is (* Acc *))
   1.265 +apply         (rule eval_Is (* LVar *))
   1.266 +apply        (simp)
   1.267 +apply       (simp split del: split_if)
   1.268  apply      (simp add: check_field_access_def Let_def)
   1.269 -apply    (rule eval_Is (* XcptE *))
   1.270 +apply     (rule eval_Is (* XcptE *))
   1.271 +apply    (simp)
   1.272 +apply    (rule conjI)
   1.273 +apply     (simp)
   1.274 +apply    (rule eval_Is (* Comp *))
   1.275  apply   (simp)
   1.276        (* end method call *)
   1.277 +apply  simp
   1.278  apply  (rule sxalloc.intros)
   1.279  apply  (rule halloc.New)
   1.280  apply   (erule alloc_one [THEN conjunct1])