--- a/QuotMain.thy	Thu Sep 24 13:32:52 2009 +0200
+++ b/QuotMain.thy	Thu Sep 24 17:43:26 2009 +0200
@@ -322,8 +322,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"
 
@@ -859,6 +859,8 @@
   val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}]
 *}
 
+ML lambda
+
 ML {*
 fun build_goal thm constructors lifted_type mk_rep_abs =
   let
@@ -870,8 +872,17 @@
       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)) = (Abs (s, t, build_aux tr))
+(*      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) =
           let
             val (f, args) = strip_comb (f $ a)
@@ -919,8 +930,9 @@
 *}
 
 ML {*
-  fun foo_conv t =
+  fun split_binop_conv t =
     let
+      val _ = tracing (Syntax.string_of_term @{context} (term_of t))
       val (lhs, rhs) = dest_ceq t;
       val (bop, _) = dest_cbinop lhs;
       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
@@ -931,13 +943,34 @@
 *}
 
 ML {*
-  fun foo_tac n thm =
+  fun split_arg_conv t =
+    let
+      val (lhs, rhs) = dest_ceq t;
+      val (lop, larg) = Thm.dest_comb lhs;
+      val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+    in
+      Drule.instantiate' [SOME caT,SOME crT] [NONE,NONE,SOME lop] @{thm arg_cong}
+    end
+*}
+
+ML {*
+  fun split_binop_tac n thm =
     let
       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 rewr = split_binop_conv cconcl;
+    in
+      rtac rewr n thm
+    end
+      handle CTERM _ => Seq.empty
+*}
+
+ML {*
+  fun split_arg_tac n thm =
+    let
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = split_arg_conv cconcl;
     in
       rtac rewr n thm
     end
@@ -960,7 +993,9 @@
       rtac @{thm card1_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,
+      DatatypeAux.cong_tac,
+      rtac @{thm ext},
+(*      rtac @{thm eq_reflection}*)
       CHANGED o (ObjectLogic.full_atomize_tac)
     ])
 *}
@@ -1066,7 +1101,6 @@
   done
 
 thm list.induct
-ML {* Logic.list_implies ((Thm.prems_of @{thm list.induct}), (Thm.concl_of @{thm list.induct})) *}
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
@@ -1079,13 +1113,14 @@
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal
+*}
+ML {*
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
-ML fset_defs_sym
+
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
-  apply (rule_tac f = "P" in arg_cong)
   sorry
 
 thm card1_suc
@@ -1100,10 +1135,11 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
+ML {* @{term "\<exists>x. P x"} *}
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
-
+  done
 
 
 (*