src/HOL/Bali/Evaln.thy
changeset 28524 644b62cf678f
parent 27226 5a3e5e46d977
child 32960 69916a850301
     1.1 --- a/src/HOL/Bali/Evaln.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  
     1.5  --{* propagation of abrupt completion *}
     1.6  
     1.7 -| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
     1.8 +| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
     1.9  
    1.10  
    1.11  --{* evaluation of variables *}
    1.12 @@ -346,13 +346,13 @@
    1.13  qed
    1.14  
    1.15  lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
    1.16 - fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
    1.17 + fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
    1.18  apply (erule evaln_cases , auto)
    1.19  done
    1.20  
    1.21  lemma evaln_abrupt: 
    1.22   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
    1.23 -  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
    1.24 +  w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))"
    1.25  apply auto
    1.26  apply (frule evaln_abrupt_lemma, auto)+
    1.27  done
    1.28 @@ -365,13 +365,13 @@
    1.29      | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
    1.30  *}
    1.31  
    1.32 -lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
    1.33 +lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
    1.34  apply (case_tac "s", case_tac "a = None")
    1.35  by (auto intro!: evaln.Lit)
    1.36  
    1.37  lemma CondI: 
    1.38   "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
    1.39 -  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
    1.40 +  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2"
    1.41  apply (case_tac "s", case_tac "a = None")
    1.42  by (auto intro!: evaln.Cond)
    1.43  
    1.44 @@ -520,7 +520,7 @@
    1.45  proof (induct)
    1.46    case (Abrupt xc s t)
    1.47    obtain n where
    1.48 -    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
    1.49 +    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
    1.50      by (iprover intro: evaln.Abrupt)
    1.51    then show ?case ..
    1.52  next