--- a/src/HOL/Bali/Decl.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/Decl.thy Tue Mar 02 12:26:50 2010 +0100
@@ -763,51 +763,57 @@
section "general recursion operators for the interface and class hiearchies"
-consts
- iface_rec :: "prog \<times> qtname \<Rightarrow> \<spacespace> (qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
- class_rec :: "prog \<times> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
-
-recdef iface_rec "same_fst ws_prog (\<lambda>G. (subint1 G)^-1)"
-"iface_rec (G,I) =
- (\<lambda>f. case iface G I of
+function
+ iface_rec :: "prog \<Rightarrow> qtname \<Rightarrow> \<spacespace>(qtname \<Rightarrow> iface \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+[simp del]: "iface_rec G I f =
+ (case iface G I of
None \<Rightarrow> undefined
| Some i \<Rightarrow> if ws_prog G
then f I i
- ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))
+ ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))
else undefined)"
-(hints recdef_wf: wf_subint1 intro: subint1I)
-declare iface_rec.simps [simp del]
+by auto
+termination
+by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subint1 G)^-1)) (%(x,y,z). (x,y))")
+ (auto simp: wf_subint1 subint1I wf_same_fst)
lemma iface_rec:
"\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>
- iface_rec (G,I) f = f I i ((\<lambda>J. iface_rec (G,J) f)`set (isuperIfs i))"
+ iface_rec G I f = f I i ((\<lambda>J. iface_rec G J f)`set (isuperIfs i))"
apply (subst iface_rec.simps)
apply simp
done
-recdef class_rec "same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)"
-"class_rec(G,C) =
- (\<lambda>t f. case class G C of
+
+function
+ class_rec :: "prog \<Rightarrow> qtname \<Rightarrow> 'a \<Rightarrow> (qtname \<Rightarrow> class \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
+where
+[simp del]: "class_rec G C t f =
+ (case class G C of
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 class_rec G (super c) t f)
else undefined)"
-(hints recdef_wf: wf_subcls1 intro: subcls1I)
-declare class_rec.simps [simp del]
+
+by auto
+termination
+by (relation "inv_image (same_fst ws_prog (\<lambda>G. (subcls1 G)^-1)) (%(x,y,z,w). (x,y))")
+ (auto simp: wf_subcls1 subcls1I wf_same_fst)
lemma class_rec: "\<lbrakk>class G C = Some c; ws_prog G\<rbrakk> \<Longrightarrow>
- class_rec (G,C) t f =
- f C c (if C = Object then t else class_rec (G,super c) t f)"
-apply (rule class_rec.simps [THEN trans [THEN fun_cong [THEN fun_cong]]])
+ class_rec G C t f =
+ f C c (if C = Object then t else class_rec G (super c) t f)"
+apply (subst class_rec.simps)
apply simp
done
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
--{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
"imethds G I
- \<equiv> iface_rec (G,I)
+ \<equiv> iface_rec G I
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
--- a/src/HOL/Bali/DeclConcepts.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Mar 02 12:26:50 2010 +0100
@@ -1381,7 +1381,7 @@
definition imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I
- \<equiv> iface_rec (G,I)
+ \<equiv> iface_rec G I
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
@@ -1396,7 +1396,7 @@
definition methd :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> methd) table" where
"methd G C
- \<equiv> class_rec (G,C) empty
+ \<equiv> class_rec G C empty
(\<lambda>C c subcls_mthds.
filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
subcls_mthds
@@ -1429,7 +1429,7 @@
then (case methd G statC sig of
None \<Rightarrow> None
| Some statM
- \<Rightarrow> (class_rec (G,dynC) empty
+ \<Rightarrow> (class_rec G dynC empty
(\<lambda>C c subcls_mthds.
subcls_mthds
++
@@ -1481,7 +1481,7 @@
definition fields :: "prog \<Rightarrow> qtname \<Rightarrow> ((vname \<times> qtname) \<times> field) list" where
"fields G C
- \<equiv> class_rec (G,C) [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
+ \<equiv> class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)"
text {* @{term "fields G C"}
list of fields of a class, including all the fields of the superclasses
(private, inherited and hidden ones) not only the accessible ones
@@ -1805,7 +1805,7 @@
(\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
(methd G C)"
let "?class_rec C" =
- "(class_rec (G, C) empty
+ "(class_rec G C empty
(\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
from statM Subcls ws subclseq_dynC_statC
have dynmethd_dynC_def:
@@ -2270,7 +2270,7 @@
section "calculation of the superclasses of a class"
definition superclasses :: "prog \<Rightarrow> qtname \<Rightarrow> qtname set" where
- "superclasses G C \<equiv> class_rec (G,C) {}
+ "superclasses G C \<equiv> class_rec G C {}
(\<lambda> C c superclss. (if C=Object
then {}
else insert (super c) superclss))"
--- a/src/HOL/Bali/WellForm.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Bali/WellForm.thy Tue Mar 02 12:26:50 2010 +0100
@@ -730,13 +730,15 @@
\<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
proof -
assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
+
+ note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
have "wf_prog G \<longrightarrow>
(\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
\<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
- proof (rule iface_rec.induct,intro allI impI)
+ proof (induct G I rule: iface_rec_induct', intro allI impI)
fix G I i im
- assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
- \<longrightarrow> ?P G J"
+ assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i)
+ \<Longrightarrow> ?P G J"
assume wf: "wf_prog G" and if_I: "iface G I = Some i" and
im: "im \<in> imethds G I sig"
show "\<not>is_static im \<and> accmodi im = Public"
@@ -1345,14 +1347,16 @@
qed
qed
+lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
+
lemma declclass_widen[rule_format]:
"wf_prog G
\<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m
\<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
-proof (rule class_rec.induct,intro allI impI)
+proof (induct G C rule: class_rec_induct', intro allI impI)
fix G C c m
- assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c
- \<longrightarrow> ?P G (super c)"
+ assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object
+ \<Longrightarrow> ?P G (super c)"
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
m: "methd G C sig = Some m"
show "G\<turnstile>C\<preceq>\<^sub>C declclass m"
@@ -1976,27 +1980,6 @@
qed
qed
-(* Tactical version *)
-(*
-lemma declclassD[rule_format]:
- "wf_prog G \<longrightarrow>
- (\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow>
- class G (declclass m) = Some d
- \<longrightarrow> table_of (methods d) sig = Some (mthd m))"
-apply (rule class_rec.induct)
-apply (rule impI)
-apply (rule allI)+
-apply (rule impI)
-apply (case_tac "C=Object")
-apply (force simp add: methd_rec)
-
-apply (subst methd_rec)
-apply (blast dest: wf_ws_prog)+
-apply (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig")
-apply (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
-done
-*)
-
lemma dynmethd_Object:
assumes statM: "methd G Object sig = Some statM" and
private: "accmodi statM = Private" and
@@ -2355,9 +2338,9 @@
have "wf_prog G \<longrightarrow>
(\<forall> c m. class G C = Some c \<longrightarrow> methd G C sig = Some m
\<longrightarrow> methd G (declclass m) sig = Some m)" (is "?P G C")
- proof (rule class_rec.induct,intro allI impI)
+ proof (induct G C rule: class_rec_induct', intro allI impI)
fix G C c m
- assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow>
+ assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow>
?P G (super c)"
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
m: "methd G C sig = Some m"
--- a/src/HOL/Lambda/ParRed.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Lambda/ParRed.thy Tue Mar 02 12:26:50 2010 +0100
@@ -85,14 +85,14 @@
subsection {* Complete developments *}
-consts
+fun
"cd" :: "dB => dB"
-recdef "cd" "measure size"
+where
"cd (Var n) = Var n"
- "cd (Var n \<degree> t) = Var n \<degree> cd t"
- "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
- "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
- "cd (Abs s) = Abs (cd s)"
+| "cd (Var n \<degree> t) = Var n \<degree> cd t"
+| "cd ((s1 \<degree> s2) \<degree> t) = cd (s1 \<degree> s2) \<degree> cd t"
+| "cd (Abs u \<degree> t) = (cd u)[cd t/0]"
+| "cd (Abs s) = Abs (cd s)"
lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
apply (induct s arbitrary: t rule: cd.induct)
--- a/src/HOL/Library/Word.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Library/Word.thy Tue Mar 02 12:26:50 2010 +0100
@@ -311,11 +311,11 @@
lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
by (rule bit_list_induct [of _ w],simp_all)
-consts
+fun
nat_to_bv_helper :: "nat => bit list => bit list"
-recdef nat_to_bv_helper "measure (\<lambda>n. n)"
- "nat_to_bv_helper n = (%bs. (if n = 0 then bs
- else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
+where
+ "nat_to_bv_helper n bs = (if n = 0 then bs
+ else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs))"
definition
nat_to_bv :: "nat => bit list" where
--- a/src/HOL/MicroJava/BV/Effect.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy Tue Mar 02 12:26:50 2010 +0100
@@ -34,33 +34,34 @@
| "succs Throw pc = [pc]"
text "Effect of instruction on the state type:"
-consts
-eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
-recdef eff' "{}"
-"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
-"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
-"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)"
-"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)"
-"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)"
-"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)"
-"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)"
-"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)"
-"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)"
-"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)"
-"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)"
-"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)"
+fun eff' :: "instr \<times> jvm_prog \<times> state_type \<Rightarrow> state_type"
+where
+"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" |
+"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" |
+"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\<lambda>v. None) v) # ST, LT)" |
+"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" |
+"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
+"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" |
+"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
+"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" |
+"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" |
+"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" |
+"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" |
+"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" |
"eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT))
- = (PrimT Integer#ST,LT)"
-"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)"
-"eff' (Goto b, G, s) = s"
+ = (PrimT Integer#ST,LT)" |
+"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" |
+"eff' (Goto b, G, s) = s" |
-- "Return has no successor instruction in the same method"
-"eff' (Return, G, s) = s"
+"eff' (Return, G, s) = s" |
-- "Throw always terminates abruptly"
-"eff' (Throw, G, s) = s"
+"eff' (Throw, G, s) = s" |
"eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST
in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))"
+
+
primrec match_any :: "jvm_prog \<Rightarrow> p_count \<Rightarrow> exception_table \<Rightarrow> cname list" where
"match_any G pc [] = []"
| "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;
@@ -77,16 +78,16 @@
"match G X pc et = (if \<exists>e \<in> set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])"
by (induct et) auto
-consts
+fun
xcpt_names :: "instr \<times> jvm_prog \<times> p_count \<times> exception_table \<Rightarrow> cname list"
-recdef xcpt_names "{}"
+where
"xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et"
- "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et"
- "xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et"
- "xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et"
- "xcpt_names (Throw, G, pc, et) = match_any G pc et"
- "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"
- "xcpt_names (i, G, pc, et) = []"
+| "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et"
+| "xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et"
+| "xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et"
+| "xcpt_names (Throw, G, pc, et) = match_any G pc et"
+| "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"
+| "xcpt_names (i, G, pc, et) = []"
definition xcpt_eff :: "instr \<Rightarrow> jvm_prog \<Rightarrow> p_count \<Rightarrow> state_type option \<Rightarrow> exception_table \<Rightarrow> succ_type" where
@@ -118,53 +119,53 @@
text "Conditions under which eff is applicable:"
-consts
+
+fun
app' :: "instr \<times> jvm_prog \<times> p_count \<times> nat \<times> ty \<times> state_type \<Rightarrow> bool"
-
-recdef app' "{}"
+where
"app' (Load idx, G, pc, maxs, rT, s) =
- (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)"
+ (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)" |
"app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) =
- (idx < length LT)"
+ (idx < length LT)" |
"app' (LitPush v, G, pc, maxs, rT, s) =
- (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)"
+ (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)" |
"app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) =
(is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
- G \<turnstile> oT \<preceq> (Class C))"
+ G \<turnstile> oT \<preceq> (Class C))" |
"app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) =
(is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
- G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))"
+ G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
"app' (New C, G, pc, maxs, rT, s) =
- (is_class G C \<and> length (fst s) < maxs)"
+ (is_class G C \<and> length (fst s) < maxs)" |
"app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) =
- (is_class G C)"
+ (is_class G C)" |
"app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) =
- True"
+ True" |
"app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) =
- (1+length ST < maxs)"
+ (1+length ST < maxs)" |
"app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =
- (2+length ST < maxs)"
+ (2+length ST < maxs)" |
"app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) =
- (3+length ST < maxs)"
+ (3+length ST < maxs)" |
"app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =
- True"
+ True" |
"app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =
- True"
+ True" |
"app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) =
- (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))"
+ (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))" |
"app' (Goto b, G, pc, maxs, rT, s) =
- (0 \<le> int pc + b)"
+ (0 \<le> int pc + b)" |
"app' (Return, G, pc, maxs, rT, (T#ST,LT)) =
- (G \<turnstile> T \<preceq> rT)"
+ (G \<turnstile> T \<preceq> rT)" |
"app' (Throw, G, pc, maxs, rT, (T#ST,LT)) =
- isRefT T"
+ isRefT T" |
"app' (Invoke C mn fpTs, G, pc, maxs, rT, s) =
(length fpTs < length (fst s) \<and>
(let apTs = rev (take (length fpTs) (fst s));
X = hd (drop (length fpTs) (fst s))
in
G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
- list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))"
+ list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |
"app' (i,G, pc,maxs,rT,s) = False"
@@ -208,7 +209,7 @@
qed auto
lemma 2: "\<not>(2 < length a) \<Longrightarrow> a = [] \<or> (\<exists> l. a = [l]) \<or> (\<exists> l l'. a = [l,l'])"
-proof -;
+proof -
assume "\<not>(2 < length a)"
hence "length a < (Suc (Suc (Suc 0)))" by simp
hence * : "length a = 0 \<or> length a = Suc 0 \<or> length a = Suc (Suc 0)"
@@ -268,7 +269,7 @@
"(app (Checkcast C) G maxs rT pc et (Some s)) =
(\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
(\<forall>x \<in> set (match G ClassCast pc et). is_class G x))"
- by (cases s, cases "fst s", simp add: app_def) (cases "hd (fst s)", auto)
+ by (cases s, cases "fst s", simp) (cases "hd (fst s)", auto)
lemma appPop[simp]:
"(app Pop G maxs rT pc et (Some s)) = (\<exists>ts ST LT. s = (ts#ST,LT))"
@@ -359,7 +360,7 @@
assume app: "?app (a,b)"
hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \<and>
length fpTs < length a" (is "?a \<and> ?l")
- by (auto simp add: app_def)
+ by auto
hence "?a \<and> 0 < length (drop (length fpTs) a)" (is "?a \<and> ?l")
by auto
hence "?a \<and> ?l \<and> length (rev (take (length fpTs) a)) = length fpTs"
@@ -374,7 +375,7 @@
hence "\<exists>apTs X ST. a = rev apTs @ X # ST \<and> length apTs = length fpTs"
by blast
with app
- show ?thesis by (unfold app_def, clarsimp) blast
+ show ?thesis by clarsimp blast
qed
with Pair
have "?app s \<Longrightarrow> ?P s" by (simp only:)
--- a/src/HOL/MicroJava/JVM/JVMExec.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Tue Mar 02 12:26:50 2010 +0100
@@ -8,21 +8,19 @@
theory JVMExec imports JVMExecInstr JVMExceptions begin
-consts
+fun
exec :: "jvm_prog \<times> jvm_state => jvm_state option"
-
-
--- "exec is not recursive. recdef is just used for pattern matching"
-recdef exec "{}"
+-- "exec is not recursive. fun is just used for pattern matching"
+where
"exec (G, xp, hp, []) = None"
- "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
+| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
(let
i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc;
(xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs
in Some (find_handler G xcpt' hp' frs'))"
- "exec (G, Some xp, hp, frs) = None"
+| "exec (G, Some xp, hp, frs) = None"
definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Tue Mar 02 12:26:50 2010 +0100
@@ -25,20 +25,18 @@
| insert: "A \<in> RsetR m ==> zgcd a m = 1 ==>
\<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m"
-consts
- BnorRset :: "int * int => int set"
-
-recdef BnorRset
- "measure ((\<lambda>(a, m). nat a) :: int * int => nat)"
- "BnorRset (a, m) =
+fun
+ BnorRset :: "int \<Rightarrow> int => int set"
+where
+ "BnorRset a m =
(if 0 < a then
- let na = BnorRset (a - 1, m)
+ let na = BnorRset (a - 1) m
in (if zgcd a m = 1 then insert a na else na)
else {})"
definition
norRRset :: "int => int set" where
- "norRRset m = BnorRset (m - 1, m)"
+ "norRRset m = BnorRset (m - 1) m"
definition
noXRRset :: "int => int => int set" where
@@ -74,28 +72,27 @@
lemma BnorRset_induct:
assumes "!!a m. P {} a m"
- and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m
- ==> P (BnorRset(a,m)) a m"
- shows "P (BnorRset(u,v)) u v"
+ and "!!a m :: int. 0 < a ==> P (BnorRset (a - 1) m) (a - 1) m
+ ==> P (BnorRset a m) a m"
+ shows "P (BnorRset u v) u v"
apply (rule BnorRset.induct)
- apply safe
- apply (case_tac [2] "0 < a")
- apply (rule_tac [2] prems)
+ apply (case_tac "0 < a")
+ apply (rule_tac assms)
apply simp_all
- apply (simp_all add: BnorRset.simps prems)
+ apply (simp_all add: BnorRset.simps assms)
done
-lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a"
+lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset a m \<longrightarrow> b \<le> a"
apply (induct a m rule: BnorRset_induct)
apply simp
apply (subst BnorRset.simps)
apply (unfold Let_def, auto)
done
-lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
+lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset a m"
by (auto dest: Bnor_mem_zle)
-lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b"
+lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset a m --> 0 < b"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -103,7 +100,7 @@
done
lemma Bnor_mem_if [rule_format]:
- "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)"
+ "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset a m"
apply (induct a m rule: BnorRset.induct, auto)
apply (subst BnorRset.simps)
defer
@@ -111,7 +108,7 @@
apply (unfold Let_def, auto)
done
-lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m"
+lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset a m \<in> RsetR m"
apply (induct a m rule: BnorRset_induct, simp)
apply (subst BnorRset.simps)
apply (unfold Let_def, auto)
@@ -124,7 +121,7 @@
apply (rule_tac [5] Bnor_mem_zg, auto)
done
-lemma Bnor_fin: "finite (BnorRset (a, m))"
+lemma Bnor_fin: "finite (BnorRset a m)"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -258,8 +255,8 @@
by (unfold inj_on_def, auto)
lemma Bnor_prod_power [rule_format]:
- "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) =
- \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))"
+ "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) =
+ \<Prod>(BnorRset a m) * x^card (BnorRset a m)"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (simplesubst BnorRset.simps) --{*multiple redexes*}
@@ -284,7 +281,7 @@
done
lemma Bnor_prod_zgcd [rule_format]:
- "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1"
+ "a < m --> zgcd (\<Prod>(BnorRset a m)) m = 1"
apply (induct a m rule: BnorRset_induct)
prefer 2
apply (subst BnorRset.simps)
@@ -299,13 +296,13 @@
apply (case_tac "x = 0")
apply (case_tac [2] "m = 1")
apply (rule_tac [3] iffD1)
- apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))"
+ apply (rule_tac [3] k = "\<Prod>(BnorRset (m - 1) m)"
in zcong_cancel2)
prefer 5
apply (subst Bnor_prod_power [symmetric])
apply (rule_tac [7] Bnor_prod_zgcd, simp_all)
apply (rule bijzcong_zcong_prod)
- apply (fold norRRset_def noXRRset_def)
+ apply (fold norRRset_def, fold noXRRset_def)
apply (subst RRset2norRR_eq_norR [symmetric])
apply (rule_tac [3] inj_func_bijR, auto)
apply (unfold zcongm_def)
@@ -319,12 +316,12 @@
done
lemma Bnor_prime:
- "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a"
+ "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset a p) = nat a"
apply (induct a p rule: BnorRset.induct)
apply (subst BnorRset.simps)
apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime)
- apply (subgoal_tac "finite (BnorRset (a - 1,m))")
- apply (subgoal_tac "a ~: BnorRset (a - 1,m)")
+ apply (subgoal_tac "finite (BnorRset (a - 1) m)")
+ apply (subgoal_tac "a ~: BnorRset (a - 1) m")
apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1)
apply (frule Bnor_mem_zle, arith)
apply (frule Bnor_fin)
--- a/src/HOL/Old_Number_Theory/IntFact.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/IntFact.thy Tue Mar 02 12:26:50 2010 +0100
@@ -14,14 +14,14 @@
\bigskip
*}
-consts
+fun
zfact :: "int => int"
- d22set :: "int => int set"
-
-recdef zfact "measure ((\<lambda>n. nat n) :: int => nat)"
+where
"zfact n = (if n \<le> 0 then 1 else n * zfact (n - 1))"
-recdef d22set "measure ((\<lambda>a. nat a) :: int => nat)"
+fun
+ d22set :: "int => int set"
+where
"d22set a = (if 1 < a then insert a (d22set (a - 1)) else {})"
@@ -38,12 +38,10 @@
and "!!a. 1 < (a::int) ==> P (d22set (a - 1)) (a - 1) ==> P (d22set a) a"
shows "P (d22set u) u"
apply (rule d22set.induct)
- apply safe
- prefer 2
- apply (case_tac "1 < a")
- apply (rule_tac prems)
- apply (simp_all (no_asm_simp))
- apply (simp_all (no_asm_simp) add: d22set.simps prems)
+ apply (case_tac "1 < a")
+ apply (rule_tac assms)
+ apply (simp_all (no_asm_simp))
+ apply (simp_all (no_asm_simp) add: d22set.simps assms)
done
lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> 1 < b"
@@ -66,7 +64,8 @@
lemma d22set_mem: "1 < b \<Longrightarrow> b \<le> a \<Longrightarrow> b \<in> d22set a"
apply (induct a rule: d22set.induct)
apply auto
- apply (simp_all add: d22set.simps)
+ apply (subst d22set.simps)
+ apply (case_tac "b < a", auto)
done
lemma d22set_fin: "finite (d22set a)"
@@ -81,8 +80,6 @@
lemma d22set_prod_zfact: "\<Prod>(d22set a) = zfact a"
apply (induct a rule: d22set.induct)
- apply safe
- apply (simp add: d22set.simps zfact.simps)
apply (subst d22set.simps)
apply (subst zfact.simps)
apply (case_tac "1 < a")
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Tue Mar 02 12:26:50 2010 +0100
@@ -19,17 +19,14 @@
subsection {* Definitions *}
-consts
- xzgcda :: "int * int * int * int * int * int * int * int => int * int * int"
-
-recdef xzgcda
- "measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r)
- :: int * int * int * int *int * int * int * int => nat)"
- "xzgcda (m, n, r', r, s', s, t', t) =
+fun
+ xzgcda :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int => (int * int * int)"
+where
+ "xzgcda m n r' r s' s t' t =
(if r \<le> 0 then (r', s', t')
- else xzgcda (m, n, r, r' mod r,
- s, s' - (r' div r) * s,
- t, t' - (r' div r) * t))"
+ else xzgcda m n r (r' mod r)
+ s (s' - (r' div r) * s)
+ t (t' - (r' div r) * t))"
definition
zprime :: "int \<Rightarrow> bool" where
@@ -37,7 +34,7 @@
definition
xzgcd :: "int => int => int * int * int" where
- "xzgcd m n = xzgcda (m, n, m, n, 1, 0, 0, 1)"
+ "xzgcd m n = xzgcda m n m n 1 0 0 1"
definition
zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") where
@@ -307,9 +304,8 @@
lemma xzgcd_correct_aux1:
"zgcd r' r = k --> 0 < r -->
- (\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))"
- apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
- z = s and aa = t' and ab = t in xzgcda.induct)
+ (\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn))"
+ apply (induct m n r' r s' s t' t rule: xzgcda.induct)
apply (subst zgcd_eq)
apply (subst xzgcda.simps, auto)
apply (case_tac "r' mod r = 0")
@@ -321,17 +317,16 @@
done
lemma xzgcd_correct_aux2:
- "(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) --> 0 < r -->
+ "(\<exists>sn tn. xzgcda m n r' r s' s t' t = (k, sn, tn)) --> 0 < r -->
zgcd r' r = k"
- apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
- z = s and aa = t' and ab = t in xzgcda.induct)
+ apply (induct m n r' r s' s t' t rule: xzgcda.induct)
apply (subst zgcd_eq)
apply (subst xzgcda.simps)
apply (auto simp add: linorder_not_le)
apply (case_tac "r' mod r = 0")
prefer 2
apply (frule_tac a = "r'" in pos_mod_sign, auto)
- apply (metis Pair_eq simps zle_refl)
+ apply (metis Pair_eq xzgcda.simps zle_refl)
done
lemma xzgcd_correct:
@@ -362,10 +357,9 @@
by (rule iffD2 [OF order_less_le conjI])
lemma xzgcda_linear [rule_format]:
- "0 < r --> xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) -->
+ "0 < r --> xzgcda m n r' r s' s t' t = (rn, sn, tn) -->
r' = s' * m + t' * n --> r = s * m + t * n --> rn = sn * m + tn * n"
- apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and
- z = s and aa = t' and ab = t in xzgcda.induct)
+ apply (induct m n r' r s' s t' t rule: xzgcda.induct)
apply (subst xzgcda.simps)
apply (simp (no_asm))
apply (rule impI)+
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 02 12:26:50 2010 +0100
@@ -17,14 +17,12 @@
inv :: "int => int => int" where
"inv p a = (a^(nat (p - 2))) mod p"
-consts
- wset :: "int * int => int set"
-
-recdef wset
- "measure ((\<lambda>(a, p). nat a) :: int * int => nat)"
- "wset (a, p) =
+fun
+ wset :: "int \<Rightarrow> int => int set"
+where
+ "wset a p =
(if 1 < a then
- let ws = wset (a - 1, p)
+ let ws = wset (a - 1) p
in (if a \<in> ws then ws else insert a (insert (inv p a) ws)) else {})"
@@ -163,35 +161,33 @@
lemma wset_induct:
assumes "!!a p. P {} a p"
and "!!a p. 1 < (a::int) \<Longrightarrow>
- P (wset (a - 1, p)) (a - 1) p ==> P (wset (a, p)) a p"
- shows "P (wset (u, v)) u v"
- apply (rule wset.induct, safe)
- prefer 2
- apply (case_tac "1 < a")
- apply (rule prems)
- apply simp_all
- apply (simp_all add: wset.simps prems)
+ P (wset (a - 1) p) (a - 1) p ==> P (wset a p) a p"
+ shows "P (wset u v) u v"
+ apply (rule wset.induct)
+ apply (case_tac "1 < a")
+ apply (rule assms)
+ apply (simp_all add: wset.simps assms)
done
lemma wset_mem_imp_or [rule_format]:
- "1 < a \<Longrightarrow> b \<notin> wset (a - 1, p)
- ==> b \<in> wset (a, p) --> b = a \<or> b = inv p a"
+ "1 < a \<Longrightarrow> b \<notin> wset (a - 1) p
+ ==> b \<in> wset a p --> b = a \<or> b = inv p a"
apply (subst wset.simps)
apply (unfold Let_def, simp)
done
-lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset (a, p)"
+lemma wset_mem_mem [simp]: "1 < a ==> a \<in> wset a p"
apply (subst wset.simps)
apply (unfold Let_def, simp)
done
-lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1, p) ==> b \<in> wset (a, p)"
+lemma wset_subset: "1 < a \<Longrightarrow> b \<in> wset (a - 1) p ==> b \<in> wset a p"
apply (subst wset.simps)
apply (unfold Let_def, auto)
done
lemma wset_g_1 [rule_format]:
- "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> 1 < b"
+ "zprime p --> a < p - 1 --> b \<in> wset a p --> 1 < b"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
apply (case_tac [2] "b = inv p a")
@@ -203,7 +199,7 @@
done
lemma wset_less [rule_format]:
- "zprime p --> a < p - 1 --> b \<in> wset (a, p) --> b < p - 1"
+ "zprime p --> a < p - 1 --> b \<in> wset a p --> b < p - 1"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
apply (case_tac [2] "b = inv p a")
@@ -216,7 +212,7 @@
lemma wset_mem [rule_format]:
"zprime p -->
- a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset (a, p)"
+ a < p - 1 --> 1 < b --> b \<le> a --> b \<in> wset a p"
apply (induct a p rule: wset.induct, auto)
apply (rule_tac wset_subset)
apply (simp (no_asm_simp))
@@ -224,8 +220,8 @@
done
lemma wset_mem_inv_mem [rule_format]:
- "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset (a, p)
- --> inv p b \<in> wset (a, p)"
+ "zprime p --> 5 \<le> p --> a < p - 1 --> b \<in> wset a p
+ --> inv p b \<in> wset a p"
apply (induct a p rule: wset_induct, auto)
apply (case_tac "b = a")
apply (subst wset.simps)
@@ -240,13 +236,13 @@
lemma wset_inv_mem_mem:
"zprime p \<Longrightarrow> 5 \<le> p \<Longrightarrow> a < p - 1 \<Longrightarrow> 1 < b \<Longrightarrow> b < p - 1
- \<Longrightarrow> inv p b \<in> wset (a, p) \<Longrightarrow> b \<in> wset (a, p)"
+ \<Longrightarrow> inv p b \<in> wset a p \<Longrightarrow> b \<in> wset a p"
apply (rule_tac s = "inv p (inv p b)" and t = b in subst)
apply (rule_tac [2] wset_mem_inv_mem)
apply (rule inv_inv, simp_all)
done
-lemma wset_fin: "finite (wset (a, p))"
+lemma wset_fin: "finite (wset a p)"
apply (induct a p rule: wset_induct)
prefer 2
apply (subst wset.simps)
@@ -255,27 +251,27 @@
lemma wset_zcong_prod_1 [rule_format]:
"zprime p -->
- 5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset(a, p). x) = 1] (mod p)"
+ 5 \<le> p --> a < p - 1 --> [(\<Prod>x\<in>wset a p. x) = 1] (mod p)"
apply (induct a p rule: wset_induct)
prefer 2
apply (subst wset.simps)
- apply (unfold Let_def, auto)
+ apply (auto, unfold Let_def, auto)
apply (subst setprod_insert)
apply (tactic {* stac (thm "setprod_insert") 3 *})
apply (subgoal_tac [5]
- "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
+ "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
prefer 5
apply (simp add: zmult_assoc)
apply (rule_tac [5] zcong_zmult)
apply (rule_tac [5] inv_is_inv)
apply (tactic "clarify_tac @{claset} 4")
- apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
+ apply (subgoal_tac [4] "a \<in> wset (a - 1) p")
apply (rule_tac [5] wset_inv_mem_mem)
apply (simp_all add: wset_fin)
apply (rule inv_distinct, auto)
done
-lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2, p)"
+lemma d22set_eq_wset: "zprime p ==> d22set (p - 2) = wset (p - 2) p"
apply safe
apply (erule wset_mem)
apply (rule_tac [2] d22set_g_1)
--- a/src/HOL/ZF/Games.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/ZF/Games.thy Tue Mar 02 12:26:50 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/ZF/Games.thy
+(* Title: HOL/ZF/MainZF.thy/Games.thy
Author: Steven Obua
An application of HOLZF: Partizan Games. See "Partizan Games in
@@ -347,13 +347,12 @@
right_option_def[symmetric] left_option_def[symmetric])
done
-consts
+function
neg_game :: "game \<Rightarrow> game"
-
-recdef neg_game "option_of"
- "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
-
-declare neg_game.simps[simp del]
+where
+ [simp del]: "neg_game g = Game (zimage neg_game (right_options g)) (zimage neg_game (left_options g))"
+by auto
+termination by (relation "option_of") auto
lemma "neg_game (neg_game g) = g"
apply (induct g rule: neg_game.induct)
@@ -365,17 +364,16 @@
apply (auto simp add: zet_ext_eq zimage_iff)
done
-consts
+function
ge_game :: "(game * game) \<Rightarrow> bool"
-
-recdef ge_game "(gprod_2_1 option_of)"
- "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
+where
+ [simp del]: "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G)))
else \<not> (ge_game (H, x)))
else (if zin x (left_options H) then \<not> (ge_game (x, G)) else True))"
-(hints simp: gprod_2_1_def)
-
-declare ge_game.simps [simp del]
+by auto
+termination by (relation "(gprod_2_1 option_of)")
+ (simp, auto simp: gprod_2_1_def)
lemma ge_game_eq: "ge_game (G, H) = (\<forall> x. (zin x (right_options G) \<longrightarrow> \<not> ge_game (H, x)) \<and> (zin x (left_options H) \<longrightarrow> \<not> ge_game (x, G)))"
apply (subst ge_game.simps[where G=G and H=H])
@@ -506,19 +504,18 @@
definition zero_game :: game
where "zero_game \<equiv> Game zempty zempty"
-consts
- plus_game :: "game * game \<Rightarrow> game"
+function
+ plus_game :: "game \<Rightarrow> game \<Rightarrow> game"
+where
+ [simp del]: "plus_game G H = Game (zunion (zimage (\<lambda> g. plus_game g H) (left_options G))
+ (zimage (\<lambda> h. plus_game G h) (left_options H)))
+ (zunion (zimage (\<lambda> g. plus_game g H) (right_options G))
+ (zimage (\<lambda> h. plus_game G h) (right_options H)))"
+by auto
+termination by (relation "gprod_2_2 option_of")
+ (simp, auto simp: gprod_2_2_def)
-recdef plus_game "gprod_2_2 option_of"
- "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
- (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
- (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
- (zimage (\<lambda> h. plus_game (G, h)) (right_options H)))"
-(hints simp add: gprod_2_2_def)
-
-declare plus_game.simps[simp del]
-
-lemma plus_game_comm: "plus_game (G, H) = plus_game (H, G)"
+lemma plus_game_comm: "plus_game G H = plus_game H G"
proof (induct G H rule: plus_game.induct)
case (1 G H)
show ?case
@@ -541,11 +538,11 @@
lemma right_zero_game[simp]: "right_options (zero_game) = zempty"
by (simp add: zero_game_def)
-lemma plus_game_zero_right[simp]: "plus_game (G, zero_game) = G"
+lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
proof -
{
fix G H
- have "H = zero_game \<longrightarrow> plus_game (G, H) = G "
+ have "H = zero_game \<longrightarrow> plus_game G H = G "
proof (induct G H rule: plus_game.induct, rule impI)
case (goal1 G H)
note induct_hyp = prems[simplified goal1, simplified] and prems
@@ -553,7 +550,7 @@
apply (simp only: plus_game.simps[where G=G and H=H])
apply (simp add: game_ext_eq prems)
apply (auto simp add:
- zimage_cong[where f = "\<lambda> g. plus_game (g, zero_game)" and g = "id"]
+ zimage_cong[where f = "\<lambda> g. plus_game g zero_game" and g = "id"]
induct_hyp)
done
qed
@@ -561,7 +558,7 @@
then show ?thesis by auto
qed
-lemma plus_game_zero_left: "plus_game (zero_game, G) = G"
+lemma plus_game_zero_left: "plus_game zero_game G = G"
by (simp add: plus_game_comm)
lemma left_imp_options[simp]: "zin opt (left_options g) \<Longrightarrow> zin opt (options g)"
@@ -571,11 +568,11 @@
by (simp add: options_def zunion)
lemma left_options_plus:
- "left_options (plus_game (u, v)) = zunion (zimage (\<lambda>g. plus_game (g, v)) (left_options u)) (zimage (\<lambda>h. plus_game (u, h)) (left_options v))"
+ "left_options (plus_game u v) = zunion (zimage (\<lambda>g. plus_game g v) (left_options u)) (zimage (\<lambda>h. plus_game u h) (left_options v))"
by (subst plus_game.simps, simp)
lemma right_options_plus:
- "right_options (plus_game (u, v)) = zunion (zimage (\<lambda>g. plus_game (g, v)) (right_options u)) (zimage (\<lambda>h. plus_game (u, h)) (right_options v))"
+ "right_options (plus_game u v) = zunion (zimage (\<lambda>g. plus_game g v) (right_options u)) (zimage (\<lambda>h. plus_game u h) (right_options v))"
by (subst plus_game.simps, simp)
lemma left_options_neg: "left_options (neg_game u) = zimage neg_game (right_options u)"
@@ -584,32 +581,32 @@
lemma right_options_neg: "right_options (neg_game u) = zimage neg_game (left_options u)"
by (subst neg_game.simps, simp)
-lemma plus_game_assoc: "plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
proof -
{
fix a
- have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game (F, G), H) = plus_game (F, plus_game (G, H))"
+ have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
proof (induct a rule: induct_game, (rule impI | rule allI)+)
case (goal1 x F G H)
- let ?L = "plus_game (plus_game (F, G), H)"
- let ?R = "plus_game (F, plus_game (G, H))"
+ let ?L = "plus_game (plus_game F G) H"
+ let ?R = "plus_game F (plus_game G H)"
note options_plus = left_options_plus right_options_plus
{
fix opt
note hyp = goal1(1)[simplified goal1(2), rule_format]
- have F: "zin opt (options F) \<Longrightarrow> plus_game (plus_game (opt, G), H) = plus_game (opt, plus_game (G, H))"
+ have F: "zin opt (options F) \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
by (blast intro: hyp lprod_3_3)
- have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game (F, opt), H) = plus_game (F, plus_game (opt, H))"
+ have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
by (blast intro: hyp lprod_3_4)
- have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game (F, G), opt) = plus_game (F, plus_game (G, opt))"
+ have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)"
by (blast intro: hyp lprod_3_5)
note F and G and H
}
note induct_hyp = this
have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
by (auto simp add:
- plus_game.simps[where G="plus_game (F,G)" and H=H]
- plus_game.simps[where G="F" and H="plus_game (G,H)"]
+ plus_game.simps[where G="plus_game F G" and H=H]
+ plus_game.simps[where G="F" and H="plus_game G H"]
zet_ext_eq zunion zimage_iff options_plus
induct_hyp left_imp_options right_imp_options)
then show ?case
@@ -619,7 +616,7 @@
then show ?thesis by auto
qed
-lemma neg_plus_game: "neg_game (plus_game (G, H)) = plus_game(neg_game G, neg_game H)"
+lemma neg_plus_game: "neg_game (plus_game G H) = plus_game (neg_game G) (neg_game H)"
proof (induct G H rule: plus_game.induct)
case (1 G H)
note opt_ops =
@@ -627,26 +624,26 @@
left_options_neg right_options_neg
show ?case
by (auto simp add: opt_ops
- neg_game.simps[of "plus_game (G,H)"]
+ neg_game.simps[of "plus_game G H"]
plus_game.simps[of "neg_game G" "neg_game H"]
Game_ext zet_ext_eq zunion zimage_iff prems)
qed
-lemma eq_game_plus_inverse: "eq_game (plus_game (x, neg_game x)) zero_game"
+lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
proof (induct x rule: wf_induct[OF wf_option_of])
case (goal1 x)
{ fix y
assume "zin y (options x)"
- then have "eq_game (plus_game (y, neg_game y)) zero_game"
+ then have "eq_game (plus_game y (neg_game y)) zero_game"
by (auto simp add: prems)
}
note ihyp = this
{
fix y
assume y: "zin y (right_options x)"
- have "\<not> (ge_game (zero_game, plus_game (y, neg_game x)))"
+ have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game (y, neg_game y)"])
+ apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: prems)
done
@@ -655,9 +652,9 @@
{
fix y
assume y: "zin y (left_options x)"
- have "\<not> (ge_game (zero_game, plus_game (x, neg_game y)))"
+ have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game (y, neg_game y)"])
+ apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
apply (auto simp add: left_options_plus zunion zimage_iff intro: prems)
done
@@ -666,9 +663,9 @@
{
fix y
assume y: "zin y (left_options x)"
- have "\<not> (ge_game (plus_game (y, neg_game x), zero_game))"
+ have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game (y, neg_game y)"])
+ apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: prems)
done
@@ -677,9 +674,9 @@
{
fix y
assume y: "zin y (right_options x)"
- have "\<not> (ge_game (plus_game (x, neg_game y), zero_game))"
+ have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game (y, neg_game y)"])
+ apply (rule exI[where x="plus_game y (neg_game y)"])
apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
apply (auto simp add: right_options_plus zunion zimage_iff intro: prems)
done
@@ -687,28 +684,28 @@
note case4 = this
show ?case
apply (simp add: eq_game_def)
- apply (simp add: ge_game.simps[of "plus_game (x, neg_game x)" "zero_game"])
- apply (simp add: ge_game.simps[of "zero_game" "plus_game (x, neg_game x)"])
+ apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
+ apply (simp add: ge_game.simps[of "zero_game" "plus_game x (neg_game x)"])
apply (simp add: right_options_plus left_options_plus right_options_neg left_options_neg zunion zimage_iff)
apply (auto simp add: case1 case2 case3 case4)
done
qed
-lemma ge_plus_game_left: "ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
proof -
{ fix a
- have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game(plus_game (x, y), plus_game (x, z))"
+ have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
proof (induct a rule: induct_game, (rule impI | rule allI)+)
case (goal1 a x y z)
note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
{
- assume hyp: "ge_game(plus_game (x, y), plus_game (x, z))"
+ assume hyp: "ge_game(plus_game x y, plus_game x z)"
have "ge_game (y, z)"
proof -
{ fix yr
assume yr: "zin yr (right_options y)"
- from hyp have "\<not> (ge_game (plus_game (x, z), plus_game (x, yr)))"
- by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
+ from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
+ by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
right_options_plus zunion zimage_iff intro: yr)
then have "\<not> (ge_game (z, yr))"
apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
@@ -718,8 +715,8 @@
note yr = this
{ fix zl
assume zl: "zin zl (left_options z)"
- from hyp have "\<not> (ge_game (plus_game (x, zl), plus_game (x, y)))"
- by (auto simp add: ge_game_eq[of "plus_game (x,y)" "plus_game(x,z)"]
+ from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
+ by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
left_options_plus zunion zimage_iff intro: zl)
then have "\<not> (ge_game (zl, y))"
apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
@@ -739,11 +736,11 @@
{
fix x'
assume x': "zin x' (right_options x)"
- assume hyp: "ge_game (plus_game (x, z), plus_game (x', y))"
- then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
- by (auto simp add: ge_game_eq[of "plus_game (x,z)" "plus_game (x', y)"]
+ assume hyp: "ge_game (plus_game x z, plus_game x' y)"
+ then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+ by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"]
right_options_plus zunion zimage_iff intro: x')
- have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+ have t: "ge_game (plus_game x' y, plus_game x' z)"
apply (subst induct_hyp[symmetric])
apply (auto intro: lprod_3_3 x' yz)
done
@@ -753,11 +750,11 @@
{
fix x'
assume x': "zin x' (left_options x)"
- assume hyp: "ge_game (plus_game (x', z), plus_game (x, y))"
- then have n: "\<not> (ge_game (plus_game (x', y), plus_game (x', z)))"
- by (auto simp add: ge_game_eq[of "plus_game (x',z)" "plus_game (x, y)"]
+ assume hyp: "ge_game (plus_game x' z, plus_game x y)"
+ then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+ by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"]
left_options_plus zunion zimage_iff intro: x')
- have t: "ge_game (plus_game (x', y), plus_game (x', z))"
+ have t: "ge_game (plus_game x' y, plus_game x' z)"
apply (subst induct_hyp[symmetric])
apply (auto intro: lprod_3_3 x' yz)
done
@@ -767,7 +764,7 @@
{
fix y'
assume y': "zin y' (right_options y)"
- assume hyp: "ge_game (plus_game(x, z), plus_game (x, y'))"
+ assume hyp: "ge_game (plus_game x z, plus_game x y')"
then have "ge_game(z, y')"
apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
apply (auto simp add: hyp lprod_3_6 y')
@@ -780,7 +777,7 @@
{
fix z'
assume z': "zin z' (left_options z)"
- assume hyp: "ge_game (plus_game(x, z'), plus_game (x, y))"
+ assume hyp: "ge_game (plus_game x z', plus_game x y)"
then have "ge_game(z', y)"
apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
apply (auto simp add: hyp lprod_3_7 z')
@@ -790,7 +787,7 @@
with z' have "False" by (auto simp add: ge_game_leftright_refl)
}
note case4 = this
- have "ge_game(plus_game (x, y), plus_game (x, z))"
+ have "ge_game(plus_game x y, plus_game x z)"
apply (subst ge_game_eq)
apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
apply (auto intro: case1 case2 case3 case4)
@@ -804,7 +801,7 @@
then show ?thesis by blast
qed
-lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game (y, x), plus_game (z, x))"
+lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
by (simp add: ge_plus_game_left plus_game_comm)
lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
@@ -865,7 +862,7 @@
Pg_minus_def: "- G = contents (\<Union> g \<in> Rep_Pg G. {Abs_Pg (eq_game_rel `` {neg_game g})})"
definition
- Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game (g,h)})})"
+ Pg_plus_def: "G + H = contents (\<Union> g \<in> Rep_Pg G. \<Union> h \<in> Rep_Pg H. {Abs_Pg (eq_game_rel `` {plus_game g h})})"
definition
Pg_diff_def: "G - H = G + (- (H::Pg))"
@@ -891,14 +888,14 @@
apply (simp add: eq_game_rel_def)
done
-lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game (g, h)})"
+lemma char_Pg_plus[simp]: "Abs_Pg (eq_game_rel `` {g}) + Abs_Pg (eq_game_rel `` {h}) = Abs_Pg (eq_game_rel `` {plus_game g h})"
proof -
- have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game (g, h)})}) respects2 eq_game_rel"
+ have "(\<lambda> g h. {Abs_Pg (eq_game_rel `` {plus_game g h})}) respects2 eq_game_rel"
apply (simp add: congruent2_def)
apply (auto simp add: eq_game_rel_def eq_game_def)
- apply (rule_tac y="plus_game (y1, z2)" in ge_game_trans)
+ apply (rule_tac y="plus_game y1 z2" in ge_game_trans)
apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
- apply (rule_tac y="plus_game (z1, y2)" in ge_game_trans)
+ apply (rule_tac y="plus_game z1 y2" in ge_game_trans)
apply (simp add: ge_plus_game_left[symmetric] ge_plus_game_right[symmetric])+
done
then show ?thesis
--- a/src/HOL/ZF/Zet.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/ZF/Zet.thy Tue Mar 02 12:26:50 2010 +0100
@@ -196,7 +196,7 @@
lemma zimage_id[simp]: "zimage id A = A"
by (simp add: zet_ext_eq zimage_iff)
-lemma zimage_cong[recdef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
+lemma zimage_cong[recdef_cong, fundef_cong]: "\<lbrakk> M = N; !! x. zin x N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> zimage f M = zimage g N"
by (auto simp add: zet_ext_eq zimage_iff)
end