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
```