# HG changeset patch # User haftmann # Date 1223388470 -7200 # Node ID 644b62cf678f06ce9ff415ac77ac44ea8d19af6f # Parent 5818d9cfb2e78a7c2b839ca57206281efe37db87 arbitrary is undefined diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Algebra/FiniteProduct.thy --- a/src/HOL/Algebra/FiniteProduct.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Algebra/FiniteProduct.thy Tue Oct 07 16:07:50 2008 +0200 @@ -291,7 +291,7 @@ finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" "finprod G f A == if finite A then foldD (carrier G) (mult G o f) \ A - else arbitrary" + else undefined" syntax "_finprod" :: "index => idt => 'a set => 'b => 'b" diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Algebra/IntRing.thy Tue Oct 07 16:07:50 2008 +0200 @@ -118,7 +118,7 @@ qed interpretation int: comm_monoid ["\"] - where "finprod \ f A = (if finite A then setprod f A else arbitrary)" + where "finprod \ f A = (if finite A then setprod f A else undefined)" proof - -- "Specification" show "comm_monoid \" by (unfold_locales) (auto simp: int_ring_def) @@ -128,7 +128,7 @@ { fix x y have "mult \ x y = x * y" by (simp add: int_ring_def) } note mult = this have one: "one \ = 1" by (simp add: int_ring_def) - show "finprod \ f A = (if finite A then setprod f A else arbitrary)" + show "finprod \ f A = (if finite A then setprod f A else undefined)" proof (cases "finite A") case True then show ?thesis proof induct case empty show ?case by (simp add: one) @@ -143,7 +143,7 @@ interpretation int: abelian_monoid ["\"] where "zero \ = 0" and "add \ x y = x + y" - and "finsum \ f A = (if finite A then setsum f A else arbitrary)" + and "finsum \ f A = (if finite A then setsum f A else undefined)" proof - -- "Specification" show "abelian_monoid \" by (unfold_locales) (auto simp: int_ring_def) @@ -153,7 +153,7 @@ { fix x y show "add \ x y = x + y" by (simp add: int_ring_def) } note add = this show zero: "zero \ = 0" by (simp add: int_ring_def) - show "finsum \ f A = (if finite A then setsum f A else arbitrary)" + show "finsum \ f A = (if finite A then setsum f A else undefined)" proof (cases "finite A") case True then show ?thesis proof induct case empty show ?case by (simp add: zero) diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/AxSem.thy Tue Oct 07 16:07:50 2008 +0200 @@ -501,7 +501,7 @@ | hazard:"G,A\{P \. Not \ type_ok G t} t\ {Q}" -| Abrupt: "G,A\{P\(arbitrary3 t) \. Not \ normal} t\ {P}" +| Abrupt: "G,A\{P\(undefined3 t) \. Not \ normal} t\ {P}" --{* variables *} | LVar: " G,A\{Normal (\s.. P\Var (lvar vn s))} LVar vn=\ {P}" diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/AxSound.thy --- a/src/HOL/Bali/AxSound.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/AxSound.thy Tue Oct 07 16:07:50 2008 +0200 @@ -433,15 +433,15 @@ by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast next case (Abrupt A P t) - show "G,A|\\{ {P\arbitrary3 t \. Not \ normal} t\ {P} }" + show "G,A|\\{ {P\undefined3 t \. Not \ normal} t\ {P} }" proof (rule validI) fix n s0 L accC T C v s1 Y Z assume conf_s0: "s0\\(G, L)" assume eval: "G\s0 \t\\n\ (v, s1)" - assume "(P\arbitrary3 t \. Not \ normal) Y s0 Z" - then obtain P: "P (arbitrary3 t) s0 Z" and abrupt_s0: "\ normal s0" + assume "(P\undefined3 t \. Not \ normal) Y s0 Z" + then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "\ normal s0" by simp - from eval abrupt_s0 obtain "s1=s0" and "v=arbitrary3 t" + from eval abrupt_s0 obtain "s1=s0" and "v=undefined3 t" by auto with P conf_s0 show "P v s1 Z \ s1\\(G, L)" @@ -2175,13 +2175,13 @@ note conf = `(Some abr, s)\\(G, L)` note P = `P Y' (Some abr, s) Z` note valid_A = `\t\A. G\n'\t` - show "(P'\=False\=\) (arbitrary3 t') (Some abr, s) Z" + show "(P'\=False\=\) (undefined3 t') (Some abr, s) Z" proof - have eval_e: - "G\(Some abr,s) \\e\\<^sub>e\\n'\ (arbitrary3 \e\\<^sub>e,(Some abr,s))" + "G\(Some abr,s) \\e\\<^sub>e\\n'\ (undefined3 \e\\<^sub>e,(Some abr,s))" by auto from valid_e P valid_A conf eval_e - have "P' (arbitrary3 \e\\<^sub>e) (Some abr,s) Z" + have "P' (undefined3 \e\\<^sub>e) (Some abr,s) Z" by (cases rule: validE [where ?P="P"]) simp+ with t' show ?thesis by auto diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/Decl.thy Tue Oct 07 16:07:50 2008 +0200 @@ -373,7 +373,7 @@ ObjectC_def:"ObjectC \ (Object,\access=Public,cfields=[],methods=Object_mdecls, - init=Skip,super=arbitrary,superIfs=[]\)" + init=Skip,super=undefined,superIfs=[]\)" SXcptC_def:"SXcptC xn\ (SXcpt xn,\access=Public,cfields=[],methods=SXcpt_mdecls, init=Skip, super=if xn = Throwable then Object @@ -761,11 +761,11 @@ recdef iface_rec "same_fst ws_prog (\G. (subint1 G)^-1)" "iface_rec (G,I) = (\f. case iface G I of - None \ arbitrary + None \ undefined | Some i \ if ws_prog G then f I i ((\J. iface_rec (G,J) f)`set (isuperIfs i)) - else arbitrary)" + else undefined)" (hints recdef_wf: wf_subint1 intro: subint1I) declare iface_rec.simps [simp del] @@ -779,12 +779,12 @@ recdef class_rec "same_fst ws_prog (\G. (subcls1 G)^-1)" "class_rec(G,C) = (\t f. case class G C of - None \ arbitrary + None \ undefined | Some c \ if ws_prog G then f C c (if C = Object then t else class_rec (G,super c) t f) - else arbitrary)" + else undefined)" (hints recdef_wf: wf_subcls1 intro: subcls1I) declare class_rec.simps [simp del] diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/Eval.thy Tue Oct 07 16:07:50 2008 +0200 @@ -58,7 +58,7 @@ \end{itemize} \item the rules are defined carefully in order to be applicable even in not type-correct situations (yielding undefined values), - e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}. + e.g. @{text "the_Addr (Val (Bool b)) = undefined"}. \begin{itemize} \item[++] fewer rules \item[-] less readable because of auxiliary functions like @{text the_Addr} @@ -141,21 +141,21 @@ "\es\\<^sub>l" \ "In3 es" constdefs - arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \ vals" - "arbitrary3 \ sum3_case (In1 \ sum_case (\x. arbitrary) (\x. Unit)) - (\x. In2 arbitrary) (\x. In3 arbitrary)" + undefined3 :: "('al + 'ar, 'b, 'c) sum3 \ vals" + "undefined3 \ sum3_case (In1 \ sum_case (\x. undefined) (\x. Unit)) + (\x. In2 undefined) (\x. In3 undefined)" -lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary" -by (simp add: arbitrary3_def) +lemma [simp]: "undefined3 (In1l x) = In1 undefined" +by (simp add: undefined3_def) -lemma [simp]: "arbitrary3 (In1r x) = \" -by (simp add: arbitrary3_def) +lemma [simp]: "undefined3 (In1r x) = \" +by (simp add: undefined3_def) -lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary" -by (simp add: arbitrary3_def) +lemma [simp]: "undefined3 (In2 x) = In2 undefined" +by (simp add: undefined3_def) -lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary" -by (simp add: arbitrary3_def) +lemma [simp]: "undefined3 (In3 x) = In3 undefined" +by (simp add: undefined3_def) section "exception throwing and catching" @@ -479,7 +479,7 @@ where --{* allocating objects on the heap, cf. 12.5 *} Abrupt: - "G\(Some x,s) \halloc oi\arbitrary\ (Some x,s)" + "G\(Some x,s) \halloc oi\undefined\ (Some x,s)" | New: "\new_Addr (heap s) = Some a; (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi) @@ -522,7 +522,7 @@ --{* cf. 14.1, 15.5 *} | Abrupt: - "G\(Some xc,s) \t\\ (arbitrary3 t, (Some xc, s))" + "G\(Some xc,s) \t\\ (undefined3 t, (Some xc, s))" --{* execution of statements *} @@ -971,13 +971,13 @@ lemma eval_abrupt_lemma: - "G\s \t\\ (v,s') \ abrupt s=Some xc \ s'= s \ v = arbitrary3 t" + "G\s \t\\ (v,s') \ abrupt s=Some xc \ s'= s \ v = undefined3 t" by (erule eval_cases, auto) lemma eval_abrupt: " G\(Some xc,s) \t\\ (w,s') = - (s'=(Some xc,s) \ w=arbitrary3 t \ - G\(Some xc,s) \t\\ (arbitrary3 t,(Some xc,s)))" + (s'=(Some xc,s) \ w=undefined3 t \ + G\(Some xc,s) \t\\ (undefined3 t,(Some xc,s)))" apply auto apply (frule eval_abrupt_lemma, auto)+ done @@ -989,7 +989,7 @@ | _ => SOME (mk_meta_eq @{thm eval_abrupt})) *} -lemma LitI: "G\s \Lit v-\(if normal s then v else arbitrary)\ s" +lemma LitI: "G\s \Lit v-\(if normal s then v else undefined)\ s" apply (case_tac "s", case_tac "a = None") by (auto intro!: eval.Lit) @@ -1007,7 +1007,7 @@ lemma CondI: "\s1. \G\s \e-\b\ s1; G\s1 \(if the_Bool b then e1 else e2)-\v\ s2\ \ - G\s \e ? e1 : e2-\(if normal s1 then v else arbitrary)\ s2" + G\s \e ? e1 : e2-\(if normal s1 then v else undefined)\ s2" apply (case_tac "s", case_tac "a = None") by (auto intro!: eval.Cond) @@ -1054,7 +1054,7 @@ done lemma eval_StatRef: -"G\s \StatRef rt-\(if abrupt s=None then Null else arbitrary)\ s" +"G\s \StatRef rt-\(if abrupt s=None then Null else undefined)\ s" apply (case_tac "s", simp) apply (case_tac "a = None") apply (auto del: eval.Abrupt intro!: eval.intros) diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/Evaln.thy Tue Oct 07 16:07:50 2008 +0200 @@ -49,7 +49,7 @@ --{* propagation of abrupt completion *} -| Abrupt: "G\(Some xc,s) \t\\n\ (arbitrary3 t,(Some xc,s))" +| Abrupt: "G\(Some xc,s) \t\\n\ (undefined3 t,(Some xc,s))" --{* evaluation of variables *} @@ -346,13 +346,13 @@ qed lemma evaln_abrupt_lemma: "G\s \e\\n\ (v,s') \ - fst s = Some xc \ s' = s \ v = arbitrary3 e" + fst s = Some xc \ s' = s \ v = undefined3 e" apply (erule evaln_cases , auto) done lemma evaln_abrupt: "\s'. G\(Some xc,s) \e\\n\ (w,s') = (s' = (Some xc,s) \ - w=arbitrary3 e \ G\(Some xc,s) \e\\n\ (arbitrary3 e,(Some xc,s)))" + w=undefined3 e \ G\(Some xc,s) \e\\n\ (undefined3 e,(Some xc,s)))" apply auto apply (frule evaln_abrupt_lemma, auto)+ done @@ -365,13 +365,13 @@ | _ => SOME (mk_meta_eq @{thm evaln_abrupt})) *} -lemma evaln_LitI: "G\s \Lit v-\(if normal s then v else arbitrary)\n\ s" +lemma evaln_LitI: "G\s \Lit v-\(if normal s then v else undefined)\n\ s" apply (case_tac "s", case_tac "a = None") by (auto intro!: evaln.Lit) lemma CondI: "\s1. \G\s \e-\b\n\ s1; G\s1 \(if the_Bool b then e1 else e2)-\v\n\ s2\ \ - G\s \e ? e1 : e2-\(if normal s1 then v else arbitrary)\n\ s2" + G\s \e ? e1 : e2-\(if normal s1 then v else undefined)\n\ s2" apply (case_tac "s", case_tac "a = None") by (auto intro!: evaln.Cond) @@ -520,7 +520,7 @@ proof (induct) case (Abrupt xc s t) obtain n where - "G\(Some xc, s) \t\\n\ (arbitrary3 t, (Some xc, s))" + "G\(Some xc, s) \t\\n\ (undefined3 t, (Some xc, s))" by (iprover intro: evaln.Abrupt) then show ?case .. next diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/Example.thy Tue Oct 07 16:07:50 2008 +0200 @@ -230,7 +230,7 @@ lemma table_classes_Object [simp]: "table_of Classes Object = Some \access=Public,cfields=[] ,methods=Object_mdecls - ,init=Skip,super=arbitrary,superIfs=[]\" + ,init=Skip,super=undefined,superIfs=[]\" apply (unfold table_classes_defs) apply (simp (no_asm) add:Object_def) done @@ -1246,13 +1246,13 @@ "obj_c" == "\tag=CInst (SXcpt NullPointer),values=CONST empty\" "arr_N" == "CONST empty(Inl (CONST arr, CONST Base)\Null)" "arr_a" == "CONST empty(Inl (CONST arr, CONST Base)\Addr a)" - "globs1" == "CONST empty(Inr (CONST Ext) \\tag=arbitrary, values=CONST empty\) - (Inr (CONST Base) \\tag=arbitrary, values=arr_N\) - (Inr Object\\tag=arbitrary, values=CONST empty\)" - "globs2" == "CONST empty(Inr (CONST Ext) \\tag=arbitrary, values=CONST empty\) - (Inr Object\\tag=arbitrary, values=CONST empty\) + "globs1" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) + (Inr (CONST Base) \\tag=CONST undefined, values=arr_N\) + (Inr Object\\tag=CONST undefined, values=CONST empty\)" + "globs2" == "CONST empty(Inr (CONST Ext) \\tag=CONST undefined, values=CONST empty\) + (Inr Object\\tag=CONST undefined, values=CONST empty\) (Inl a\obj_a) - (Inr (CONST Base) \\tag=arbitrary, values=arr_a\)" + (Inr (CONST Base) \\tag=CONST undefined, values=arr_a\)" "globs3" == "globs2(Inl b\obj_b)" "globs8" == "globs3(Inl c\obj_c)" "locs3" == "CONST empty(VName (CONST e)\Addr b)" diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/State.thy Tue Oct 07 16:07:50 2008 +0200 @@ -328,7 +328,7 @@ init_class_obj :: "prog \ qtname \ st \ st" translations - "init_class_obj G C" == "init_obj G arbitrary (Inr C)" + "init_class_obj G C" == "init_obj G CONST undefined (Inr C)" lemma gupd_def2 [simp]: "gupd(r\obj) (st g l) = st (g(r\obj)) l" apply (unfold gupd_def) diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/Trans.thy --- a/src/HOL/Bali/Trans.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/Trans.thy Tue Oct 07 16:07:50 2008 +0200 @@ -81,7 +81,7 @@ \ x c. t \ \Skip Finally c\ \ xc \ Xcpt x; \ a c. t \ \FinA a c\\ \ - G\(t,Some xc,s) \1 (\Lit arbitrary\,Some xc,s)" + G\(t,Some xc,s) \1 (\Lit undefined\,Some xc,s)" | InsInitE: "\G\(\c\,Norm s) \1 (\c'\, s')\ \ diff -r 5818d9cfb2e7 -r 644b62cf678f src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/TypeSafe.thy Tue Oct 07 16:07:50 2008 +0200 @@ -1738,7 +1738,7 @@ from `(Some xc, s)\\(G,L)` show "(Some xc, s)\\(G,L) \ (normal (Some xc, s) - \ G,L,store (Some xc,s)\t\arbitrary3 t\\T) \ + \ G,L,store (Some xc,s)\t\undefined3 t\\T) \