diff -r 86fba2c4eeef -r 57bde65f6eb2 QuotMain.thy --- a/QuotMain.thy Wed Nov 25 10:52:21 2009 +0100 +++ b/QuotMain.thy Wed Nov 25 11:41:42 2009 +0100 @@ -227,35 +227,6 @@ *) -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}) -*} -*) - definition Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" where @@ -273,94 +244,6 @@ *} -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))) -*} lemma universal_twice: assumes *: "\x. (P x \ Q x)" @@ -373,32 +256,6 @@ shows "(a \ b) \ (c \ d)" using a b by auto -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 -*} - section {* RepAbs injection *} (* @@ -473,16 +330,6 @@ handle TYPE _ => ty (* for dest_Type *) *} -(*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 {* fun find_matching_types rty ty = @@ -535,19 +382,6 @@ | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) | _ => error ("no type variables allowed")) end - -(* 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 {* @@ -609,73 +443,6 @@ ML {* symmetric (eq_reflection OF @{thms id_def}) *} 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 instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => let val pat = Drule.strip_imp_concl (cprop_of thm) @@ -801,19 +568,6 @@ ]) *} -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 -*} - section {* Cleaning the goal *} @@ -854,22 +608,6 @@ 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) -*} - ML {* fun findaps_all rty tm = case tm of @@ -882,83 +620,6 @@ fun findaps rty tm = distinct (op =) (findaps_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 applic_prs lthy rty qty absrep ty = @@ -1035,76 +696,6 @@ *} -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 -*} (******************************************) (******************************************) @@ -1461,70 +1052,6 @@ *} 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 -*} - -ML {* fun inst_spec ctrm = let val cty = ctyp_of_term ctrm