src/HOL/Bali/TypeSafe.thy
changeset 13384 a34e38154413
parent 13337 f75dfc606ac7
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Jul 16 18:52:26 2002 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Jul 16 20:25:21 2002 +0200
     1.3 @@ -854,6 +854,10 @@
     1.4  
     1.5  subsection "accessibility"
     1.6  
     1.7 +text {* 
     1.8 +\par
     1.9 +*} (* dummy text command to break paragraph for latex;
    1.10 +              large paragraphs exhaust memory of debian pdflatex *)
    1.11  
    1.12  (* #### stat raus und gleich is_static f schreiben *) 
    1.13  theorem dynamic_field_access_ok:
    1.14 @@ -1707,7 +1711,9 @@
    1.15    next
    1.16      case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
    1.17      have hyp_e1: "PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)" .
    1.18 -    have hyp_e2: "PROP ?TypeSafe       s1  s2 (In1l e2) (In1 v2)" .
    1.19 +    have hyp_e2: "PROP ?TypeSafe       s1  s2 
    1.20 +                   (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
    1.21 +                   (In1 v2)" .
    1.22      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
    1.23      have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T" .
    1.24      then obtain e1T e2T where
    1.25 @@ -1716,20 +1722,22 @@
    1.26        wt_binop: "wt_binop G binop e1T e2T" and
    1.27               T: "T=Inl (PrimT (binop_type binop))"
    1.28        by (auto elim!: wt_elim_cases)
    1.29 +    have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
    1.30 +      by simp
    1.31      from conf_s0 wt_e1 
    1.32      obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
    1.33                    wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
    1.34            error_free_s1: "error_free s1"
    1.35        by (auto dest!: hyp_e1)
    1.36 -    from conf_s1 wt_e2 error_free_s1
    1.37 +    from conf_s1 wt_e2 wt_Skip error_free_s1
    1.38      obtain      conf_s2: "s2\<Colon>\<preceq>(G, L)"  and
    1.39 -                  wt_v2: "normal s2 \<longrightarrow> G,store s2\<turnstile>v2\<Colon>\<preceq>e2T" and
    1.40            error_free_s2: "error_free s2"
    1.41 -      by (auto dest!: hyp_e2)
    1.42 -    from wt_v1 wt_v2 wt_binop T
    1.43 +      by (cases "need_second_arg binop v1")
    1.44 +         (auto dest!: hyp_e2 )
    1.45 +    from wt_binop T
    1.46      have "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
    1.47        by (cases binop) auto
    1.48 -    with conf_s2 error_free_s2
    1.49 +    with conf_s2 conf_s1 error_free_s2 error_free_s1
    1.50      show "s2\<Colon>\<preceq>(G, L) \<and>
    1.51            (normal s2 \<longrightarrow>
    1.52          G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
    1.53 @@ -2364,6 +2372,12 @@
    1.54    qed
    1.55    then show ?thesis .
    1.56  qed
    1.57 +
    1.58 +text {* 
    1.59 +
    1.60 +
    1.61 +*} (* dummy text command to break paragraph for latex;
    1.62 +              large paragraphs exhaust memory of debian pdflatex *)
    1.63   
    1.64  corollary eval_ts: 
    1.65   "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T\<rbrakk> 
    1.66 @@ -2395,4 +2409,22 @@
    1.67  apply (drule (3) eval_type_sound)
    1.68  apply clarsimp
    1.69  done
    1.70 +
    1.71 +lemma wf_eval_Fin: 
    1.72 +  assumes wf:    "wf_prog G" and
    1.73 +          wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)" and
    1.74 +        conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" and
    1.75 +        eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" and
    1.76 +        eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" and
    1.77 +            s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
    1.78 +  shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
    1.79 +proof -
    1.80 +  from eval_c1 wt_c1 wf conf_s0
    1.81 +  have "error_free (x1,s1)"
    1.82 +    by (auto dest: eval_type_sound)
    1.83 +  with eval_c1 eval_c2 s3
    1.84 +  show ?thesis
    1.85 +    by - (rule eval.Fin, auto simp add: error_free_def)
    1.86 +qed
    1.87 +
    1.88  end