
diff -r a250b56e7f2a -r ab53ddefc542 QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 12:06:00 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 16:36:20 2009 +0200
@@ -381,6 +381,22 @@
   make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
 *}
 
+(*consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
+
+ML {*
+    get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
+ |> fst
+ |> Syntax.string_of_term @{context}
+ |> writeln
+*}
+
+local_setup {*
+  fn lthy => (Toplevel.program (fn () =>
+    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
+  )) |> snd
+*}
+*)
+
 term vr'
 term ap'
 term ap'
@@ -650,17 +666,91 @@
 ML {*
   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"}]
+  val consts = [@{const_name "Nil"}, @{const_name "Cons"},
+                @{const_name "membship"}, @{const_name "card1"},
+                @{const_name "append"}, @{const_name "fold1"}];
+               
 *}
 
+ML {* val tm = @{term "x :: 'a list"} *}
+ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}
+ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}
+
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
 ML {* val fall = Const(@{const_name all}, dummyT) *}
 
 ML {*
-fun build_goal_term ctxt thm constructors rty qty mk_rep mk_abs =
+fun needs_lift (rty as Type (rty_s, _)) ty =
+  case ty of
+    Type (s, tys) =>
+      (s = rty_s) orelse (exists (needs_lift rty) tys)
+  | _ => false
+
+*}
+
+ML {*
+fun build_goal_term lthy thm constructors rty qty =
+  let
+    fun mk_rep tm =
+      let
+        val ty = exchange_ty rty qty (fastype_of tm)
+      in fst (get_fun repF rty qty lthy ty) $ tm end
+
+    fun mk_abs tm =
+      let
+        val _ = tracing (Syntax.string_of_term @{context} tm)
+        val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
+        val ty = exchange_ty rty qty (fastype_of tm) in
+      fst (get_fun absF rty qty lthy ty) $ tm end
+
+    fun is_constructor (Const (x, _)) = member (op =) constructors x
+      | is_constructor _ = false;
+
+    fun build_aux lthy tm =
+      case tm of
+      Abs (a as (_, vty, _)) =>
+      let
+        val (vs, t) = Term.dest_abs a;
+        val v = Free(vs, vty);
+        val t' = lambda v (build_aux lthy t)
+      in
+      if (not (needs_lift rty (fastype_of tm))) then t'
+      else mk_rep (mk_abs (
+        if not (needs_lift rty vty) then t'
+        else
+          let
+            val v' = mk_rep (mk_abs v);
+            val t1 = Envir.beta_norm (t' $ v')
+          in
+            lambda v t1
+          end
+      ))
+      end
+    | x =>
+      let
+        val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
+        val (opp, tms0) = Term.strip_comb tm
+        val tms = map (build_aux lthy) tms0
+        val ty = fastype_of tm
+      in
+        if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
+          then (list_comb (opp, (hd tms0) :: (tl tms)))
+      else if (is_constructor opp andalso needs_lift rty ty) then
+          mk_rep (mk_abs (list_comb (opp,tms)))
+        else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
+            mk_rep(mk_abs(list_comb(opp,tms)))
+        else if tms = [] then opp
+        else list_comb(opp, tms)
+      end
+  in
+    build_aux lthy (Thm.prop_of thm)
+  end
+
+*}
+
+ML {*
+fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =
   let
     fun mk_rep_abs x = mk_rep (mk_abs x);
 
@@ -719,21 +809,18 @@
 *}
 
 ML {*
-fun build_goal ctxt thm cons rty qty mk_rep mk_abs =
-  Logic.mk_equals ((build_goal_term ctxt thm cons rty qty mk_rep mk_abs), (Thm.prop_of thm))
+fun build_goal ctxt thm cons rty qty =
+  Logic.mk_equals ((build_goal_term ctxt thm cons rty qty), (Thm.prop_of thm))
 *}
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
 *}
-  
+
 ML {*
-m1_novars |> prop_of
-|> Syntax.string_of_term @{context}
-|> writeln; 
-build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
-|> Syntax.string_of_term @{context}
-|> writeln
+cterm_of @{theory} (prop_of m1_novars);
+cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
+cterm_of @{theory} (build_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)
 *}
 
 
@@ -813,7 +900,7 @@
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -829,7 +916,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"} @{typ "'a fset"} mk_rep mk_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -840,7 +927,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"} @{typ "'a fset"} mk_rep mk_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -851,7 +938,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"} @{typ "'a fset"} mk_rep mk_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   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)
@@ -862,17 +949,18 @@
   apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
-lemma zzz' :
+(*lemma zzz' :
   "(REP_fset (INSERT a (INSERT a (ABS_fset xs))) \<approx> REP_fset (INSERT a (ABS_fset xs)))"
   using list_eq.intros(4) by (simp only: zzz)
 
 thm QUOT_TYPE_I_fset.REPS_same
 ML {* val zzz'' = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} @{thm zzz'} *}
+*)
 
 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"} @{typ "'a fset"} mk_rep mk_abs
+  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
@@ -911,21 +999,11 @@
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-
 (* TODO: Consider defining it with an "if"; sth like:
    Babs p m = \<lambda>x. if x \<in> p then m x else undefined
 *)
 
 ML {*
-fun needs_lift (rty as Type (rty_s, _)) ty =
-  case ty of
-    Type (s, tys) =>
-      (s = rty_s) orelse (exists (needs_lift rty) tys)
-  | _ => false
-
-*}
-
-ML {*
 (* trm \<Rightarrow> new_trm *)
 fun regularise trm rty rel lthy =
   case trm of
@@ -1046,7 +1124,7 @@
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
-prove {*
+prove list_induct_r: {*
  Logic.mk_implies
    ((prop_of li),
    (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
@@ -1058,6 +1136,12 @@
   apply (metis)
   done
 
+ML {* val thm = @{thm list_induct_r} OF [li] *}
+ML {* val trm = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* Syntax.string_of_term @{context} trm |> writeln *}
+term fun_map
+ML {* Toplevel.program (fn () => cterm_of @{theory} trm) *}
+
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
 prove card1_suc_r: {*
@@ -1086,11 +1170,11 @@
 ML {*
   val goal =
     Toplevel.program (fn () =>
-      build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs
+      build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
     )
 *}
 ML {*
-  val cgoal = 
+  val cgoal =
     Toplevel.program (fn () =>
       cterm_of @{theory} goal
     )




