# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259379963 -3600
# Node ID 123877af04edc55cd89f40b55a57fa0031f7f15b
# Parent  cd6ce3322b8f72dbbe65935f63abb27199ccc08f
fixed examples in IntEx and FSet

diff -r cd6ce3322b8f -r 123877af04ed FSet.thy
--- a/FSet.thy	Sat Nov 28 04:37:30 2009 +0100
+++ b/FSet.thy	Sat Nov 28 04:46:03 2009 +0100
@@ -322,7 +322,7 @@
 
 lemma "CARD x = Suc n \<Longrightarrow> (\<exists>a b. \<not> IN a b & x = INSERT a b)"
 apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *})
-done
+oops
 
 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))"
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
@@ -347,7 +347,7 @@
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 prefer 2
 apply(rule cheat)
 apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
@@ -449,7 +449,7 @@
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply (tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)
diff -r cd6ce3322b8f -r 123877af04ed IntEx.thy
--- a/IntEx.thy	Sat Nov 28 04:37:30 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 04:46:03 2009 +0100
@@ -147,11 +147,9 @@
 ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
-lemma cheat: "P" sorry
-
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 prefer 2
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -161,12 +159,6 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***)
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
@@ -178,7 +170,13 @@
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
-apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
+apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
 done
 
 lemma plus_assoc_pre:
@@ -191,7 +189,7 @@
 
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
@@ -228,7 +226,7 @@
 
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
-apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *})
 apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) 
 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}