diff -r 86fba2c4eeef -r 57bde65f6eb2 UnusedQuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/UnusedQuotMain.thy Wed Nov 25 11:41:42 2009 +0100 @@ -0,0 +1,486 @@ + +text {* tyRel takes a type and builds a relation that a quantifier over this + type needs to respect. *} +ML {* +fun tyRel ty rty rel lthy = + if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) + then rel + else (case ty of + Type (s, tys) => + let + val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; + val ty_out = ty --> ty --> @{typ bool}; + val tys_out = tys_rel ---> ty_out; + in + (case (maps_lookup (ProofContext.theory_of lthy) s) of + SOME (info) => list_comb (Const (#relfun info, tys_out), + map (fn ty => tyRel ty rty rel lthy) tys) + | NONE => HOLogic.eq_const ty + ) + end + | _ => HOLogic.eq_const ty) +*} + +(* +ML {* cterm_of @{theory} + (tyRel @{typ "'a \ 'a list \ 't \ 't"} (Logic.varifyT @{typ "'a list"}) + @{term "f::('a list \ 'a list \ bool)"} @{context}) +*} +*) + + +ML {* +fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) +fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) +fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) +fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) +*} + +(* applies f to the subterm of an abstractions, otherwise to the given term *) +ML {* +fun apply_subt f trm = + case trm of + Abs (x, T, t) => + let + val (x', t') = Term.dest_abs (x, T, t) + in + Term.absfree (x', T, f t') + end + | _ => f trm +*} + + + +(* FIXME: if there are more than one quotient, then you have to look up the relation *) +ML {* +fun my_reg lthy rel rty trm = + case trm of + Abs (x, T, t) => + if (needs_lift rty T) then + let + val rrel = tyRel T rty rel lthy + in + (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) + end + else + Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) + | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => + let + val ty1 = domain_type ty + val ty2 = domain_type ty1 + val rrel = tyRel T rty rel lthy + in + if (needs_lift rty T) then + (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) + else + Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t + end + | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => + let + val ty1 = domain_type ty + val ty2 = domain_type ty1 + val rrel = tyRel T rty rel lthy + in + if (needs_lift rty T) then + (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) + else + Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t + end + | Const (@{const_name "op ="}, ty) $ t => + if needs_lift rty (fastype_of t) then + (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *) + else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) + | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) + | _ => trm +*} + +(* For polymorphic types we need to find the type of the Relation term. *) +(* TODO: we assume that the relation is a Constant. Is this always true? *) +ML {* +fun my_reg_inst lthy rel rty trm = + case rel of + Const (n, _) => Syntax.check_term lthy + (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) +*} + +(* +ML {* + val r = Free ("R", dummyT); + val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\(x::'b list). P x"}); + val t2 = Syntax.check_term @{context} t; + cterm_of @{theory} t2 +*} +*) + +text {* Assumes that the given theorem is atomized *} +ML {* + fun build_regularize_goal thm rty rel lthy = + Logic.mk_implies + ((prop_of thm), + (my_reg_inst lthy rel rty (prop_of thm))) +*} + +ML {* +fun regularize thm rty rel rel_eqv rel_refl lthy = + let + val goal = build_regularize_goal thm rty rel lthy; + fun tac ctxt = + (ObjectLogic.full_atomize_tac) THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac rel_refl, + atac, + rtac @{thm universal_twice}, + (rtac @{thm impI} THEN' atac), + rtac @{thm implication_twice}, + EqSubst.eqsubst_tac ctxt [0] + [(@{thm equiv_res_forall} OF [rel_eqv]), + (@{thm equiv_res_exists} OF [rel_eqv])], + (* For a = b \ a \ b *) + (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), + (rtac @{thm RIGHT_RES_FORALL_REGULAR}) + ]); + val cthm = Goal.prove lthy [] [] goal + (fn {context, ...} => tac context 1); + in + cthm OF [thm] + end +*} + +(*consts Rl :: "'a list \ 'a list \ bool" +axioms Rl_eq: "EQUIV Rl" + +quotient ql = "'a list" / "Rl" + by (rule Rl_eq) +ML {* + ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \ (nat \ nat) list"}); + ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \ nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \ (nat \ nat) list"}) +*} +*) + +ML {* +(* returns all subterms where two types differ *) +fun diff (T, S) Ds = + case (T, S) of + (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds + | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds + | (Type (a, Ts), Type (b, Us)) => + if a = b then diffs (Ts, Us) Ds else (T, S)::Ds + | _ => (T, S)::Ds +and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) + | diffs ([], []) Ds = Ds + | diffs _ _ = error "Unequal length of type arguments" + +*} + +ML {* +fun build_repabs_term lthy thm consts rty qty = + let + (* TODO: The rty and qty stored in the quotient_info should + be varified, so this will soon not be needed *) + val rty = Logic.varifyT rty; + val qty = Logic.varifyT qty; + + fun mk_abs tm = + let + val ty = fastype_of tm + in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end + fun mk_repabs tm = + let + val ty = fastype_of tm + in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end + + fun is_lifted_const (Const (x, _)) = member (op =) consts x + | is_lifted_const _ = 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_repabs ( + if not (needs_lift rty vty) then t' + else + let + val v' = mk_repabs v; + (* TODO: I believe 'beta' is not needed any more *) + val t1 = (* Envir.beta_norm *) (t' $ v') + in + lambda v t1 + end) + end + | x => + case Term.strip_comb tm of + (Const(@{const_name Respects}, _), _) => tm + | (opp, tms0) => + let + val tms = map (build_aux lthy) tms0 + val ty = fastype_of tm + in + if (is_lifted_const opp andalso needs_lift rty ty) then + mk_repabs (list_comb (opp, tms)) + else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then + mk_repabs (list_comb (opp, tms)) + else if tms = [] then opp + else list_comb(opp, tms) + end + in + repeat_eqsubst_prop lthy @{thms id_def_sym} + (build_aux lthy (Thm.prop_of thm)) + end +*} + +text {* Builds provable goals for regularized theorems *} +ML {* +fun build_repabs_goal ctxt thm cons rty qty = + Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) +*} + +ML {* +fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = + let + val rt = build_repabs_term lthy thm consts rty qty; + val rg = Logic.mk_equals ((Thm.prop_of thm), rt); + fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' + (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); + val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); + in + @{thm Pure.equal_elim_rule1} OF [cthm, thm] + end +*} + + +(* TODO: Check if it behaves properly with varifyed rty *) +ML {* +fun findabs_all rty tm = + case tm of + Abs(_, T, b) => + let + val b' = subst_bound ((Free ("x", T)), b); + val tys = findabs_all rty b' + val ty = fastype_of tm + in if needs_lift rty ty then (ty :: tys) else tys + end + | f $ a => (findabs_all rty f) @ (findabs_all rty a) + | _ => []; +fun findabs rty tm = distinct (op =) (findabs_all rty tm) +*} + + +(* Currently useful only for LAMBDA_PRS *) +ML {* +fun make_simp_prs_thm lthy quot_thm thm typ = + let + val (_, [lty, rty]) = dest_Type typ; + val thy = ProofContext.theory_of lthy; + val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) + val inst = [SOME lcty, NONE, SOME rcty]; + val lpi = Drule.instantiate' inst [] thm; + val tac = + (compose_tac (false, lpi, 2)) THEN_ALL_NEW + (quotient_tac quot_thm); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + in + MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t + end +*} + +ML {* +fun findallex_all rty qty tm = + case tm of + Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + ((T :: tya), tye) + else (tya, tye) end + | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => + let + val (tya, tye) = findallex_all rty qty s + in if needs_lift rty T then + (tya, (T :: tye)) + else (tya, tye) end + | Abs(_, T, b) => + findallex_all rty qty (subst_bound ((Free ("x", T)), b)) + | f $ a => + let + val (a1, e1) = findallex_all rty qty f; + val (a2, e2) = findallex_all rty qty a; + in (a1 @ a2, e1 @ e2) end + | _ => ([], []); +*} + +ML {* +fun findallex lthy rty qty tm = + let + val (a, e) = findallex_all rty qty tm; + val (ad, ed) = (map domain_type a, map domain_type e); + val (au, eu) = (distinct (op =) ad, distinct (op =) ed); + val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) + in + (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) + end +*} + +ML {* +fun make_allex_prs_thm lthy quot_thm thm typ = + let + val (_, [lty, rty]) = dest_Type typ; + val thy = ProofContext.theory_of lthy; + val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) + val inst = [NONE, SOME lcty]; + val lpi = Drule.instantiate' inst [] thm; + val tac = + (compose_tac (false, lpi, 1)) THEN_ALL_NEW + (quotient_tac quot_thm); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + val t_noid = MetaSimplifier.rewrite_rule + [@{thm eq_reflection} OF @{thms id_apply}] t; + val t_sym = @{thm "HOL.sym"} OF [t_noid]; + val t_eq = @{thm "eq_reflection"} OF [t_sym] + in + t_eq + end +*} + +ML {* +fun lift_thm lthy qty qty_name rsp_thms defs rthm = +let + val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) + + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; + val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; + val consts = lookup_quot_consts defs; + val t_a = atomize_thm rthm; + + val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) + + val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; + + val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) + + val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; + + val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) + + val (alls, exs) = findallex lthy rty qty (prop_of t_a); + val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls + val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs + val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) + + val abs = findabs rty (prop_of t_a); + val aps = findaps rty (prop_of t_a); + val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; + val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; + val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) + + val defs_sym = flat (map (add_lower_defs lthy) defs); + val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; + val t_id = simp_ids lthy t_l; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) + + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) + + val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) + + val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; + + val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) + + val t_rv = ObjectLogic.rulify t_r + + val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv)) +in + Thm.varifyT t_rv +end +*} + +ML {* +fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = + let + val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end +*} + + +ML {* +fun regularize_goal lthy thm rel_eqv rel_refl qtrm = + let + val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; + fun tac lthy = regularize_tac lthy rel_eqv rel_refl; + val cthm = Goal.prove lthy [] [] reg_trm + (fn {context, ...} => tac context 1); + in + cthm OF [thm] + end +*} + +ML {* +fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = + let + val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); + fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' + (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); + val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); + in + @{thm Pure.equal_elim_rule1} OF [cthm, thm] + end +*} + +ML {* +fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = +let + val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; + val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; + val t_a = atomize_thm rthm; + val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; + val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; + val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; + val (alls, exs) = findallex lthy rty qty (prop_of t_a); + val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls + val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs + val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t + val abs = findabs rty (prop_of t_a); + val aps = findaps rty (prop_of t_a); + val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; + val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; + val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; + val defs_sym = flat (map (add_lower_defs lthy) defs); + val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; + val t_id = simp_ids lthy t_l; + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; + val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; + val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; + val t_rv = ObjectLogic.rulify t_r +in + Thm.varifyT t_rv +end +*} + +ML {* +fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = + let + val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; + val (_, lthy2) = note (name, lifted_thm) lthy; + in + lthy2 + end +*} +