--- 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) \<one> A
- else arbitrary"
+ else undefined"
syntax
"_finprod" :: "index => idt => 'a set => 'b => 'b"
--- 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 ["\<Z>"]
- where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
+ where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
@@ -128,7 +128,7 @@
{ fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
note mult = this
have one: "one \<Z> = 1" by (simp add: int_ring_def)
- show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
+ show "finprod \<Z> 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 ["\<Z>"]
where "zero \<Z> = 0"
and "add \<Z> x y = x + y"
- and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
+ and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
@@ -153,7 +153,7 @@
{ fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
note add = this
show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
- show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
+ show "finsum \<Z> 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)
--- 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\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
-| Abrupt: "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
+| Abrupt: "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
--{* variables *}
| LVar: " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
--- 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|\<Turnstile>\<Colon>{ {P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
+ show "G,A|\<Turnstile>\<Colon>{ {P\<leftarrow>undefined3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
proof (rule validI)
fix n s0 L accC T C v s1 Y Z
assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
- assume "(P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal) Y s0 Z"
- then obtain P: "P (arbitrary3 t) s0 Z" and abrupt_s0: "\<not> normal s0"
+ assume "(P\<leftarrow>undefined3 t \<and>. Not \<circ> normal) Y s0 Z"
+ then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "\<not> 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 \<and> s1\<Colon>\<preceq>(G, L)"
@@ -2175,13 +2175,13 @@
note conf = `(Some abr, s)\<Colon>\<preceq>(G, L)`
note P = `P Y' (Some abr, s) Z`
note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
- show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (arbitrary3 t') (Some abr, s) Z"
+ show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
proof -
have eval_e:
- "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (arbitrary3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
+ "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
by auto
from valid_e P valid_A conf eval_e
- have "P' (arbitrary3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
+ have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
by (cases rule: validE [where ?P="P"]) simp+
with t' show ?thesis
by auto
--- 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 \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
- init=Skip,super=arbitrary,superIfs=[]\<rparr>)"
+ init=Skip,super=undefined,superIfs=[]\<rparr>)"
SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>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 (\<lambda>G. (subint1 G)^-1)"
"iface_rec (G,I) =
(\<lambda>f. case iface G I of
- None \<Rightarrow> arbitrary
+ None \<Rightarrow> undefined
| Some i \<Rightarrow> if ws_prog G
then f I i
((\<lambda>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 (\<lambda>G. (subcls1 G)^-1)"
"class_rec(G,C) =
(\<lambda>t f. case class G C of
- None \<Rightarrow> arbitrary
+ None \<Rightarrow> undefined
| Some c \<Rightarrow> 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]
--- 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 @@
"\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
constdefs
- arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
- "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
- (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
+ undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
+ "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
+ (\<lambda>x. In2 undefined) (\<lambda>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) = \<diamondsuit>"
-by (simp add: arbitrary3_def)
+lemma [simp]: "undefined3 (In1r x) = \<diamondsuit>"
+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\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
+ "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>undefined\<rightarrow> (Some x,s)"
| New: "\<lbrakk>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\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t, (Some xc, s))"
+ "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t, (Some xc, s))"
--{* execution of statements *}
@@ -971,13 +971,13 @@
lemma eval_abrupt_lemma:
- "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
+ "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = undefined3 t"
by (erule eval_cases, auto)
lemma eval_abrupt:
" G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =
- (s'=(Some xc,s) \<and> w=arbitrary3 t \<and>
- G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
+ (s'=(Some xc,s) \<and> w=undefined3 t \<and>
+ G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (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\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
+lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Lit)
@@ -1007,7 +1007,7 @@
lemma CondI:
"\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow>
- G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
+ G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<rightarrow> s2"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: eval.Cond)
@@ -1054,7 +1054,7 @@
done
lemma eval_StatRef:
-"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
+"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else undefined)\<rightarrow> s"
apply (case_tac "s", simp)
apply (case_tac "a = None")
apply (auto del: eval.Abrupt intro!: eval.intros)
--- 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\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
+| Abrupt: "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
--{* evaluation of variables *}
@@ -346,13 +346,13 @@
qed
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow>
- fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
+ fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
apply (erule evaln_cases , auto)
done
lemma evaln_abrupt:
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>
- w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
+ w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (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\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
+lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
apply (case_tac "s", case_tac "a = None")
by (auto intro!: evaln.Lit)
lemma CondI:
"\<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>
- G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
+ G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> 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\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
+ "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
by (iprover intro: evaln.Abrupt)
then show ?case ..
next
--- 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 \<lparr>access=Public,cfields=[]
,methods=Object_mdecls
- ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
+ ,init=Skip,super=undefined,superIfs=[]\<rparr>"
apply (unfold table_classes_defs)
apply (simp (no_asm) add:Object_def)
done
@@ -1246,13 +1246,13 @@
"obj_c" == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
"arr_N" == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
"arr_a" == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
- "globs1" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
- (Inr (CONST Base) \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)"
- "globs2" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
- (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
+ "globs1" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
+ (Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
+ (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
+ "globs2" == "CONST empty(Inr (CONST Ext) \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
+ (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
(Inl a\<mapsto>obj_a)
- (Inr (CONST Base) \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
+ (Inr (CONST Base) \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
"globs3" == "globs2(Inl b\<mapsto>obj_b)"
"globs8" == "globs3(Inl c\<mapsto>obj_c)"
"locs3" == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
--- 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 \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> 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\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
apply (unfold gupd_def)
--- 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 @@
\<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
\<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk>
\<Longrightarrow>
- G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
+ G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
\<Longrightarrow>
--- 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)\<Colon>\<preceq>(G,L)`
show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and>
(normal (Some xc, s)
- \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and>
+ \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and>
(error_free (Some xc, s) = error_free (Some xc, s))"
by simp
next
@@ -3850,7 +3850,7 @@
and abrupt: "\<And> s t abr L accC T A.
\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
- \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
+ \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
and skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
and expr: "\<And> e s0 s1 v L accC eT E.
\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
--- a/src/HOL/Bali/WellForm.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Bali/WellForm.thy Tue Oct 07 16:07:50 2008 +0200
@@ -562,7 +562,7 @@
lemma class_Object [simp]:
"wf_prog G \<Longrightarrow>
class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
- init=Skip,super=arbitrary,superIfs=[]\<rparr>"
+ init=Skip,super=undefined,superIfs=[]\<rparr>"
apply (unfold wf_prog_def Let_def ObjectC_def)
apply (fast dest!: map_of_SomeI)
done
--- a/src/HOL/Datatype.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Datatype.thy Tue Oct 07 16:07:50 2008 +0200
@@ -567,10 +567,10 @@
constdefs
Suml :: "('a => 'c) => 'a + 'b => 'c"
- "Suml == (%f. sum_case f arbitrary)"
+ "Suml == (%f. sum_case f undefined)"
Sumr :: "('b => 'c) => 'a + 'b => 'c"
- "Sumr == sum_case arbitrary"
+ "Sumr == sum_case undefined"
lemma Suml_inject: "Suml f = Suml g ==> f = g"
by (unfold Suml_def) (erule sum_case_inject)
--- a/src/HOL/HoareParallel/OG_Syntax.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/HoareParallel/OG_Syntax.thy Tue Oct 07 16:07:50 2008 +0200
@@ -45,7 +45,7 @@
"IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
"IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
"WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
- "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV arbitrary DO c OD"
+ "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
"r SKIP" \<rightleftharpoons> "AnnBasic r id"
"c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2"
--- a/src/HOL/IMPP/Misc.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/IMPP/Misc.thy Tue Oct 07 16:07:50 2008 +0200
@@ -11,7 +11,7 @@
begin
defs
- newlocs_def: "newlocs == %x. arbitrary"
+ newlocs_def: "newlocs == %x. undefined"
setlocs_def: "setlocs s l' == case s of st g l => st g l'"
getlocs_def: "getlocs s == case s of st g l => l"
update_def: "update s vn v == case vn of
--- a/src/HOL/Isar_examples/Hoare.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Isar_examples/Hoare.thy Tue Oct 07 16:07:50 2008 +0200
@@ -232,7 +232,7 @@
"\<acute>x := a" => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
"IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
"WHILE b INV i DO c OD" => "While .{b}. i c"
- "WHILE b DO c OD" == "WHILE b INV arbitrary DO c OD"
+ "WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD"
parse_translation {*
let
@@ -383,7 +383,7 @@
by (rule while)
lemma [intro?]:
- "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"
+ "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
by (rule while)
--- a/src/HOL/Library/FuncSet.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Oct 07 16:07:50 2008 +0200
@@ -15,11 +15,11 @@
definition
extensional :: "'a set => ('a => 'b) set" where
- "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
+ "extensional A = {f. \<forall>x. x~:A --> f x = undefined}"
definition
"restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
- "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
+ "restrict f A = (%x. if x \<in> A then f x else undefined)"
abbreviation
funcset :: "['a set, 'b set] => ('a => 'b) set"
@@ -117,7 +117,7 @@
by (simp add: Pi_def restrict_def)
lemma restrict_apply [simp]:
- "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
+ "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
by (simp add: restrict_def)
lemma restrict_ext:
@@ -164,7 +164,7 @@
subsection{*Extensionality*}
-lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
+lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
by (simp add: extensional_def)
lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
--- a/src/HOL/Library/Heap.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Library/Heap.thy Tue Oct 07 16:07:50 2008 +0200
@@ -115,7 +115,7 @@
lim :: addr
definition empty :: heap where
- "empty = \<lparr>arrays = (\<lambda>_. arbitrary), refs = (\<lambda>_. arbitrary), lim = 0\<rparr>" -- "why arbitrary?"
+ "empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
subsection {* Imperative references and arrays *}
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Tue Oct 07 16:07:50 2008 +0200
@@ -926,7 +926,7 @@
with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
have state'_val:
"state' =
- Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary,
+ Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined,
D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)"
(is "state' = Norm (hp, ?f # ?f' # frs)")
by (simp add: raise_system_xcpt_def)
@@ -947,7 +947,7 @@
(is "G \<turnstile> ?LT <=l LT0")
by (simp add: wt_start_def sup_state_conv)
- have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
+ have r: "approx_loc G hp (replicate mxl' undefined) (replicate mxl' Err)"
by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
from wfprog mD is_class_D
@@ -963,7 +963,7 @@
hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
with r a l_o l
- have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
+ have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' undefined) ?LT"
(is "approx_loc G hp ?lt ?LT")
by (auto simp add: approx_loc_append approx_stk_def)
--- a/src/HOL/MicroJava/Comp/CorrComp.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy Tue Oct 07 16:07:50 2008 +0200
@@ -1138,7 +1138,7 @@
apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
apply (simp (no_asm_simp)) (* length pns = length pvs *)
-apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
+apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) undefined) *)
(* body statement *)
--- a/src/HOL/MicroJava/J/Eval.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Tue Oct 07 16:07:50 2008 +0200
@@ -45,7 +45,7 @@
-- "evaluation of expressions"
- XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)" -- "cf. 15.5"
+ XcptE:"G\<turnstile>(Some xc,s) -e\<succ>undefined-> (Some xc,s)" -- "cf. 15.5"
-- "cf. 15.8.1"
| NewC: "[| h = heap s; (a,x) = new_Addr h;
@@ -98,7 +98,7 @@
-- "evaluation of expression lists"
-- "cf. 15.5"
-| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
+| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]undefined-> (Some xc,s)"
-- "cf. 15.11.???"
| Nil: "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
--- a/src/HOL/MicroJava/J/Example.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Tue Oct 07 16:07:50 2008 +0200
@@ -137,7 +137,7 @@
done
declare map_of_Cons [simp del] -- "sic!"
-lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
+lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])"
apply (unfold ObjectC_def class_def)
apply (simp (no_asm))
done
--- a/src/HOL/MicroJava/J/JListExample.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy Tue Oct 07 16:07:50 2008 +0200
@@ -5,7 +5,9 @@
header {* \isaheader{Example for generating executable code from Java semantics} *}
-theory JListExample imports Eval SystemClasses begin
+theory JListExample
+imports Eval SystemClasses
+begin
ML {* Syntax.ambiguity_level := 100000 *}
@@ -72,9 +74,9 @@
in nr 0 end;
*}
- "arbitrary" ("(raise Match)")
- "arbitrary :: val" ("{* Unit *}")
- "arbitrary :: cname" ("\"\"")
+ "undefined" ("(raise Match)")
+ "undefined :: val" ("{* Unit *}")
+ "undefined :: cname" ("\"\"")
"Object" ("\"Object\"")
"list_name" ("\"list\"")
--- a/src/HOL/MicroJava/J/SystemClasses.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/SystemClasses.thy Tue Oct 07 16:07:50 2008 +0200
@@ -15,7 +15,7 @@
constdefs
ObjectC :: "'c cdecl"
- "ObjectC \<equiv> (Object, (arbitrary,[],[]))"
+ "ObjectC \<equiv> (Object, (undefined,[],[]))"
NullPointerC :: "'c cdecl"
"NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 07 16:07:50 2008 +0200
@@ -56,7 +56,7 @@
(cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
"class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
(\<lambda>r C t f. case class G C of
- None \<Rightarrow> arbitrary
+ None \<Rightarrow> undefined
| Some (D,fs,ms) \<Rightarrow>
f C fs ms (if C = Object then t else r D t f))"
@@ -68,10 +68,10 @@
definition
"wf_class G = wfP ((subcls1 G)^--1)"
-lemma class_rec_func [code func]:
+lemma class_rec_func (*[code func]*):
"class_rec G C t f = (if wf_class G then
(case class G C
- of None \<Rightarrow> arbitrary
+ of None \<Rightarrow> undefined
| Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f))
else class_rec G C t f)"
proof (cases "wf_class G")
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Oct 07 16:07:50 2008 +0200
@@ -46,6 +46,6 @@
start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
"start_state G C m \<equiv>
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
- (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])"
+ (None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])"
end
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Tue Oct 07 16:07:50 2008 +0200
@@ -66,7 +66,7 @@
dynT = fst(the(hp(the_Addr oref)));
(dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
frs' = if xp'=None then
- [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
+ [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
else []
in
(xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))"
--- a/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy Tue Oct 07 16:07:50 2008 +0200
@@ -101,9 +101,9 @@
in nr 0 end;
*}
- "arbitrary" ("(raise Match)")
- "arbitrary :: val" ("{* Unit *}")
- "arbitrary :: cname" ("{* Object *}")
+ "undefined" ("(raise Match)")
+ "undefined :: val" ("{* Unit *}")
+ "undefined :: cname" ("{* Object *}")
"list_nam" ("\"list\"")
"test_nam" ("\"test\"")
--- a/src/HOL/NanoJava/TypeRel.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/NanoJava/TypeRel.thy Tue Oct 07 16:07:50 2008 +0200
@@ -104,10 +104,10 @@
consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)"
recdef (permissive) class_rec "subcls1\<inverse>"
- "class_rec C = (\<lambda>f. case class C of None \<Rightarrow> arbitrary
+ "class_rec C = (\<lambda>f. case class C of None \<Rightarrow> undefined
| Some m \<Rightarrow> if wf (subcls1\<inverse>)
then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
- else arbitrary)"
+ else undefined)"
(hints intro: subcls1I)
lemma class_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
--- a/src/HOL/Nominal/nominal_primrec.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Oct 07 16:07:50 2008 +0200
@@ -142,7 +142,7 @@
(case AList.lookup (op =) eqns cname of
NONE => (warning ("No equation for constructor " ^ quote cname ^
"\nin definition of function " ^ quote fname);
- (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
+ (fnameTs', fnss', (Const (@{const_name undefined}, dummyT))::fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
@@ -183,7 +183,7 @@
case AList.lookup (op =) fns i of
NONE =>
let
- val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
+ val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
--- a/src/HOL/Sum_Type.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Sum_Type.thy Tue Oct 07 16:07:50 2008 +0200
@@ -126,8 +126,8 @@
(if (\<exists>!y. x = Inl y)
then f (THE y. x = Inl y)
else g (THE y. x = Inr y))"
-definition "Projl x = sum_case id arbitrary x"
-definition "Projr x = sum_case arbitrary id x"
+definition "Projl x = sum_case id undefined x"
+definition "Projr x = sum_case undefined id x"
lemma sum_cases[simp]:
"sum_case f g (Inl x) = f x"
--- a/src/HOL/TLA/Memory/RPCParameters.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy Tue Oct 07 16:07:50 2008 +0200
@@ -44,7 +44,7 @@
| (othercall v) => False"
RPCRelayArg_def: "RPCRelayArg ra ==
case ra of (memcall m) => m
- | (othercall v) => arbitrary"
+ | (othercall v) => undefined"
lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Oct 07 16:07:50 2008 +0200
@@ -291,7 +291,7 @@
let
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
- in Const ("arbitrary", Ts @ Ts' ---> T')
+ in Const (@{const_name undefined}, Ts @ Ts' ---> T')
end) constrs) descr';
val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Oct 07 16:07:50 2008 +0200
@@ -125,7 +125,7 @@
{left = fn t => In0 $ t,
right = fn t => In1 $ t,
init =
- if ts = [] then Const ("arbitrary", Univ_elT)
+ if ts = [] then Const (@{const_name undefined}, Univ_elT)
else foldr1 (HOLogic.mk_binop Scons_name) ts};
(* function spaces *)
--- a/src/HOL/Tools/function_package/fundef_common.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Oct 07 16:07:50 2008 +0200
@@ -189,7 +189,7 @@
FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
val default_config =
- FundefConfig { sequential=false, default="%x. arbitrary", domintros=false, tailrec=false }
+ FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false }
(* Analyzing function equations *)
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Oct 07 16:07:50 2008 +0200
@@ -298,7 +298,7 @@
#> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
-val fun_config = FundefConfig { sequential=true, default="%x. arbitrary" (* FIXME dynamic scoping *),
+val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*),
domintros=false, tailrec=false }
--- a/src/HOL/Tools/inductive_package.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Oct 07 16:07:50 2008 +0200
@@ -212,7 +212,7 @@
else apsnd (cons p) (find_arg T x ps);
fun make_args Ts xs =
- map (fn (T, (NONE, ())) => Const ("arbitrary", T) | (_, (SOME t, ())) => t)
+ map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t)
(fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
fun make_args' Ts xs Us =
--- a/src/HOL/Tools/refute.ML Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Tools/refute.ML Tue Oct 07 16:07:50 2008 +0200
@@ -681,7 +681,7 @@
Const ("True", _) => t
| (* redundant, since 'False' is also an IDT constructor *)
Const ("False", _) => t
- | Const ("arbitrary", _) => t
+ | Const (@{const_name undefined}, _) => t
| Const ("The", _) => t
| Const ("Hilbert_Choice.Eps", _) => t
| Const ("All", _) => t
@@ -856,7 +856,7 @@
| Const ("True", _) => axs
(* redundant, since 'False' is also an IDT constructor *)
| Const ("False", _) => axs
- | Const ("arbitrary", T) => collect_type_axioms (axs, T)
+ | Const (@{const_name undefined}, T) => collect_type_axioms (axs, T)
| Const ("The", T) =>
let
val ax = specialize_type thy ("The", T)
@@ -3202,23 +3202,23 @@
end
| Type ("prop", []) =>
(case index_from_interpretation intr of
- ~1 => SOME (HOLogic.mk_Trueprop (Const ("arbitrary", HOLogic.boolT)))
+ ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
| 0 => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
| 1 => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
| _ => raise REFUTE ("stlc_interpreter",
"illegal interpretation for a propositional value"))
| Type _ => if index_from_interpretation intr = (~1) then
- SOME (Const ("arbitrary", T))
+ SOME (Const (@{const_name undefined}, T))
else
SOME (Const (string_of_typ T ^
string_of_int (index_from_interpretation intr), T))
| TFree _ => if index_from_interpretation intr = (~1) then
- SOME (Const ("arbitrary", T))
+ SOME (Const (@{const_name undefined}, T))
else
SOME (Const (string_of_typ T ^
string_of_int (index_from_interpretation intr), T))
| TVar _ => if index_from_interpretation intr = (~1) then
- SOME (Const ("arbitrary", T))
+ SOME (Const (@{const_name undefined}, T))
else
SOME (Const (string_of_typ T ^
string_of_int (index_from_interpretation intr), T))
@@ -3291,7 +3291,7 @@
"interpretation is not a leaf"))
in
if element < 0 then
- SOME (Const ("arbitrary", Type (s, Ts)))
+ SOME (Const (@{const_name undefined}, Type (s, Ts)))
else let
(* takes a datatype constructor, and if for some arguments this *)
(* constructor generates the datatype's element that is given by *)
--- a/src/HOL/Wellfounded.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Wellfounded.thy Tue Oct 07 16:07:50 2008 +0200
@@ -33,7 +33,7 @@
"acyclic r == !x. (x,x) ~: r^+"
cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
- "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
+ "cut f r x == (%y. if (y,x):r then f y else undefined)"
adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
"adm_wf R F == ALL f g x.
--- a/src/HOL/Word/WordDefinition.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/Word/WordDefinition.thy Tue Oct 07 16:07:50 2008 +0200
@@ -66,9 +66,9 @@
-- "whether a cast (or other) function is to a longer or shorter length"
source_size :: "('a :: len0 word => 'b) => nat"
- "source_size c == let arb = arbitrary ; x = c arb in size arb"
+ "source_size c == let arb = undefined ; x = c arb in size arb"
target_size :: "('a => 'b :: len0 word) => nat"
- "target_size c == size (c arbitrary)"
+ "target_size c == size (c undefined)"
is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
"is_up c == source_size c <= target_size c"
is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
--- a/src/HOL/ex/Quickcheck.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Tue Oct 07 16:07:50 2008 +0200
@@ -48,10 +48,10 @@
lemma random'_if:
fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
- assumes "random' 0 j = undefined"
+ assumes "random' 0 j = (\<lambda>s. undefined)"
and "\<And>i. random' (Suc_index i) j = rhs2 i"
shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
- by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun)
+ by (cases i rule: index.exhaust) (insert assms, simp_all)
setup {*
let
@@ -115,7 +115,8 @@
|> (map o apsnd) (List.partition fst)
|> map (mk_clauses thy this_ty)
val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
- (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, this_ty')),
+ (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
+ Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
(random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
]))) rhss;
in eqss end;
@@ -198,7 +199,7 @@
(seed : Random_Engine.seed) =
let
val (seed', seed'') = random_split seed;
- val state = ref (seed', [], Const (@{const_name arbitrary}, T1 --> T2));
+ val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
val fun_upd = Const (@{const_name fun_upd},
(T1 --> T2) --> T1 --> T2 --> T1 --> T2);
fun random_fun' x =
--- a/src/HOL/ex/Refute_Examples.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Tue Oct 07 16:07:50 2008 +0200
@@ -421,21 +421,21 @@
(*****************************************************************************)
-subsubsection {* arbitrary *}
+subsubsection {* undefined *}
-lemma "arbitrary"
+lemma "undefined"
refute
oops
-lemma "P arbitrary"
+lemma "P undefined"
refute
oops
-lemma "arbitrary x"
+lemma "undefined x"
refute
oops
-lemma "arbitrary arbitrary"
+lemma "undefined undefined"
refute
oops
@@ -494,7 +494,7 @@
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
-typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
+typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
by auto
lemma "(x::'a myTdef) = y"
@@ -1326,7 +1326,7 @@
inductive_set arbitrarySet :: "'a set"
where
- "arbitrary : arbitrarySet"
+ "undefined : arbitrarySet"
lemma "x : arbitrarySet"
refute
@@ -1360,7 +1360,7 @@
a_even :: "'a set"
and a_odd :: "'a set"
where
- "arbitrary : a_even"
+ "undefined : a_even"
| "x : a_even \<Longrightarrow> f x : a_odd"
| "x : a_odd \<Longrightarrow> f x : a_even"
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Oct 07 16:07:50 2008 +0200
@@ -26,7 +26,7 @@
definition
jth :: "nat => 'a fstream => 'a" where
- "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary)"
+ "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)"
definition
first :: "'a fstream => 'a" where
@@ -34,8 +34,7 @@
definition
last :: "'a fstream => 'a" where
- "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
- | Infty => arbitrary)"
+ "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
abbreviation
@@ -92,19 +91,19 @@
lemma last_fsingleton[simp]: "last (<a>) = a"
by (simp add: last_def)
-lemma first_UU[simp]: "first UU = arbitrary"
+lemma first_UU[simp]: "first UU = undefined"
by (simp add: first_def jth_def)
-lemma last_UU[simp]:"last UU = arbitrary"
+lemma last_UU[simp]:"last UU = undefined"
by (simp add: last_def jth_def inat_defs)
-lemma last_infinite[simp]:"#s = Infty ==> last s = arbitrary"
+lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
by (simp add: last_def)
-lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = arbitrary"
+lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
by (simp add: jth_def inat_defs split:inat_splits, auto)
-lemma jth_UU[simp]:"jth n UU = arbitrary"
+lemma jth_UU[simp]:"jth n UU = undefined"
by (simp add: jth_def)
lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s"
--- a/src/HOLCF/IOA/meta_theory/TL.thy Tue Oct 07 16:07:40 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.thy Tue Oct 07 16:07:50 2008 +0200
@@ -38,9 +38,7 @@
defs
unlift_def:
- "unlift x == (case x of
- UU => arbitrary
- | Def y => y)"
+ "unlift x == (case x of Def y => y)"
(* this means that for nil and UU the effect is unpredictable *)
Init_def: