# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254232694 -7200
# Node ID b2ab3ba388a06064551fc5c2484c69c081620eb6
# Parent  13a719ddef69514872b55aef7aa46ac591c2b1ed
Handling abstraction correctly.

diff -r 13a719ddef69 -r b2ab3ba388a0 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 29 13:38:27 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 15:58:14 2009 +0200
@@ -822,15 +822,18 @@
   done
 
 ML {*
-  fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
+  fun mk_rep x = @{term REP_fset} $ x;
+  fun mk_abs x = @{term ABS_fset} $ x;
   val consts = [@{const_name "Nil"}, @{const_name "append"},
                 @{const_name "Cons"}, @{const_name "membship"},
                 @{const_name "card1"}]
 *}
 
 ML {*
-fun build_goal ctxt thm constructors qty mk_rep_abs =
+fun build_goal ctxt thm constructors rty qty mk_rep mk_abs =
   let
+    fun mk_rep_abs x = mk_rep (mk_abs x);
+
     fun is_constructor (Const (x, _)) = member (op =) constructors x
       | is_constructor _ = false;
 
@@ -838,7 +841,7 @@
       let
         val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
       in
-        if type_of t = qty then mk_rep_abs t else t
+        if fastype_of t = rty then mk_rep_abs t else t
       end;
 
     fun build_aux ctxt1 tm =
@@ -848,7 +851,16 @@
       in
         (case head of
           Abs (x, T, t) =>
-            let
+            if T = rty then let
+              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
+              val v = Free (x', qty);
+              val t' = subst_bound (mk_rep v, t);
+              val rec_term = build_aux ctxt2 t';
+              val _ = tracing (Syntax.string_of_term ctxt2 t')
+              val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
+            in
+              Term.lambda_name (x, v) rec_term
+            end else let
               val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
               val v = Free (x', T);
               val t' = subst_bound (v, t);
@@ -973,7 +985,7 @@
 
 ML {*
   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
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1009,7 +1021,7 @@
 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 @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1021,7 +1033,7 @@
 thm m2
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1033,7 +1045,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 @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_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)
@@ -1056,7 +1068,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 @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 *}
 ML {*
   val cgoal =
@@ -1080,11 +1092,15 @@
 ML {*
   val goal =
     Toplevel.program (fn () =>
-      build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+      build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
     )
 *}
+term all
 ML {*
-  val cgoal = cterm_of @{theory} goal
+  val cgoal = 
+    Toplevel.program (fn () =>
+      cterm_of @{theory} goal
+    )
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
 
@@ -1097,7 +1113,7 @@
   fun lift_theorem_fset_aux thm lthy =
     let
       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
-      val goal = build_goal @{context} novars consts @{typ "'a list"} mk_rep_abs;
+      val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_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;
@@ -1178,7 +1194,7 @@
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
 *}
 ML {*
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
 *}
 ML {*
   val cgoal = cterm_of @{theory} goal