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 \ t) \ t" + +ML {* + get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt \ 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))) \ 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 \ bool) \ ('a \ 'b) \ 'a \ 'b" where "(x \ p) \ (Babs p m x = m x)" - (* TODO: Consider defining it with an "if"; sth like: Babs p m = \x. if x \ 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 \ 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 \"} @{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 )