--- a/QuotMain.thy	Thu Aug 27 09:04:39 2009 +0200
+++ b/QuotMain.thy	Fri Aug 28 10:01:25 2009 +0200
@@ -592,6 +592,14 @@
 apply(auto)
 done
 
+lemma cons_preserves:
+  fixes z
+  assumes a: "xs \<approx> ys"
+  shows "(z # xs) \<approx> (z # ys)"
+using a
+apply (rule QuotMain.list_eq.intros(5))
+done
+
 ML {*
 fun unlam_def orig_ctxt ctxt t =
   let
@@ -693,24 +701,31 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}]
+  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}]
 *}
 
 ML {*
-fun build_goal thm constructors mk_rep_abs =
+fun build_goal thm constructors lifted_type mk_rep_abs =
   let
     fun is_const (Const (x, t)) = x mem constructors
       | is_const _ = false
+    fun maybe_mk_rep_abs t =
+      let
+        val _ = writeln ("Maybe: " ^ Syntax.string_of_term @{context} t)
+      in
+        if type_of t = lifted_type then mk_rep_abs t else t
+      end
     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
       | build_aux (f $ a) =
           let
             val (f,args) = strip_comb (f $ a)
+            val _ = writeln (Syntax.string_of_term @{context} f)
            in
-            (if is_const f then mk_rep_abs (list_comb (f, (map mk_rep_abs (map build_aux args))))
+            (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)))
           end
       | build_aux x =
-          if is_const x then mk_rep_abs x else x
+          if is_const x then maybe_mk_rep_abs x else x
     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
   in
   HOLogic.mk_eq ((build_aux concl), concl)
@@ -726,7 +741,7 @@
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
-  val goal = build_goal m1_novars consts mk_rep_abs
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
 *}
 
@@ -750,10 +765,35 @@
 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 mk_rep_abs
+  val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
 *}
 ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
 ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
+ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}
+
+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
+*}
+ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *}
+ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+apply(rule_tac f="(op =)" in arg_cong2)
+unfolding IN_def
+apply (rule_tac mem_respects)
+unfolding INSERT_def
+apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (rule cons_preserves)
+apply (simp only: QUOT_TYPE_fset_i.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_fset_i.REP_ABS_rsp)
+apply (rule list_eq_sym)
+done