# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1253717096 -7200
# Node ID e35198635d6410bfe46f716e12d925e31f88533e
# Parent  2b59bf690633624ea8c4d26e48e0e2275ce9d5bc
Using "atomize" the versions with arbitrary Trueprops can be proven.

diff -r 2b59bf690633 -r e35198635d64 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 22 17:39:52 2009 +0200
+++ b/QuotMain.thy	Wed Sep 23 16:44:56 2009 +0200
@@ -886,7 +886,7 @@
     val concl2 = Logic.list_implies (prems, concl)
 (*    val concl2 = fold (fn a => fn c => HOLogic.mk_imp (a, c)) prems concl*)
   in
-  HOLogic.mk_eq ((build_aux concl2), concl2)
+  Logic.mk_equals ( (build_aux concl2), concl2)
 end *}
 
 ML {* val emptyt = (symmetric (unlam_def  @{context} @{thm EMPTY_def})) *}
@@ -965,8 +965,6 @@
     ])
 *}
 
-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
@@ -974,20 +972,19 @@
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
 
-notation ( output) "prop" ("#_" [1000] 1000)
+(*notation ( output) "prop" ("#_" [1000] 1000) *)
+notation ( output) "Trueprop" ("#_" [1000] 1000)
 
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+lemma tp:
+  shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
+  by auto
+
+prove {* (Thm.term_of cgoal2) *}
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (tactic {* print_tac "" *})
-  thm arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="]
-(*  apply (rule arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])*)
-  apply (subst arg_cong2 [of "x memb REP_fset (ABS_fset (REP_fset (ABS_fset [])))" "x memb []" False False "op ="])
   apply (tactic {* foo_tac' @{context} 1 *})
-  apply (tactic {* foo_tac' @{context} 1 *})
-  thm arg_cong2 [of "x memb []" "x memb []" False False "op ="]
-  (*apply (rule arg_cong2 [of "x memb []" "x memb []" False False "op ="])
-  done *)
-  sorry
+  done
 
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
@@ -996,9 +993,11 @@
   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 {* Thm.term_of cgoal2 *}
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-(*  apply (tactic {* foo_tac' @{context} 1 *})*)
+  apply (tactic {* foo_tac' @{context} 1 *})
   sorry
 
 thm m2
@@ -1008,10 +1007,12 @@
   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 {* Thm.term_of cgoal2 *}
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-(*  apply (tactic {* foo_tac' @{context} 1 *})
-  done *) sorry
+  apply (tactic {* foo_tac' @{context} 1 *})
+  done
 
 thm list_eq.intros(4)
 ML {*
@@ -1023,13 +1024,17 @@
 *}
 
 (* It is the same, but we need a name for it. *)
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+prove {* Thm.term_of cgoal3 *}
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
-  sorry
+  done
 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)"
+  "Trueprop (REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))
+    \<equiv> Trueprop (a # a # xs \<approx> a # xs)"
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
@@ -1054,18 +1059,6 @@
   )
 *}
 
-thm sym
-ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm sym}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-*}
-ML {*
-  val cgoal = 
-    Toplevel.program (fn () =>
-      cterm_of @{theory} goal
-    )
-*}
-
 
 thm list_eq.intros(5)
 ML {*
@@ -1081,12 +1074,14 @@
 ML {*
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
+prove {* Thm.term_of cgoal2 *}
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
+  apply (rule tp)
+  apply (tactic {* ObjectLogic.full_atomize_tac 1 *})
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
-
 thm list.induct
 ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}