
diff -r f078dbf557b7 -r d98224cafb86 QuotMain.thy
--- a/QuotMain.thy	Mon Sep 28 19:10:27 2009 +0200
+++ b/QuotMain.thy	Mon Sep 28 19:15:19 2009 +0200
@@ -151,18 +151,18 @@
                |> map Free
 in
   lambda c
-    (HOLogic.exists_const ty $ 
+    (HOLogic.exists_const ty $
        lambda x (HOLogic.mk_eq (c, (rel $ x))))
 end
 
 
 (* makes the new type definitions and proves non-emptyness*)
 fun typedef_make (qty_name, rel, ty) lthy =
-let  
+let
   val typedef_tac =
      EVERY1 [rewrite_goal_tac @{thms mem_def},
-             rtac @{thm exI}, 
-             rtac @{thm exI}, 
+             rtac @{thm exI},
+             rtac @{thm exI},
              rtac @{thm refl}]
 in
   LocalTheory.theory_result
@@ -217,7 +217,7 @@
             rtac @{thm QUOT_TYPE.QUOTIENT},
             rtac quot_type_thm]
 in
-  Goal.prove lthy [] [] goal 
+  Goal.prove lthy [] [] goal
     (K typedef_quotient_thm_tac)
 end
 *}
@@ -324,8 +324,8 @@
 | app  "trm" "trm"
 | lam  "nat" "trm"
 
-axiomatization 
-  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" 
+axiomatization
+  RR :: "trm \<Rightarrow> trm \<Rightarrow> bool"
 where
   r_eq: "EQUIV RR"
 
@@ -480,7 +480,7 @@
 
 ML {*
 fun exchange_ty rty qty ty =
-  if ty = rty 
+  if ty = rty
   then qty
   else
     (case ty of
@@ -674,7 +674,7 @@
   fixes xs :: "'a list"
   assumes a : "x memb xs"
   shows "x # xs \<approx> xs"
-  using a 
+  using a
   apply (induct xs)
   apply (auto intro: list_eq.intros)
   done
@@ -684,10 +684,10 @@
   fixes n :: "nat"
   assumes c: "card1 xs = Suc n"
   shows "\<exists>a ys. ~(a memb ys) \<and> xs \<approx> (a # ys)"
-  using c 
+  using c
 apply(induct xs)
 apply (metis Suc_neq_Zero card1_0)
-apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_sym mem_cons)
+apply (metis QUOT_TYPE_I_fset.R_trans QuotMain.card1_cons list_eq_refl mem_cons)
 done
 
 lemma cons_preserves:
@@ -698,13 +698,13 @@
 
 
 text {*
-  Unlam_def converts a definition given as 
+  Unlam_def converts a definition given as
 
     c \<equiv> %x. %y. f x y
 
-  to a theorem of the form 
-   
-    c x y \<equiv> f x y 
+  to a theorem of the form
+
+    c x y \<equiv> f x y
 
   This function is needed to rewrite the right-hand
   side to the left-hand side.
@@ -817,8 +817,8 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}, @{const_name "append"}, 
-                @{const_name "Cons"}, @{const_name "membship"}, 
+  val consts = [@{const_name "Nil"}, @{const_name "append"},
+                @{const_name "Cons"}, @{const_name "membship"},
                 @{const_name "card1"}]
 *}
 
@@ -865,7 +865,7 @@
   let
     fun is_const (Const (x, t)) = member (op =) constructors x
       | is_const _ = false
-  
+
     fun maybe_mk_rep_abs t =
       let
         val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
@@ -892,7 +892,7 @@
           end
       | build_aux _ x =
           if is_const x then maybe_mk_rep_abs x else x
-    
+
     val concl2 = term_of (#prop (crep_thm thm))
   in
   Logic.mk_equals (build_aux ctxt concl2, concl2)
@@ -1004,16 +1004,8 @@
 *}
 
 ML {*
-<<<<<<< variant A
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
->>>>>>> variant B
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
-####### Ancestor
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
-======= end
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1043,17 +1035,13 @@
 
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
-  apply (atomize (full))
-  
-  apply (rule trueprop_cong)
   apply (tactic {* foo_tac' @{context} 1 *})
-  thm eq_reflection
   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 goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1065,7 +1053,7 @@
 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 goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1077,7 +1065,7 @@
 thm list_eq.intros(4)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
@@ -1105,7 +1093,7 @@
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
-  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
 *}
 ML {*
   val cgoal =
@@ -1148,7 +1136,7 @@
   fun lift_theorem_fset_aux thm lthy =
     let
       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
-      val goal = build_goal novars consts @{typ "'a list"} mk_rep_abs;
+      val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_abs;
       val cgoal = cterm_of @{theory} goal;
       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
       val tac = (LocalDefs.unfold_tac @{context} fset_defs) THEN (foo_tac' @{context}) 1;
@@ -1237,7 +1225,7 @@
 ML {* @{term "\<exists>x. P x"} *}
 ML {*  Thm.bicompose *}
 prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) 
+  apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
 
 




