arbitrary is undefined
authorhaftmann
Tue Oct 07 16:07:50 2008 +0200 (2008-10-07)
changeset 28524644b62cf678f
parent 28523 5818d9cfb2e7
child 28525 42297ae4df47
arbitrary is undefined
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Trans.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Datatype.thy
src/HOL/HoareParallel/OG_Syntax.thy
src/HOL/IMPP/Misc.thy
src/HOL/Isar_examples/Hoare.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Heap.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/J/SystemClasses.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/JVM/JVMExec.thy
src/HOL/MicroJava/JVM/JVMExecInstr.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/NanoJava/TypeRel.thy
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Sum_Type.thy
src/HOL/TLA/Memory/RPCParameters.thy
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/refute.ML
src/HOL/Wellfounded.thy
src/HOL/Word/WordDefinition.thy
src/HOL/ex/Quickcheck.thy
src/HOL/ex/Refute_Examples.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/IOA/meta_theory/TL.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -291,7 +291,7 @@
     1.4    finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
     1.5    "finprod G f A == if finite A
     1.6        then foldD (carrier G) (mult G o f) \<one> A
     1.7 -      else arbitrary"
     1.8 +      else undefined"
     1.9  
    1.10  syntax
    1.11    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:40 2008 +0200
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Tue Oct 07 16:07:50 2008 +0200
     2.3 @@ -118,7 +118,7 @@
     2.4  qed
     2.5  
     2.6  interpretation int: comm_monoid ["\<Z>"]
     2.7 -  where "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
     2.8 +  where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
     2.9  proof -
    2.10    -- "Specification"
    2.11    show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    2.12 @@ -128,7 +128,7 @@
    2.13    { fix x y have "mult \<Z> x y = x * y" by (simp add: int_ring_def) }
    2.14    note mult = this
    2.15    have one: "one \<Z> = 1" by (simp add: int_ring_def)
    2.16 -  show "finprod \<Z> f A = (if finite A then setprod f A else arbitrary)"
    2.17 +  show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    2.18    proof (cases "finite A")
    2.19      case True then show ?thesis proof induct
    2.20        case empty show ?case by (simp add: one)
    2.21 @@ -143,7 +143,7 @@
    2.22  interpretation int: abelian_monoid ["\<Z>"]
    2.23    where "zero \<Z> = 0"
    2.24      and "add \<Z> x y = x + y"
    2.25 -    and "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
    2.26 +    and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    2.27  proof -
    2.28    -- "Specification"
    2.29    show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    2.30 @@ -153,7 +153,7 @@
    2.31    { fix x y show "add \<Z> x y = x + y" by (simp add: int_ring_def) }
    2.32    note add = this
    2.33    show zero: "zero \<Z> = 0" by (simp add: int_ring_def)
    2.34 -  show "finsum \<Z> f A = (if finite A then setsum f A else arbitrary)"
    2.35 +  show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    2.36    proof (cases "finite A")
    2.37      case True then show ?thesis proof induct
    2.38        case empty show ?case by (simp add: zero)
     3.1 --- a/src/HOL/Bali/AxSem.thy	Tue Oct 07 16:07:40 2008 +0200
     3.2 +++ b/src/HOL/Bali/AxSem.thy	Tue Oct 07 16:07:50 2008 +0200
     3.3 @@ -501,7 +501,7 @@
     3.4  
     3.5  | hazard:"G,A\<turnstile>{P \<and>. Not \<circ> type_ok G t} t\<succ> {Q}"
     3.6  
     3.7 -| Abrupt:  "G,A\<turnstile>{P\<leftarrow>(arbitrary3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
     3.8 +| Abrupt:  "G,A\<turnstile>{P\<leftarrow>(undefined3 t) \<and>. Not \<circ> normal} t\<succ> {P}"
     3.9  
    3.10    --{* variables *}
    3.11  | LVar:  " G,A\<turnstile>{Normal (\<lambda>s.. P\<leftarrow>Var (lvar vn s))} LVar vn=\<succ> {P}"
     4.1 --- a/src/HOL/Bali/AxSound.thy	Tue Oct 07 16:07:40 2008 +0200
     4.2 +++ b/src/HOL/Bali/AxSound.thy	Tue Oct 07 16:07:50 2008 +0200
     4.3 @@ -433,15 +433,15 @@
     4.4      by (simp add: ax_valids2_def triple_valid2_def2 type_ok_def) fast
     4.5  next
     4.6    case (Abrupt A P t)
     4.7 -  show "G,A|\<Turnstile>\<Colon>{ {P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
     4.8 +  show "G,A|\<Turnstile>\<Colon>{ {P\<leftarrow>undefined3 t \<and>. Not \<circ> normal} t\<succ> {P} }"
     4.9    proof (rule validI)
    4.10      fix n s0 L accC T C v s1 Y Z 
    4.11      assume conf_s0: "s0\<Colon>\<preceq>(G, L)"
    4.12      assume eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s1)"
    4.13 -    assume "(P\<leftarrow>arbitrary3 t \<and>. Not \<circ> normal) Y s0 Z"
    4.14 -    then obtain P: "P (arbitrary3 t) s0 Z" and abrupt_s0: "\<not> normal s0"
    4.15 +    assume "(P\<leftarrow>undefined3 t \<and>. Not \<circ> normal) Y s0 Z"
    4.16 +    then obtain P: "P (undefined3 t) s0 Z" and abrupt_s0: "\<not> normal s0"
    4.17        by simp
    4.18 -    from eval abrupt_s0 obtain "s1=s0" and "v=arbitrary3 t"
    4.19 +    from eval abrupt_s0 obtain "s1=s0" and "v=undefined3 t"
    4.20        by auto
    4.21      with P conf_s0
    4.22      show "P v s1 Z \<and> s1\<Colon>\<preceq>(G, L)"
    4.23 @@ -2175,13 +2175,13 @@
    4.24  	  note conf = `(Some abr, s)\<Colon>\<preceq>(G, L)`
    4.25  	  note P = `P Y' (Some abr, s) Z`
    4.26  	  note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
    4.27 -	  show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (arbitrary3 t') (Some abr, s) Z"
    4.28 +	  show "(P'\<leftarrow>=False\<down>=\<diamondsuit>) (undefined3 t') (Some abr, s) Z"
    4.29  	  proof -
    4.30  	    have eval_e: 
    4.31 -	      "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (arbitrary3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
    4.32 +	      "G\<turnstile>(Some abr,s) \<midarrow>\<langle>e\<rangle>\<^sub>e\<succ>\<midarrow>n'\<rightarrow> (undefined3 \<langle>e\<rangle>\<^sub>e,(Some abr,s))"
    4.33  	      by auto
    4.34  	    from valid_e P valid_A conf eval_e 
    4.35 -	    have "P' (arbitrary3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
    4.36 +	    have "P' (undefined3 \<langle>e\<rangle>\<^sub>e) (Some abr,s) Z"
    4.37  	      by (cases rule: validE [where ?P="P"]) simp+
    4.38  	    with t' show ?thesis
    4.39  	      by auto
     5.1 --- a/src/HOL/Bali/Decl.thy	Tue Oct 07 16:07:40 2008 +0200
     5.2 +++ b/src/HOL/Bali/Decl.thy	Tue Oct 07 16:07:50 2008 +0200
     5.3 @@ -373,7 +373,7 @@
     5.4  
     5.5  
     5.6  ObjectC_def:"ObjectC  \<equiv> (Object,\<lparr>access=Public,cfields=[],methods=Object_mdecls,
     5.7 -                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>)"
     5.8 +                                  init=Skip,super=undefined,superIfs=[]\<rparr>)"
     5.9  SXcptC_def:"SXcptC xn\<equiv> (SXcpt xn,\<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
    5.10                                     init=Skip,
    5.11                                     super=if xn = Throwable then Object 
    5.12 @@ -761,11 +761,11 @@
    5.13  recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)" 
    5.14  "iface_rec (G,I) = 
    5.15    (\<lambda>f. case iface G I of 
    5.16 -         None \<Rightarrow> arbitrary 
    5.17 +         None \<Rightarrow> undefined 
    5.18         | Some i \<Rightarrow> if ws_prog G 
    5.19                        then f I i 
    5.20                                 ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
    5.21 -                      else arbitrary)"
    5.22 +                      else undefined)"
    5.23  (hints recdef_wf: wf_subint1 intro: subint1I)
    5.24  declare iface_rec.simps [simp del]
    5.25  
    5.26 @@ -779,12 +779,12 @@
    5.27  recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
    5.28  "class_rec(G,C) = 
    5.29    (\<lambda>t f. case class G C of 
    5.30 -           None \<Rightarrow> arbitrary 
    5.31 +           None \<Rightarrow> undefined 
    5.32           | Some c \<Rightarrow> if ws_prog G 
    5.33                          then f C c 
    5.34                                   (if C = Object then t 
    5.35                                                  else class_rec (G,super c) t f)
    5.36 -                        else arbitrary)"
    5.37 +                        else undefined)"
    5.38  (hints recdef_wf: wf_subcls1 intro: subcls1I)
    5.39  declare class_rec.simps [simp del]
    5.40  
     6.1 --- a/src/HOL/Bali/Eval.thy	Tue Oct 07 16:07:40 2008 +0200
     6.2 +++ b/src/HOL/Bali/Eval.thy	Tue Oct 07 16:07:50 2008 +0200
     6.3 @@ -58,7 +58,7 @@
     6.4    \end{itemize}
     6.5  \item the rules are defined carefully in order to be applicable even in not
     6.6    type-correct situations (yielding undefined values),
     6.7 -  e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}.
     6.8 +  e.g. @{text "the_Addr (Val (Bool b)) = undefined"}.
     6.9    \begin{itemize}
    6.10    \item[++] fewer rules 
    6.11    \item[-]  less readable because of auxiliary functions like @{text the_Addr}
    6.12 @@ -141,21 +141,21 @@
    6.13    "\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es"
    6.14  
    6.15  constdefs
    6.16 -  arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
    6.17 - "arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit))
    6.18 -                     (\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)"
    6.19 +  undefined3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals"
    6.20 + "undefined3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. undefined) (\<lambda>x. Unit))
    6.21 +                     (\<lambda>x. In2 undefined) (\<lambda>x. In3 undefined)"
    6.22  
    6.23 -lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary"
    6.24 -by (simp add: arbitrary3_def)
    6.25 +lemma [simp]: "undefined3 (In1l x) = In1 undefined"
    6.26 +by (simp add: undefined3_def)
    6.27  
    6.28 -lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>"
    6.29 -by (simp add: arbitrary3_def)
    6.30 +lemma [simp]: "undefined3 (In1r x) = \<diamondsuit>"
    6.31 +by (simp add: undefined3_def)
    6.32  
    6.33 -lemma [simp]: "arbitrary3 (In2  x) = In2 arbitrary"
    6.34 -by (simp add: arbitrary3_def)
    6.35 +lemma [simp]: "undefined3 (In2  x) = In2 undefined"
    6.36 +by (simp add: undefined3_def)
    6.37  
    6.38 -lemma [simp]: "arbitrary3 (In3  x) = In3 arbitrary"
    6.39 -by (simp add: arbitrary3_def)
    6.40 +lemma [simp]: "undefined3 (In3  x) = In3 undefined"
    6.41 +by (simp add: undefined3_def)
    6.42  
    6.43  
    6.44  section "exception throwing and catching"
    6.45 @@ -479,7 +479,7 @@
    6.46  where --{* allocating objects on the heap, cf. 12.5 *}
    6.47  
    6.48    Abrupt: 
    6.49 -  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)"
    6.50 +  "G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>undefined\<rightarrow> (Some x,s)"
    6.51  
    6.52  | New:	  "\<lbrakk>new_Addr (heap s) = Some a; 
    6.53  	    (x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi)
    6.54 @@ -522,7 +522,7 @@
    6.55  
    6.56    --{* cf. 14.1, 15.5 *}
    6.57  | Abrupt: 
    6.58 -   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t, (Some xc, s))"
    6.59 +   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t, (Some xc, s))"
    6.60  
    6.61  
    6.62  --{* execution of statements *}
    6.63 @@ -971,13 +971,13 @@
    6.64  
    6.65  
    6.66  lemma eval_abrupt_lemma: 
    6.67 -  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t"
    6.68 +  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = undefined3 t"
    6.69  by (erule eval_cases, auto)
    6.70  
    6.71  lemma eval_abrupt: 
    6.72   " G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') =  
    6.73 -     (s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 
    6.74 -     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))"
    6.75 +     (s'=(Some xc,s) \<and> w=undefined3 t \<and> 
    6.76 +     G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (undefined3 t,(Some xc,s)))"
    6.77  apply auto
    6.78  apply (frule eval_abrupt_lemma, auto)+
    6.79  done
    6.80 @@ -989,7 +989,7 @@
    6.81      | _ => SOME (mk_meta_eq @{thm eval_abrupt}))
    6.82  *}
    6.83  
    6.84 -lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s"
    6.85 +lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<rightarrow> s"
    6.86  apply (case_tac "s", case_tac "a = None")
    6.87  by (auto intro!: eval.Lit)
    6.88  
    6.89 @@ -1007,7 +1007,7 @@
    6.90  
    6.91  lemma CondI: 
    6.92    "\<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> 
    6.93 -         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2"
    6.94 +         G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<rightarrow> s2"
    6.95  apply (case_tac "s", case_tac "a = None")
    6.96  by (auto intro!: eval.Cond)
    6.97  
    6.98 @@ -1054,7 +1054,7 @@
    6.99  done
   6.100  
   6.101  lemma eval_StatRef: 
   6.102 -"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s"
   6.103 +"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else undefined)\<rightarrow> s"
   6.104  apply (case_tac "s", simp)
   6.105  apply (case_tac "a = None")
   6.106  apply (auto del: eval.Abrupt intro!: eval.intros)
     7.1 --- a/src/HOL/Bali/Evaln.thy	Tue Oct 07 16:07:40 2008 +0200
     7.2 +++ b/src/HOL/Bali/Evaln.thy	Tue Oct 07 16:07:50 2008 +0200
     7.3 @@ -49,7 +49,7 @@
     7.4  
     7.5  --{* propagation of abrupt completion *}
     7.6  
     7.7 -| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
     7.8 +| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
     7.9  
    7.10  
    7.11  --{* evaluation of variables *}
    7.12 @@ -346,13 +346,13 @@
    7.13  qed
    7.14  
    7.15  lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
    7.16 - fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
    7.17 + fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
    7.18  apply (erule evaln_cases , auto)
    7.19  done
    7.20  
    7.21  lemma evaln_abrupt: 
    7.22   "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
    7.23 -  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
    7.24 +  w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))"
    7.25  apply auto
    7.26  apply (frule evaln_abrupt_lemma, auto)+
    7.27  done
    7.28 @@ -365,13 +365,13 @@
    7.29      | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
    7.30  *}
    7.31  
    7.32 -lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
    7.33 +lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
    7.34  apply (case_tac "s", case_tac "a = None")
    7.35  by (auto intro!: evaln.Lit)
    7.36  
    7.37  lemma CondI: 
    7.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> 
    7.39 -  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
    7.40 +  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2"
    7.41  apply (case_tac "s", case_tac "a = None")
    7.42  by (auto intro!: evaln.Cond)
    7.43  
    7.44 @@ -520,7 +520,7 @@
    7.45  proof (induct)
    7.46    case (Abrupt xc s t)
    7.47    obtain n where
    7.48 -    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
    7.49 +    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
    7.50      by (iprover intro: evaln.Abrupt)
    7.51    then show ?case ..
    7.52  next
     8.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 07 16:07:40 2008 +0200
     8.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 07 16:07:50 2008 +0200
     8.3 @@ -230,7 +230,7 @@
     8.4  lemma table_classes_Object [simp]: 
     8.5   "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
     8.6                                   ,methods=Object_mdecls
     8.7 -                                 ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
     8.8 +                                 ,init=Skip,super=undefined,superIfs=[]\<rparr>"
     8.9  apply (unfold table_classes_defs)
    8.10  apply (simp (no_asm) add:Object_def)
    8.11  done
    8.12 @@ -1246,13 +1246,13 @@
    8.13    "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    8.14    "arr_N"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
    8.15    "arr_a"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    8.16 -  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    8.17 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
    8.18 -                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)"
    8.19 -  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    8.20 -                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    8.21 +  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    8.22 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    8.23 +                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    8.24 +  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    8.25 +                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    8.26                       (Inl a\<mapsto>obj_a)
    8.27 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
    8.28 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    8.29    "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
    8.30    "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
    8.31    "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"
     9.1 --- a/src/HOL/Bali/State.thy	Tue Oct 07 16:07:40 2008 +0200
     9.2 +++ b/src/HOL/Bali/State.thy	Tue Oct 07 16:07:50 2008 +0200
     9.3 @@ -328,7 +328,7 @@
     9.4    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
     9.5  
     9.6  translations
     9.7 - "init_class_obj G C" == "init_obj G arbitrary (Inr C)"
     9.8 + "init_class_obj G C" == "init_obj G CONST undefined (Inr C)"
     9.9  
    9.10  lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
    9.11  apply (unfold gupd_def)
    10.1 --- a/src/HOL/Bali/Trans.thy	Tue Oct 07 16:07:40 2008 +0200
    10.2 +++ b/src/HOL/Bali/Trans.thy	Tue Oct 07 16:07:50 2008 +0200
    10.3 @@ -81,7 +81,7 @@
    10.4                    \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x;
    10.5                    \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 
    10.6                  \<Longrightarrow> 
    10.7 -                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit arbitrary\<rangle>,Some xc,s)"
    10.8 +                  G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)"
    10.9  
   10.10  | InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk>
   10.11               \<Longrightarrow> 
    11.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Oct 07 16:07:40 2008 +0200
    11.2 +++ b/src/HOL/Bali/TypeSafe.thy	Tue Oct 07 16:07:50 2008 +0200
    11.3 @@ -1738,7 +1738,7 @@
    11.4      from `(Some xc, s)\<Colon>\<preceq>(G,L)`
    11.5      show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
    11.6        (normal (Some xc, s) 
    11.7 -      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>arbitrary3 t\<Colon>\<preceq>T) \<and> 
    11.8 +      \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and> 
    11.9        (error_free (Some xc, s) = error_free (Some xc, s))"
   11.10        by simp
   11.11    next
   11.12 @@ -3850,7 +3850,7 @@
   11.13     and  abrupt: "\<And> s t abr L accC T A. 
   11.14                    \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
   11.15                     \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
   11.16 -                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (arbitrary3 t) (Some abr, s)"
   11.17 +                  \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
   11.18     and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
   11.19     and    expr: "\<And> e s0 s1 v L accC eT E.
   11.20                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
    12.1 --- a/src/HOL/Bali/WellForm.thy	Tue Oct 07 16:07:40 2008 +0200
    12.2 +++ b/src/HOL/Bali/WellForm.thy	Tue Oct 07 16:07:50 2008 +0200
    12.3 @@ -562,7 +562,7 @@
    12.4  lemma class_Object [simp]: 
    12.5  "wf_prog G \<Longrightarrow> 
    12.6    class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
    12.7 -                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>"
    12.8 +                                  init=Skip,super=undefined,superIfs=[]\<rparr>"
    12.9  apply (unfold wf_prog_def Let_def ObjectC_def)
   12.10  apply (fast dest!: map_of_SomeI)
   12.11  done
    13.1 --- a/src/HOL/Datatype.thy	Tue Oct 07 16:07:40 2008 +0200
    13.2 +++ b/src/HOL/Datatype.thy	Tue Oct 07 16:07:50 2008 +0200
    13.3 @@ -567,10 +567,10 @@
    13.4  
    13.5  constdefs
    13.6    Suml :: "('a => 'c) => 'a + 'b => 'c"
    13.7 -  "Suml == (%f. sum_case f arbitrary)"
    13.8 +  "Suml == (%f. sum_case f undefined)"
    13.9  
   13.10    Sumr :: "('b => 'c) => 'a + 'b => 'c"
   13.11 -  "Sumr == sum_case arbitrary"
   13.12 +  "Sumr == sum_case undefined"
   13.13  
   13.14  lemma Suml_inject: "Suml f = Suml g ==> f = g"
   13.15    by (unfold Suml_def) (erule sum_case_inject)
    14.1 --- a/src/HOL/HoareParallel/OG_Syntax.thy	Tue Oct 07 16:07:40 2008 +0200
    14.2 +++ b/src/HOL/HoareParallel/OG_Syntax.thy	Tue Oct 07 16:07:50 2008 +0200
    14.3 @@ -45,7 +45,7 @@
    14.4    "IF b THEN c1 ELSE c2 FI" \<rightharpoonup> "Cond .{b}. c1 c2"
    14.5    "IF b THEN c FI" \<rightleftharpoons> "IF b THEN c ELSE SKIP FI"
    14.6    "WHILE b INV i DO c OD" \<rightharpoonup> "While .{b}. i c"
    14.7 -  "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV arbitrary DO c OD"
    14.8 +  "WHILE b DO c OD" \<rightleftharpoons> "WHILE b INV CONST undefined DO c OD"
    14.9  
   14.10    "r SKIP" \<rightleftharpoons> "AnnBasic r id"
   14.11    "c_1;; c_2" \<rightleftharpoons> "AnnSeq c_1 c_2" 
    15.1 --- a/src/HOL/IMPP/Misc.thy	Tue Oct 07 16:07:40 2008 +0200
    15.2 +++ b/src/HOL/IMPP/Misc.thy	Tue Oct 07 16:07:50 2008 +0200
    15.3 @@ -11,7 +11,7 @@
    15.4  begin
    15.5  
    15.6  defs
    15.7 -  newlocs_def: "newlocs       == %x. arbitrary"
    15.8 +  newlocs_def: "newlocs       == %x. undefined"
    15.9    setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
   15.10    getlocs_def: "getlocs s     == case s of st g l => l"
   15.11     update_def: "update s vn v == case vn of
    16.1 --- a/src/HOL/Isar_examples/Hoare.thy	Tue Oct 07 16:07:40 2008 +0200
    16.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Tue Oct 07 16:07:50 2008 +0200
    16.3 @@ -232,7 +232,7 @@
    16.4    "\<acute>x := a"                 => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
    16.5    "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
    16.6    "WHILE b INV i DO c OD"   => "While .{b}. i c"
    16.7 -  "WHILE b DO c OD"         == "WHILE b INV arbitrary DO c OD"
    16.8 +  "WHILE b DO c OD"         == "WHILE b INV CONST undefined DO c OD"
    16.9  
   16.10  parse_translation {*
   16.11    let
   16.12 @@ -383,7 +383,7 @@
   16.13    by (rule while)
   16.14  
   16.15  lemma [intro?]:
   16.16 -    "|- (P Int b) c P ==> |- P (While b arbitrary c) (P Int -b)"
   16.17 +    "|- (P Int b) c P ==> |- P (While b undefined c) (P Int -b)"
   16.18    by (rule while)
   16.19  
   16.20  
    17.1 --- a/src/HOL/Library/FuncSet.thy	Tue Oct 07 16:07:40 2008 +0200
    17.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Oct 07 16:07:50 2008 +0200
    17.3 @@ -15,11 +15,11 @@
    17.4  
    17.5  definition
    17.6    extensional :: "'a set => ('a => 'b) set" where
    17.7 -  "extensional A = {f. \<forall>x. x~:A --> f x = arbitrary}"
    17.8 +  "extensional A = {f. \<forall>x. x~:A --> f x = undefined}"
    17.9  
   17.10  definition
   17.11    "restrict" :: "['a => 'b, 'a set] => ('a => 'b)" where
   17.12 -  "restrict f A = (%x. if x \<in> A then f x else arbitrary)"
   17.13 +  "restrict f A = (%x. if x \<in> A then f x else undefined)"
   17.14  
   17.15  abbreviation
   17.16    funcset :: "['a set, 'b set] => ('a => 'b) set"
   17.17 @@ -117,7 +117,7 @@
   17.18    by (simp add: Pi_def restrict_def)
   17.19  
   17.20  lemma restrict_apply [simp]:
   17.21 -    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else arbitrary)"
   17.22 +    "(\<lambda>y\<in>A. f y) x = (if x \<in> A then f x else undefined)"
   17.23    by (simp add: restrict_def)
   17.24  
   17.25  lemma restrict_ext:
   17.26 @@ -164,7 +164,7 @@
   17.27  
   17.28  subsection{*Extensionality*}
   17.29  
   17.30 -lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = arbitrary"
   17.31 +lemma extensional_arb: "[|f \<in> extensional A; x\<notin> A|] ==> f x = undefined"
   17.32    by (simp add: extensional_def)
   17.33  
   17.34  lemma restrict_extensional [simp]: "restrict f A \<in> extensional A"
    18.1 --- a/src/HOL/Library/Heap.thy	Tue Oct 07 16:07:40 2008 +0200
    18.2 +++ b/src/HOL/Library/Heap.thy	Tue Oct 07 16:07:50 2008 +0200
    18.3 @@ -115,7 +115,7 @@
    18.4    lim  :: addr
    18.5  
    18.6  definition empty :: heap where
    18.7 -  "empty = \<lparr>arrays = (\<lambda>_. arbitrary), refs = (\<lambda>_. arbitrary), lim = 0\<rparr>" -- "why arbitrary?"
    18.8 +  "empty = \<lparr>arrays = (\<lambda>_. undefined), refs = (\<lambda>_. undefined), lim = 0\<rparr>" -- "why undefined?"
    18.9  
   18.10  
   18.11  subsection {* Imperative references and arrays *}
    19.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Oct 07 16:07:40 2008 +0200
    19.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Tue Oct 07 16:07:50 2008 +0200
    19.3 @@ -926,7 +926,7 @@
    19.4    with oX_Addr oX_pos state' method ins stk' l_o l loc obj_ty mD no_xcp
    19.5    have state'_val:
    19.6      "state' =
    19.7 -     Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' arbitrary, 
    19.8 +     Norm (hp, ([], Addr ref # rev opTs @ replicate mxl' undefined, 
    19.9                  D'', (mn, pTs), 0) # (opTs @ Addr ref # stk', loc, C, sig, pc) # frs)"
   19.10      (is "state' = Norm (hp, ?f # ?f' # frs)")
   19.11      by (simp add: raise_system_xcpt_def)
   19.12 @@ -947,7 +947,7 @@
   19.13        (is "G \<turnstile> ?LT <=l LT0")
   19.14        by (simp add: wt_start_def sup_state_conv)
   19.15  
   19.16 -    have r: "approx_loc G hp (replicate mxl' arbitrary) (replicate mxl' Err)"
   19.17 +    have r: "approx_loc G hp (replicate mxl' undefined) (replicate mxl' Err)"
   19.18        by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
   19.19      
   19.20      from wfprog mD is_class_D
   19.21 @@ -963,7 +963,7 @@
   19.22      hence "approx_stk G hp (rev opTs) pTs" by (subst approx_stk_rev)
   19.23  
   19.24      with r a l_o l
   19.25 -    have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' arbitrary) ?LT"
   19.26 +    have "approx_loc G hp (Addr ref # rev opTs @ replicate mxl' undefined) ?LT"
   19.27        (is "approx_loc G hp ?lt ?LT")
   19.28        by (auto simp add: approx_loc_append approx_stk_def)
   19.29  
    20.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Oct 07 16:07:40 2008 +0200
    20.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Tue Oct 07 16:07:50 2008 +0200
    20.3 @@ -1138,7 +1138,7 @@
    20.4  apply (rule_tac ?instrs0.0 = "(compInitLvars (pns, lvars, blk, res) lvars)" in progression_transitive, rule HOL.refl)
    20.5  apply (rule_tac C=md in progression_lvar_init, assumption, assumption, assumption)
    20.6  apply (simp (no_asm_simp)) (* length pns = length pvs *)
    20.7 -apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) arbitrary) *)
    20.8 +apply (simp (no_asm_simp)) (* length lvars = length (replicate (length lvars) undefined) *)
    20.9  
   20.10  
   20.11         (* body statement *)
    21.1 --- a/src/HOL/MicroJava/J/Eval.thy	Tue Oct 07 16:07:40 2008 +0200
    21.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Tue Oct 07 16:07:50 2008 +0200
    21.3 @@ -45,7 +45,7 @@
    21.4  
    21.5    -- "evaluation of expressions"
    21.6  
    21.7 -  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>arbitrary-> (Some xc,s)"  -- "cf. 15.5"
    21.8 +  XcptE:"G\<turnstile>(Some xc,s) -e\<succ>undefined-> (Some xc,s)"  -- "cf. 15.5"
    21.9  
   21.10    -- "cf. 15.8.1"
   21.11  | NewC: "[| h = heap s; (a,x) = new_Addr h;
   21.12 @@ -98,7 +98,7 @@
   21.13    -- "evaluation of expression lists"
   21.14  
   21.15    -- "cf. 15.5"
   21.16 -| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]arbitrary-> (Some xc,s)"
   21.17 +| XcptEs:"G\<turnstile>(Some xc,s) -e[\<succ>]undefined-> (Some xc,s)"
   21.18  
   21.19    -- "cf. 15.11.???"
   21.20  | Nil:  "G\<turnstile>Norm s0 -[][\<succ>][]-> Norm s0"
    22.1 --- a/src/HOL/MicroJava/J/Example.thy	Tue Oct 07 16:07:40 2008 +0200
    22.2 +++ b/src/HOL/MicroJava/J/Example.thy	Tue Oct 07 16:07:50 2008 +0200
    22.3 @@ -137,7 +137,7 @@
    22.4  done
    22.5  declare map_of_Cons [simp del] -- "sic!"
    22.6  
    22.7 -lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])"
    22.8 +lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])"
    22.9  apply (unfold ObjectC_def class_def)
   22.10  apply (simp (no_asm))
   22.11  done
    23.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Tue Oct 07 16:07:40 2008 +0200
    23.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Oct 07 16:07:50 2008 +0200
    23.3 @@ -5,7 +5,9 @@
    23.4  
    23.5  header {* \isaheader{Example for generating executable code from Java semantics} *}
    23.6  
    23.7 -theory JListExample imports Eval SystemClasses begin
    23.8 +theory JListExample
    23.9 +imports Eval SystemClasses
   23.10 +begin
   23.11  
   23.12  ML {* Syntax.ambiguity_level := 100000 *}
   23.13  
   23.14 @@ -72,9 +74,9 @@
   23.15    in nr 0 end;
   23.16  *}
   23.17  
   23.18 -  "arbitrary" ("(raise Match)")
   23.19 -  "arbitrary :: val" ("{* Unit *}")
   23.20 -  "arbitrary :: cname" ("\"\"")
   23.21 +  "undefined" ("(raise Match)")
   23.22 +  "undefined :: val" ("{* Unit *}")
   23.23 +  "undefined :: cname" ("\"\"")
   23.24  
   23.25    "Object" ("\"Object\"")
   23.26    "list_name" ("\"list\"")
    24.1 --- a/src/HOL/MicroJava/J/SystemClasses.thy	Tue Oct 07 16:07:40 2008 +0200
    24.2 +++ b/src/HOL/MicroJava/J/SystemClasses.thy	Tue Oct 07 16:07:50 2008 +0200
    24.3 @@ -15,7 +15,7 @@
    24.4  
    24.5  constdefs
    24.6    ObjectC :: "'c cdecl"
    24.7 -  "ObjectC \<equiv> (Object, (arbitrary,[],[]))"
    24.8 +  "ObjectC \<equiv> (Object, (undefined,[],[]))"
    24.9  
   24.10    NullPointerC :: "'c cdecl"
   24.11    "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))"
    25.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 07 16:07:40 2008 +0200
    25.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Tue Oct 07 16:07:50 2008 +0200
    25.3 @@ -56,7 +56,7 @@
    25.4      (cname \<Rightarrow> fdecl list \<Rightarrow> 'c mdecl list \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
    25.5    "class_rec G == wfrec {(C, D). (subcls1 G)^--1 C D}
    25.6      (\<lambda>r C t f. case class G C of
    25.7 -         None \<Rightarrow> arbitrary
    25.8 +         None \<Rightarrow> undefined
    25.9         | Some (D,fs,ms) \<Rightarrow> 
   25.10             f C fs ms (if C = Object then t else r D t f))"
   25.11  
   25.12 @@ -68,10 +68,10 @@
   25.13  definition
   25.14    "wf_class G = wfP ((subcls1 G)^--1)"
   25.15  
   25.16 -lemma class_rec_func [code func]:
   25.17 +lemma class_rec_func (*[code func]*):
   25.18    "class_rec G C t f = (if wf_class G then
   25.19      (case class G C
   25.20 -      of None \<Rightarrow> arbitrary
   25.21 +      of None \<Rightarrow> undefined
   25.22         | Some (D, fs, ms) \<Rightarrow> f C fs ms (if C = Object then t else class_rec G D t f))
   25.23      else class_rec G C t f)"
   25.24  proof (cases "wf_class G")
    26.1 --- a/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Oct 07 16:07:40 2008 +0200
    26.2 +++ b/src/HOL/MicroJava/JVM/JVMExec.thy	Tue Oct 07 16:07:50 2008 +0200
    26.3 @@ -46,6 +46,6 @@
    26.4    start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state"
    26.5    "start_state G C m \<equiv>
    26.6    let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in
    26.7 -    (None, start_heap G, [([], Null # replicate mxl arbitrary, C, (m,[]), 0)])"
    26.8 +    (None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])"
    26.9  
   26.10  end
    27.1 --- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Oct 07 16:07:40 2008 +0200
    27.2 +++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy	Tue Oct 07 16:07:50 2008 +0200
    27.3 @@ -66,7 +66,7 @@
    27.4         dynT = fst(the(hp(the_Addr oref)));
    27.5         (dc,mh,mxs,mxl,c)= the (method (G,dynT) (mn,ps));
    27.6         frs' = if xp'=None then 
    27.7 -                [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)]
    27.8 +                [([],rev argsoref@replicate mxl undefined,dc,(mn,ps),0)]
    27.9                else []
   27.10     in 
   27.11        (xp', hp, frs'@(stk, vars, Cl, sig, pc)#frs))" 
    28.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Oct 07 16:07:40 2008 +0200
    28.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Oct 07 16:07:50 2008 +0200
    28.3 @@ -101,9 +101,9 @@
    28.4    in nr 0 end;
    28.5  *}
    28.6  
    28.7 -  "arbitrary" ("(raise Match)")
    28.8 -  "arbitrary :: val" ("{* Unit *}")
    28.9 -  "arbitrary :: cname" ("{* Object *}")
   28.10 +  "undefined" ("(raise Match)")
   28.11 +  "undefined :: val" ("{* Unit *}")
   28.12 +  "undefined :: cname" ("{* Object *}")
   28.13  
   28.14    "list_nam" ("\"list\"")
   28.15    "test_nam" ("\"test\"")
    29.1 --- a/src/HOL/NanoJava/TypeRel.thy	Tue Oct 07 16:07:40 2008 +0200
    29.2 +++ b/src/HOL/NanoJava/TypeRel.thy	Tue Oct 07 16:07:50 2008 +0200
    29.3 @@ -104,10 +104,10 @@
    29.4  consts class_rec ::"cname \<Rightarrow> (class \<Rightarrow> ('a \<times> 'b) list) \<Rightarrow> ('a \<rightharpoonup> 'b)"
    29.5  
    29.6  recdef (permissive) class_rec "subcls1\<inverse>"
    29.7 -      "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> arbitrary 
    29.8 +      "class_rec C = (\<lambda>f. case class C of None   \<Rightarrow> undefined 
    29.9                                          | Some m \<Rightarrow> if wf (subcls1\<inverse>) 
   29.10         then (if C=Object then empty else class_rec (super m) f) ++ map_of (f m)
   29.11 -       else arbitrary)"
   29.12 +       else undefined)"
   29.13  (hints intro: subcls1I)
   29.14  
   29.15  lemma class_rec: "\<lbrakk>class C = Some m;  ws_prog\<rbrakk> \<Longrightarrow>
    30.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 07 16:07:40 2008 +0200
    30.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Oct 07 16:07:50 2008 +0200
    30.3 @@ -142,7 +142,7 @@
    30.4        (case AList.lookup (op =) eqns cname of
    30.5            NONE => (warning ("No equation for constructor " ^ quote cname ^
    30.6              "\nin definition of function " ^ quote fname);
    30.7 -              (fnameTs', fnss', (Const ("arbitrary", dummyT))::fns))
    30.8 +              (fnameTs', fnss', (Const (@{const_name undefined}, dummyT))::fns))
    30.9          | SOME (ls, cargs', rs, rhs, eq) =>
   30.10              let
   30.11                val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
   30.12 @@ -183,7 +183,7 @@
   30.13    case AList.lookup (op =) fns i of
   30.14       NONE =>
   30.15         let
   30.16 -         val dummy_fns = map (fn (_, cargs) => Const ("arbitrary",
   30.17 +         val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
   30.18             replicate ((length cargs) + (length (List.filter is_rec_type cargs)))
   30.19               dummyT ---> HOLogic.unitT)) constrs;
   30.20           val _ = warning ("No function definition for datatype " ^ quote tname)
    31.1 --- a/src/HOL/Sum_Type.thy	Tue Oct 07 16:07:40 2008 +0200
    31.2 +++ b/src/HOL/Sum_Type.thy	Tue Oct 07 16:07:50 2008 +0200
    31.3 @@ -126,8 +126,8 @@
    31.4    (if (\<exists>!y. x = Inl y) 
    31.5    then f (THE y. x = Inl y) 
    31.6    else g (THE y. x = Inr y))"
    31.7 -definition "Projl x = sum_case id arbitrary x"
    31.8 -definition "Projr x = sum_case arbitrary id x"
    31.9 +definition "Projl x = sum_case id undefined x"
   31.10 +definition "Projr x = sum_case undefined id x"
   31.11  
   31.12  lemma sum_cases[simp]: 
   31.13    "sum_case f g (Inl x) = f x"
    32.1 --- a/src/HOL/TLA/Memory/RPCParameters.thy	Tue Oct 07 16:07:40 2008 +0200
    32.2 +++ b/src/HOL/TLA/Memory/RPCParameters.thy	Tue Oct 07 16:07:50 2008 +0200
    32.3 @@ -44,7 +44,7 @@
    32.4  		                  | (othercall v) => False"
    32.5    RPCRelayArg_def:   "RPCRelayArg ra ==
    32.6  		         case ra of (memcall m) => m
    32.7 -		                  | (othercall v) => arbitrary"
    32.8 +		                  | (othercall v) => undefined"
    32.9  
   32.10  lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF
   32.11    NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric]
    33.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 07 16:07:40 2008 +0200
    33.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Tue Oct 07 16:07:50 2008 +0200
    33.3 @@ -291,7 +291,7 @@
    33.4        let
    33.5          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    33.6          val Ts' = map mk_dummyT (List.filter is_rec_type cargs)
    33.7 -      in Const ("arbitrary", Ts @ Ts' ---> T')
    33.8 +      in Const (@{const_name undefined}, Ts @ Ts' ---> T')
    33.9        end) constrs) descr';
   33.10  
   33.11      val case_names = map (fn s => Sign.full_name thy1 (s ^ "_case")) new_type_names;
    34.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 07 16:07:40 2008 +0200
    34.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Oct 07 16:07:50 2008 +0200
    34.3 @@ -125,7 +125,7 @@
    34.4        {left = fn t => In0 $ t,
    34.5          right = fn t => In1 $ t,
    34.6          init =
    34.7 -          if ts = [] then Const ("arbitrary", Univ_elT)
    34.8 +          if ts = [] then Const (@{const_name undefined}, Univ_elT)
    34.9            else foldr1 (HOLogic.mk_binop Scons_name) ts};
   34.10  
   34.11      (* function spaces *)
    35.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 07 16:07:40 2008 +0200
    35.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 07 16:07:50 2008 +0200
    35.3 @@ -189,7 +189,7 @@
    35.4      FundefConfig {sequential=sequential, default=default, domintros=domintros,tailrec=true}
    35.5  
    35.6  val default_config =
    35.7 -  FundefConfig { sequential=false, default="%x. arbitrary", domintros=false, tailrec=false }
    35.8 +  FundefConfig { sequential=false, default="%x. undefined" (*FIXME dynamic scoping*), domintros=false, tailrec=false }
    35.9  
   35.10  
   35.11  (* Analyzing function equations *)
    36.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Oct 07 16:07:40 2008 +0200
    36.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Tue Oct 07 16:07:50 2008 +0200
    36.3 @@ -298,7 +298,7 @@
    36.4      #> Context.theory_map (FundefCommon.set_preproc sequential_preproc)
    36.5  
    36.6  
    36.7 -val fun_config = FundefConfig { sequential=true, default="%x. arbitrary" (* FIXME dynamic scoping *), 
    36.8 +val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), 
    36.9                                  domintros=false, tailrec=false }
   36.10  
   36.11  
    37.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Oct 07 16:07:40 2008 +0200
    37.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Oct 07 16:07:50 2008 +0200
    37.3 @@ -212,7 +212,7 @@
    37.4        else apsnd (cons p) (find_arg T x ps);
    37.5  
    37.6  fun make_args Ts xs =
    37.7 -  map (fn (T, (NONE, ())) => Const ("arbitrary", T) | (_, (SOME t, ())) => t)
    37.8 +  map (fn (T, (NONE, ())) => Const (@{const_name undefined}, T) | (_, (SOME t, ())) => t)
    37.9      (fold (fn (t, T) => snd o find_arg T t) xs (map (rpair (NONE, ())) Ts));
   37.10  
   37.11  fun make_args' Ts xs Us =
    38.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 07 16:07:40 2008 +0200
    38.2 +++ b/src/HOL/Tools/refute.ML	Tue Oct 07 16:07:50 2008 +0200
    38.3 @@ -681,7 +681,7 @@
    38.4          Const ("True", _)               => t
    38.5        | (* redundant, since 'False' is also an IDT constructor *)
    38.6          Const ("False", _)              => t
    38.7 -      | Const ("arbitrary", _)          => t
    38.8 +      | Const (@{const_name undefined}, _)          => t
    38.9        | Const ("The", _)                => t
   38.10        | Const ("Hilbert_Choice.Eps", _) => t
   38.11        | Const ("All", _)                => t
   38.12 @@ -856,7 +856,7 @@
   38.13        | Const ("True", _)               => axs
   38.14        (* redundant, since 'False' is also an IDT constructor *)
   38.15        | Const ("False", _)              => axs
   38.16 -      | Const ("arbitrary", T)          => collect_type_axioms (axs, T)
   38.17 +      | Const (@{const_name undefined}, T)          => collect_type_axioms (axs, T)
   38.18        | Const ("The", T)                =>
   38.19          let
   38.20            val ax = specialize_type thy ("The", T)
   38.21 @@ -3202,23 +3202,23 @@
   38.22        end
   38.23      | Type ("prop", [])      =>
   38.24        (case index_from_interpretation intr of
   38.25 -        ~1 => SOME (HOLogic.mk_Trueprop (Const ("arbitrary", HOLogic.boolT)))
   38.26 +        ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
   38.27        | 0  => SOME (HOLogic.mk_Trueprop HOLogic.true_const)
   38.28        | 1  => SOME (HOLogic.mk_Trueprop HOLogic.false_const)
   38.29        | _  => raise REFUTE ("stlc_interpreter",
   38.30          "illegal interpretation for a propositional value"))
   38.31      | Type _  => if index_from_interpretation intr = (~1) then
   38.32 -        SOME (Const ("arbitrary", T))
   38.33 +        SOME (Const (@{const_name undefined}, T))
   38.34        else
   38.35          SOME (Const (string_of_typ T ^
   38.36            string_of_int (index_from_interpretation intr), T))
   38.37      | TFree _ => if index_from_interpretation intr = (~1) then
   38.38 -        SOME (Const ("arbitrary", T))
   38.39 +        SOME (Const (@{const_name undefined}, T))
   38.40        else
   38.41          SOME (Const (string_of_typ T ^
   38.42            string_of_int (index_from_interpretation intr), T))
   38.43      | TVar _  => if index_from_interpretation intr = (~1) then
   38.44 -        SOME (Const ("arbitrary", T))
   38.45 +        SOME (Const (@{const_name undefined}, T))
   38.46        else
   38.47          SOME (Const (string_of_typ T ^
   38.48            string_of_int (index_from_interpretation intr), T))
   38.49 @@ -3291,7 +3291,7 @@
   38.50                "interpretation is not a leaf"))
   38.51          in
   38.52            if element < 0 then
   38.53 -            SOME (Const ("arbitrary", Type (s, Ts)))
   38.54 +            SOME (Const (@{const_name undefined}, Type (s, Ts)))
   38.55            else let
   38.56              (* takes a datatype constructor, and if for some arguments this  *)
   38.57              (* constructor generates the datatype's element that is given by *)
    39.1 --- a/src/HOL/Wellfounded.thy	Tue Oct 07 16:07:40 2008 +0200
    39.2 +++ b/src/HOL/Wellfounded.thy	Tue Oct 07 16:07:50 2008 +0200
    39.3 @@ -33,7 +33,7 @@
    39.4    "acyclic r == !x. (x,x) ~: r^+"
    39.5  
    39.6    cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    39.7 -  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
    39.8 +  "cut f r x == (%y. if (y,x):r then f y else undefined)"
    39.9  
   39.10    adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
   39.11    "adm_wf R F == ALL f g x.
    40.1 --- a/src/HOL/Word/WordDefinition.thy	Tue Oct 07 16:07:40 2008 +0200
    40.2 +++ b/src/HOL/Word/WordDefinition.thy	Tue Oct 07 16:07:50 2008 +0200
    40.3 @@ -66,9 +66,9 @@
    40.4  
    40.5    -- "whether a cast (or other) function is to a longer or shorter length"
    40.6    source_size :: "('a :: len0 word => 'b) => nat"
    40.7 -  "source_size c == let arb = arbitrary ; x = c arb in size arb"  
    40.8 +  "source_size c == let arb = undefined ; x = c arb in size arb"  
    40.9    target_size :: "('a => 'b :: len0 word) => nat"
   40.10 -  "target_size c == size (c arbitrary)"
   40.11 +  "target_size c == size (c undefined)"
   40.12    is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
   40.13    "is_up c == source_size c <= target_size c"
   40.14    is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
    41.1 --- a/src/HOL/ex/Quickcheck.thy	Tue Oct 07 16:07:40 2008 +0200
    41.2 +++ b/src/HOL/ex/Quickcheck.thy	Tue Oct 07 16:07:50 2008 +0200
    41.3 @@ -48,10 +48,10 @@
    41.4  
    41.5  lemma random'_if:
    41.6    fixes random' :: "index \<Rightarrow> index \<Rightarrow> seed \<Rightarrow> ('a \<times> (unit \<Rightarrow> term)) \<times> seed"
    41.7 -  assumes "random' 0 j = undefined"
    41.8 +  assumes "random' 0 j = (\<lambda>s. undefined)"
    41.9      and "\<And>i. random' (Suc_index i) j = rhs2 i"
   41.10    shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)"
   41.11 -  by (cases i rule: index.exhaust) (insert assms, simp_all add: undefined_fun)
   41.12 +  by (cases i rule: index.exhaust) (insert assms, simp_all)
   41.13  
   41.14  setup {*
   41.15  let
   41.16 @@ -115,7 +115,8 @@
   41.17          |> (map o apsnd) (List.partition fst)
   41.18          |> map (mk_clauses thy this_ty)
   41.19        val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [
   41.20 -          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Const (@{const_name undefined}, this_ty')),
   41.21 +          (random' $ @{term "0\<Colon>index"} $ @{term "j\<Colon>index"}, Abs ("s", @{typ seed},
   41.22 +            Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ seed})))),
   41.23            (random' $ @{term "Suc_index i"} $ @{term "j\<Colon>index"}, rhs)
   41.24          ]))) rhss;
   41.25      in eqss end;
   41.26 @@ -198,7 +199,7 @@
   41.27      (seed : Random_Engine.seed) =
   41.28    let
   41.29      val (seed', seed'') = random_split seed;
   41.30 -    val state = ref (seed', [], Const (@{const_name arbitrary}, T1 --> T2));
   41.31 +    val state = ref (seed', [], Const (@{const_name undefined}, T1 --> T2));
   41.32      val fun_upd = Const (@{const_name fun_upd},
   41.33        (T1 --> T2) --> T1 --> T2 --> T1 --> T2);
   41.34      fun random_fun' x =
    42.1 --- a/src/HOL/ex/Refute_Examples.thy	Tue Oct 07 16:07:40 2008 +0200
    42.2 +++ b/src/HOL/ex/Refute_Examples.thy	Tue Oct 07 16:07:50 2008 +0200
    42.3 @@ -421,21 +421,21 @@
    42.4  
    42.5  (*****************************************************************************)
    42.6  
    42.7 -subsubsection {* arbitrary *}
    42.8 +subsubsection {* undefined *}
    42.9  
   42.10 -lemma "arbitrary"
   42.11 +lemma "undefined"
   42.12    refute
   42.13  oops
   42.14  
   42.15 -lemma "P arbitrary"
   42.16 +lemma "P undefined"
   42.17    refute
   42.18  oops
   42.19  
   42.20 -lemma "arbitrary x"
   42.21 +lemma "undefined x"
   42.22    refute
   42.23  oops
   42.24  
   42.25 -lemma "arbitrary arbitrary"
   42.26 +lemma "undefined undefined"
   42.27    refute
   42.28  oops
   42.29  
   42.30 @@ -494,7 +494,7 @@
   42.31  
   42.32  text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
   42.33  
   42.34 -typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
   42.35 +typedef 'a myTdef = "insert (undefined::'a) (undefined::'a set)"
   42.36    by auto
   42.37  
   42.38  lemma "(x::'a myTdef) = y"
   42.39 @@ -1326,7 +1326,7 @@
   42.40  
   42.41  inductive_set arbitrarySet :: "'a set"
   42.42  where
   42.43 -  "arbitrary : arbitrarySet"
   42.44 +  "undefined : arbitrarySet"
   42.45  
   42.46  lemma "x : arbitrarySet"
   42.47    refute
   42.48 @@ -1360,7 +1360,7 @@
   42.49    a_even :: "'a set"
   42.50    and a_odd :: "'a set"
   42.51  where
   42.52 -  "arbitrary : a_even"
   42.53 +  "undefined : a_even"
   42.54  | "x : a_even \<Longrightarrow> f x : a_odd"
   42.55  | "x : a_odd \<Longrightarrow> f x : a_even"
   42.56  
    43.1 --- a/src/HOLCF/FOCUS/Fstreams.thy	Tue Oct 07 16:07:40 2008 +0200
    43.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Oct 07 16:07:50 2008 +0200
    43.3 @@ -26,7 +26,7 @@
    43.4  
    43.5  definition
    43.6    jth           :: "nat => 'a fstream => 'a" where
    43.7 -  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary)"
    43.8 +  "jth = (%n s. if Fin n < #s then THE a. i_th n s = Def a else undefined)"
    43.9  
   43.10  definition
   43.11    first         :: "'a fstream => 'a" where
   43.12 @@ -34,8 +34,7 @@
   43.13  
   43.14  definition
   43.15    last          :: "'a fstream => 'a" where
   43.16 -  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
   43.17 -              | Infty => arbitrary)"
   43.18 +  "last = (%s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else undefined))"
   43.19  
   43.20  
   43.21  abbreviation
   43.22 @@ -92,19 +91,19 @@
   43.23  lemma last_fsingleton[simp]: "last (<a>) = a"
   43.24  by (simp add: last_def)
   43.25  
   43.26 -lemma first_UU[simp]: "first UU = arbitrary"
   43.27 +lemma first_UU[simp]: "first UU = undefined"
   43.28  by (simp add: first_def jth_def)
   43.29  
   43.30 -lemma last_UU[simp]:"last UU = arbitrary"
   43.31 +lemma last_UU[simp]:"last UU = undefined"
   43.32  by (simp add: last_def jth_def inat_defs)
   43.33  
   43.34 -lemma last_infinite[simp]:"#s = Infty ==> last s = arbitrary"
   43.35 +lemma last_infinite[simp]:"#s = Infty ==> last s = undefined"
   43.36  by (simp add: last_def)
   43.37  
   43.38 -lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = arbitrary"
   43.39 +lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = undefined"
   43.40  by (simp add: jth_def inat_defs split:inat_splits, auto)
   43.41  
   43.42 -lemma jth_UU[simp]:"jth n UU = arbitrary" 
   43.43 +lemma jth_UU[simp]:"jth n UU = undefined" 
   43.44  by (simp add: jth_def)
   43.45  
   43.46  lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
    44.1 --- a/src/HOLCF/IOA/meta_theory/TL.thy	Tue Oct 07 16:07:40 2008 +0200
    44.2 +++ b/src/HOLCF/IOA/meta_theory/TL.thy	Tue Oct 07 16:07:50 2008 +0200
    44.3 @@ -38,9 +38,7 @@
    44.4  defs
    44.5  
    44.6  unlift_def:
    44.7 -  "unlift x == (case x of
    44.8 -                 UU   => arbitrary
    44.9 -               | Def y   => y)"
   44.10 +  "unlift x == (case x of Def y   => y)"
   44.11  
   44.12  (* this means that for nil and UU the effect is unpredictable *)
   44.13  Init_def: