# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1253274246 -7200
# Node ID ccc220a23887b373cb205984e7775ba77f5176e7
# Parent  55aefc2d524abab4a6a5a82fc550727190aeefc9
Testing the tactic further.

diff -r 55aefc2d524a -r ccc220a23887 QuotMain.thy
--- a/QuotMain.thy	Thu Sep 17 16:55:11 2009 +0200
+++ b/QuotMain.thy	Fri Sep 18 13:44:06 2009 +0200
@@ -746,58 +746,6 @@
 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
 ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 
-thm m1
-
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
-*}
-
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-  apply(rule_tac f="(op =)" in arg_cong2)
-  unfolding IN_def EMPTY_def
-  apply (rule_tac mem_respects)
-  apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply (simp_all)
-  apply (rule list_eq_sym)
-  done
-
-thm length_append (* Not true but worth checking that the goal is correct *)
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
-*}
-(*prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-unfolding CARD_def UNION_def
-apply(rule_tac f="(op =)" in arg_cong2)*)
-
-thm m2
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-  val cgoal = cterm_of @{theory} goal
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
-*}
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-apply(rule_tac f="(op =)" in arg_cong2)
-unfolding IN_def
-apply (rule_tac mem_respects)
-unfolding INSERT_def
-apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (rule cons_preserves)
-apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (rule list_eq_sym)
-apply (rule_tac f="(op \<or>)" in arg_cong2)
-apply (simp)
-apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (rule list_eq_sym)
-done
-
 notation ( output) "prop" ("#_" [1000] 1000)
 
 ML {* @{thm arg_cong2} *}
@@ -860,7 +808,8 @@
       handle CTERM _ => Seq.empty
 *}
 
-ML foo_tac
+(* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
+
 ML {*
   val foo_tac' =
     FIRST' [
@@ -872,10 +821,47 @@
     ]
 *}
 
-ML {* Thm.assume @{cprop "0 = 0"} *}
+thm m1
+
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
+*}
+
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+  apply (tactic {* foo_tac' 1 *})
+  unfolding IN_def EMPTY_def
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' 1 *})
+  done
+
 
-ML simp_tac
+thm length_append (* Not true but worth checking that the goal is correct *)
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
+*}
+(* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 2 *})
+apply (tactic {* foo_tac' 2 *})
+apply (tactic {* foo_tac' 2 *})
+unfolding CARD_def UNION_def
+apply (tactic {* foo_tac' 1 *}) *)
 
+thm m2
+ML {*
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
+*}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 apply (tactic {* foo_tac' 1 *})
 unfolding IN_def INSERT_def