# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255683271 -7200
# Node ID 4683292581bc201c1562e0fbece9500067427b6d
# Parent  f5f641c05794c337dd330ab3332d73a4195c4c30
Finally fix get_fun.

diff -r f5f641c05794 -r 4683292581bc QuotMain.thy
--- a/QuotMain.thy	Fri Oct 16 08:48:56 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 10:54:31 2009 +0200
@@ -279,8 +279,9 @@
   let
     val (fs, tys) = split_list fs_tys
     val ([oty1, oty2], [nty1, nty2]) = split_list tys
-    val oty = Type (s, [oty2, nty1])
+    val oty = Type (s, [nty1, oty2])
     val nty = Type (s, [oty1, nty2])
+    val _ = tracing (Syntax.string_of_typ @{context} oty)
     val ftys = map (op -->) tys
   in
    (case (lookup (ProofContext.theory_of lthy) s) of
@@ -307,6 +308,8 @@
 end
 *}
 
+term fun_map
+
 ML {*
   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) list) * nat"}
   |> fst
@@ -345,41 +348,11 @@
 
 *}
 
-(*ML {*
-    get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
- |> fst
- |> type_of
-*}
-
-
 ML {*
-    get_fun repF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
+    get_fun repF @{typ t} @{typ qt} @{context} @{typ "((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt"}
  |> fst
  |> cterm_of @{theory}
 *}
-*)
-
-ML {*
-    get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
- |> fst
- |> type_of
-*}
-
-ML {*
-    get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \<Rightarrow> qt"}
- |> fst
- |> cterm_of @{theory}
-*}
-
-(* The followng also fails due to incorrect types... *)
-consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
-local_setup {*
-  fn lthy => (Toplevel.program (fn () =>
-    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
-  )) |> snd
-*}
-
-
 
 text {* produces the definition for a lifted constant *}
 
@@ -427,6 +400,15 @@
 end
 *}
 
+(* A test whether get_fun works properly
+consts bla :: "(t \<Rightarrow> t) \<Rightarrow> t"
+local_setup {*
+  fn lthy => (Toplevel.program (fn () =>
+    make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy
+  )) |> snd
+*}
+*)
+
 local_setup {*
   make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
   make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #>
@@ -734,7 +716,6 @@
   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"} *}
@@ -1203,9 +1184,8 @@
 
 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) *}
+prove trm
+sorry
 
 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
 
@@ -1229,32 +1209,10 @@
 ML {* @{thm fold1_def_2_r} OF [li] *}
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
-*}
-
-ML {*
-  val goal =
-    Toplevel.program (fn () =>
-      build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
-    )
-*}
-ML {*
-  val cgoal =
-    Toplevel.program (fn () =>
-      cterm_of @{theory} goal
-    )
-  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
-*}
-
-prove {* (Thm.term_of cgoal2) *}
-  apply (tactic {* transconv_fset_tac' @{context} *})
-  sorry
-
-ML {*
   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"} @{typ "'a fset"} mk_rep mk_abs;
+      val goal = build_goal @{context} 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);
       val tac = transconv_fset_tac' @{context};
@@ -1342,8 +1300,8 @@
      (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
      (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
 thm APPLY_RSP
-thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"]
-.
+thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
+apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"])
 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
 thm LAMBDA_PRS1[symmetric]