--- 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
)