--- a/FSet.thy Sat Oct 24 17:29:20 2009 +0200
+++ b/FSet.thy Sat Oct 24 18:17:38 2009 +0200
@@ -2,42 +2,6 @@
imports QuotMain
begin
-(* test for get_fun *)
-datatype t =
- vr "string"
- | ap "t list"
- | lm "string" "t"
-
-consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool"
-axioms t_eq: "EQUIV Rt"
-
-quotient qt = "t" / "Rt"
- by (rule t_eq)
-
-ML {*
-get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
- |> fst
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {*
-get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"}
- |> fst
- |> Syntax.string_of_term @{context}
- |> writeln
-*}
-
-ML {*
-get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"}
- |> fst
- |> Syntax.pretty_term @{context}
- |> Pretty.string_of
- |> writeln
-*}
-(* end test get_fun *)
-
-
inductive
list_eq (infix "\<approx>" 50)
where
--- a/QuotMain.thy Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotMain.thy Sat Oct 24 18:17:38 2009 +0200
@@ -243,6 +243,7 @@
end
*}
+
text {* produces the definition for a lifted constant *}
ML {*
@@ -258,11 +259,12 @@
val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys
val abs_fn = (fst o get_fun absF rty qty lthy) res_ty
+ fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2
+
+ val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn)
+ |> Syntax.check_term lthy
in
- map (op $) (rep_fns ~~ fresh_args)
- |> curry list_comb oconst
- |> curry (op $) abs_fn
- |> fold_rev lambda fresh_args
+ fns $ oconst
end
*}
--- a/QuotTest.thy Sat Oct 24 17:29:20 2009 +0200
+++ b/QuotTest.thy Sat Oct 24 18:17:38 2009 +0200
@@ -72,7 +72,6 @@
quotient qt = "t" / "Rt"
by (rule t_eq)
-
ML {*
get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
|> fst