
diff -r 1d08221f48c4 -r e51af8bace65 QuotMain.thy
--- a/QuotMain.thy	Mon Sep 28 15:37:38 2009 +0200
+++ b/QuotMain.thy	Mon Sep 28 18:59:04 2009 +0200
@@ -561,7 +561,7 @@
 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys"
 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3"
 
-lemma list_eq_sym:
+lemma list_eq_refl:
   shows "xs \<approx> xs"
   apply (induct xs)
    apply (auto intro: list_eq.intros)
@@ -570,7 +570,7 @@
 lemma equiv_list_eq:
   shows "EQUIV list_eq"
   unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def
-  apply(auto intro: list_eq.intros list_eq_sym)
+  apply(auto intro: list_eq.intros list_eq_refl)
   done
 
 local_setup {*
@@ -732,7 +732,7 @@
     apply (rule_tac x = "a" in exI)
     apply (rule_tac x = "xs" in exI)
     apply (simp)
-    apply (rule list_eq_sym)
+    apply (rule list_eq_refl)
     done
   qed
 qed
@@ -806,7 +806,7 @@
 apply(rule list_eq.intros(3))
 apply(unfold REP_fset_def ABS_fset_def)
 apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
-apply(rule list_eq_sym)
+apply(rule list_eq_refl)
 done
 
 lemma append_respects_fst:
@@ -815,7 +815,7 @@
   using a
   apply(induct)
   apply(auto intro: list_eq.intros)
-  apply(simp add: list_eq_sym)
+  apply(simp add: list_eq_refl)
 done
 
 lemma yyy:
@@ -833,17 +833,17 @@
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
   apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule list_eq.intros(5))
   apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
-  apply(rule list_eq_sym)
+  apply(rule list_eq_refl)
 done
 
 lemma
@@ -862,40 +862,77 @@
 ML lambda
 
 ML {*
-fun build_goal thm constructors lifted_type mk_rep_abs =
+fun build_goal ctxt thm constructors lifted_type mk_rep_abs =
   let
-    fun is_const (Const (x, t)) = x mem constructors
+    fun is_constructor (Const (x, _)) = member (op =) constructors x
+      | is_constructor _ = false;
+
+    fun maybe_mk_rep_abs t =
+      let
+        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
+      in
+        if type_of t = lifted_type then mk_rep_abs t else t
+      end;
+
+    fun build_aux ctxt1 tm =
+      let
+        val (head, args) = Term.strip_comb tm;
+        val args' = map (build_aux ctxt1) args;
+      in
+        (case head of
+          Abs (x, T, t) =>
+            let
+              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
+              val v = Free (x', T);
+              val t' = subst_bound (v, t);
+              val rec_term = build_aux ctxt2 t';
+            in Term.lambda_name (x, v) rec_term end
+        | _ =>
+            if is_constructor head then
+              maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
+            else list_comb (head, args'))
+      end;
+
+    val concl2 = Thm.prop_of thm;
+  in
+    Logic.mk_equals (build_aux ctxt concl2, concl2)
+  end
+*}
+
+ML {*
+fun build_goal' ctxt thm constructors lifted_type mk_rep_abs =
+  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 @{context} t)
+        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
       in
         if type_of t = lifted_type then mk_rep_abs t else t
       end
 (*      handle TYPE _ => t*)
-    fun build_aux (Abs (s, t, tr)) =
-        let
-          val [(fresh_s, _)] = Variable.variant_frees @{context} [] [(s, ())];
-          val newv = Free (fresh_s, t);
-          val str = subst_bound (newv, tr);
-          val rec_term = build_aux str;
-          val bound_term = lambda newv rec_term
-        in
-          bound_term
-        end
-      | build_aux (f $ a) =
+    fun build_aux ctxt1 (Abs (x, T, t)) =
+          let
+            val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
+            val v = Free (x', T);
+            val t' = subst_bound (v, t);
+            val rec_term = build_aux ctxt2 t';
+          in Term.lambda_name (x, v) rec_term end
+      | build_aux ctxt1 (f $ a) =
           let
             val (f, args) = strip_comb (f $ a)
-            val _ = writeln (Syntax.string_of_term @{context} f)
+            val _ = writeln (Syntax.string_of_term ctxt f)
            in
-            (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
-            else list_comb ((build_aux f), (map build_aux args)))
+            if is_const f then
+              maybe_mk_rep_abs
+                (list_comb (f, map maybe_mk_rep_abs (map (build_aux ctxt1) args)))
+            else list_comb (build_aux ctxt1 f, map (build_aux ctxt1) args)
           end
-      | build_aux x =
+      | 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 concl2), concl2)
+  Logic.mk_equals (build_aux ctxt concl2, concl2)
 end *}
 
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
@@ -984,11 +1021,13 @@
   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"
   by auto
 
+
+thm QUOT_TYPE_I_fset.R_trans2
 ML {*
   fun foo_tac' ctxt =
     REPEAT_ALL_NEW (FIRST' [
-      rtac @{thm trueprop_cong},
-      rtac @{thm list_eq_sym},
+(*      rtac @{thm trueprop_cong},*)
+      rtac @{thm list_eq_refl},
       rtac @{thm cons_preserves},
       rtac @{thm mem_respects},
       rtac @{thm card1_rsp},
@@ -996,14 +1035,14 @@
       CHANGED o (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})),
       DatatypeAux.cong_tac,
       rtac @{thm ext},
-(*      rtac @{thm eq_reflection}*)
+      rtac @{thm eq_reflection},
       CHANGED o (ObjectLogic.full_atomize_tac)
     ])
 *}
 
 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 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)
 *}
@@ -1011,9 +1050,33 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+lemma atomize_eqv [atomize]: "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
+  (is "?rhs \<equiv> ?lhs")
+proof
+  assume "PROP ?lhs" then show "PROP ?rhs" by unfold
+next
+  assume *: "PROP ?rhs"
+  have "A = B"
+  proof (cases A)
+    case True
+    with * have B by unfold
+    with `A` show ?thesis by simp
+  next
+    case False
+    with * have "~ B" by auto
+    with `~ A` show ?thesis by simp
+  qed
+  then show "PROP ?lhs" by (rule eq_reflection)
+qed
+
+
 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 *)




