QuotMain.thy
changeset 25 9020ee23a020
parent 24 6885fa184e89
child 27 160f287ebb75
--- a/QuotMain.thy	Mon Sep 21 10:53:01 2009 +0200
+++ b/QuotMain.thy	Mon Sep 21 16:45:44 2009 +0200
@@ -114,11 +114,12 @@
 qed
 
 lemma REPS_same:
-  shows "R (REP a) (REP b) = (a = b)"
+  shows "R (REP a) (REP b) \<equiv> (a = b)"
+  apply (rule eq_reflection)
 proof
   assume as: "R (REP a) (REP b)"
   from rep_prop
-  obtain x y 
+  obtain x y
     where eqs: "Rep a = R x" "Rep b = R y" by blast
   from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp
   then have "R x (Eps (R y))" using lem9 by simp
@@ -827,7 +828,7 @@
 ML {*@{thm arg_cong2}*}
 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
-ML {* 
+ML {*
   Toplevel.program (fn () =>
     Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
   )
@@ -851,8 +852,8 @@
       val concl = Thm.cprem_of thm n;
       val (_, cconcl) = Thm.dest_comb concl;
       val rewr = foo_conv cconcl;
-      val _ = tracing (Display.string_of_thm @{context} rewr)
-      val _ = tracing (Display.string_of_thm @{context} thm)
+(*      val _ = tracing (Display.string_of_thm @{context} rewr)
+      val _ = tracing (Display.string_of_thm @{context} thm)*)
     in
       rtac rewr n thm
     end
@@ -862,14 +863,15 @@
 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 
 ML {*
-  val foo_tac' =
-    FIRST' [
+  fun foo_tac' ctxt =
+    REPEAT_ALL_NEW (FIRST' [
       rtac @{thm list_eq_sym},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
-      foo_tac,
-      simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})
-    ]
+      rtac @{thm QUOT_TYPE_I_fset.R_trans2},
+      CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
+      foo_tac
+    ])
 *}
 
 thm m1
@@ -883,11 +885,7 @@
 
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 
@@ -898,13 +896,10 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
-(* prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 2 *})
-  apply (tactic {* foo_tac' 1 *}) *)
+  apply (tactic {* foo_tac' @{context} 1 *})
+  sorry
 
 thm m2
 ML {*
@@ -915,19 +910,7 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 thm list_eq.intros(4)
@@ -942,19 +925,10 @@
 (* It is the same, but we need a name for it. *)
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *} sorry
 lemma zzz :
-  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx>
-    REP_fset (INSERT a (ABS_fset xs))) =  (a # a # xs \<approx> a # xs)"
+  "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
+    = (a # a # xs \<approx> a # xs)"
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply (rule QUOT_TYPE_I_fset.R_trans2)
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 lemma zzz' :
@@ -962,7 +936,20 @@
   using list_eq.intros(4) by (simp only: zzz)
 
 thm QUOT_TYPE_I_fset.REPS_same
-ML {* MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+
+ML Drule.instantiate'
+ML {* zzz'' *}
+text {*
+  A variable export will still be necessary in the end, but this is already the final theorem.
+*}
+ML {*
+  Toplevel.program (fn () =>
+    MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.thm10} (
+      Drule.instantiate' [] [NONE,SOME (@{cpat "REP_fset x"})] zzz''
+    )
+  )
+*}
 
 thm list_eq.intros(5)
 ML {*
@@ -973,15 +960,7 @@
 *}
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (rule QUOT_TYPE_I_fset.R_trans2)
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
-  apply (tactic {* foo_tac' 1 *})
+  apply (tactic {* foo_tac' @{context} 1 *})
   done
 
 (*