# HG changeset patch # User Christian Urban # Date 1261058313 -3600 # Node ID 3104d62e7a16f685765a118ca9e17d4d50da4e07 # Parent c129354f2ff68a6699c00e78d6c9608f36ee0620 moved the QuotMain code into two ML-files diff -r c129354f2ff6 -r 3104d62e7a16 Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/Examples/FSet.thy Thu Dec 17 14:58:33 2009 +0100 @@ -359,7 +359,7 @@ apply(regularize) apply(rule fun_rel_id_asm) apply(subst babs_simp) -apply(tactic {* quotient_tac @{context} 1 *}) +apply(tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) apply(rule fun_rel_id_asm) apply(rule impI) apply(rule mp[OF eq_imp_rel[OF fset_equivp]]) diff -r c129354f2ff6 -r 3104d62e7a16 Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/Examples/IntEx.thy Thu Dec 17 14:58:33 2009 +0100 @@ -135,13 +135,13 @@ done lemma "PLUS a = PLUS a" -apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) +apply(lifting_setup test2) apply(rule impI) apply(rule ballI) apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) apply(simp only: in_respects) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) +apply(injection) +apply(cleaning) done lemma test3: "my_plus = my_plus" @@ -149,7 +149,7 @@ done lemma "PLUS = PLUS" -apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) +apply(lifting_setup test3) apply(rule impI) apply(rule plus_rsp) apply(injection) @@ -158,10 +158,7 @@ lemma "PLUS a b = PLUS b a" -apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) +apply(lifting plus_sym_pre) done lemma plus_assoc_pre: @@ -173,10 +170,7 @@ done lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" -apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) +apply(lifting plus_assoc_pre) done lemma int_induct_raw: @@ -212,10 +206,7 @@ sorry lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" -apply(lifting_setup ho_tst2) -apply(regularize) -apply(injection) -apply(cleaning) +apply(lifting ho_tst2) done lemma ho_tst3: "foldl f (s::nat \ nat) ([]::(nat \ nat) list) = s" @@ -236,46 +227,6 @@ lemma lam_tst2: "(\(y :: nat \ nat). y) = (\(x :: nat \ nat). x)" by simp -(* test about lifting identity equations *) - -ML {* -(* helper code from QuotMain *) -val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} -val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} -val simproc = Simplifier.simproc_i @{theory} "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) -val simpset = (mk_minimal_ss @{context}) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv} - addsimprocs [simproc] addSolver equiv_solver -*} - -(* What regularising does *) -(*========================*) - -(* 0. preliminary simplification step *) -thm ball_reg_eqv bex_reg_eqv (* of no use: babs_reg_eqv *) - ball_reg_eqv_range bex_reg_eqv_range -(* 1. first two rtacs *) -thm ball_reg_right bex_reg_left -(* 2. monos *) -(* 3. commutation rules *) -thm ball_all_comm bex_ex_comm -(* 4. then rel-equality *) -thm eq_imp_rel -(* 5. then simplification like 0 *) -(* finally jump to 1 *) - - -(* What cleaning does *) -(*====================*) - -(* 1. conversion *) -thm lambda_prs -(* 2. simplification with *) -thm all_prs ex_prs -(* 3. Simplification with *) -thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep -(* 4. Test for refl *) - lemma shows "equivp (op \)" and "equivp ((op \) ===> (op \))" @@ -295,11 +246,9 @@ done lemma "(\(y :: my_int). y) = (\(x :: my_int). x)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *}) +apply(lifting lam_tst3a) apply(rule impI) apply(rule lam_tst3a_reg) -apply(tactic {* all_inj_repabs_tac @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) done lemma lam_tst3b: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" diff -r c129354f2ff6 -r 3104d62e7a16 Quot/Examples/LamEx.thy --- a/Quot/Examples/LamEx.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/Examples/LamEx.thy Thu Dec 17 14:58:33 2009 +0100 @@ -1,5 +1,5 @@ theory LamEx -imports Nominal "../QuotList" +imports Nominal "../QuotMain" "../QuotList" begin atom_decl name @@ -165,46 +165,46 @@ lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" -apply (tactic {* lift_tac @{context} @{thm pi_var_com} 1 *}) +apply (lifting pi_var_com) done lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" -apply (tactic {* lift_tac @{context} @{thm pi_app_com} 1 *}) +apply (lifting pi_app_com) done lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" -apply (tactic {* lift_tac @{context} @{thm pi_lam_com} 1 *}) +apply (lifting pi_lam_com) done lemma fv_var: "fv (Var (a\name)) = {a}" -apply (tactic {* lift_tac @{context} @{thm rfv_var} 1 *}) +apply (lifting rfv_var) done lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" -apply (tactic {* lift_tac @{context} @{thm rfv_app} 1 *}) +apply (lifting rfv_app) done lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" -apply (tactic {* lift_tac @{context} @{thm rfv_lam} 1 *}) +apply (lifting rfv_lam) done lemma a1: "(a\name) = (b\name) \ Var a = Var b" -apply (tactic {* lift_tac @{context} @{thm a1} 1 *}) +apply (lifting a1) done lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" -apply (tactic {* lift_tac @{context} @{thm a2} 1 *}) +apply (lifting a2) done lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" -apply (tactic {* lift_tac @{context} @{thm a3} 1 *}) +apply (lifting a3) done lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" -apply (tactic {* lift_tac @{context} @{thm alpha.cases} 1 *}) +apply (lifting alpha.cases) done lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); @@ -212,16 +212,16 @@ \(x\lam) (a\name) (b\name) xa\lam. \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ \ qxb qx qxa" -apply (tactic {* lift_tac @{context} @{thm alpha.induct} 1 *}) +apply (lifting alpha.induct) done lemma var_inject: "(Var a = Var b) = (a = b)" -apply (tactic {* lift_tac @{context} @{thm rvar_inject} 1 *}) +apply (lifting rvar_inject) done lemma lam_induct:" \\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); \name lam. P lam \ P (Lam name lam)\ \ P lam" -apply (tactic {* lift_tac @{context} @{thm rlam.induct} 1 *}) +apply (lifting rlam.induct) done lemma var_supp: diff -r c129354f2ff6 -r 3104d62e7a16 Quot/QuotMain.thy --- a/Quot/QuotMain.thy Wed Dec 16 14:28:48 2009 +0100 +++ b/Quot/QuotMain.thy Thu Dec 17 14:58:33 2009 +0100 @@ -3,6 +3,8 @@ uses ("quotient_info.ML") ("quotient_typ.ML") ("quotient_def.ML") + ("quotient_term.ML") + ("quotient_tacs.ML") begin locale QUOT_TYPE = @@ -107,36 +109,31 @@ (* lifting of constants *) use "quotient_def.ML" -section {* Simset setup *} +(* the translation functions *) +use "quotient_term.ML" -(* Since HOL_basic_ss is too "big" for us, *) -(* we set up our own minimal simpset. *) -ML {* -fun mk_minimal_ss ctxt = - Simplifier.context ctxt empty_ss - setsubgoaler asm_simp_tac - setmksimps (mksimps []) -*} +(* tactics *) +lemma eq_imp_rel: + "equivp R ==> a = b --> R a b" +by (simp add: equivp_reflp) -ML {* -fun OF1 thm1 thm2 = thm2 RS thm1 -*} +definition + "QUOT_TRUE x \ True" -(* various tactic combinators *) -ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) -*} +lemma quot_true_dests: + shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" + and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" + and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" + and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" +by (simp_all add: QUOT_TRUE_def ext) -ML {* -(* prints warning, if goal is unsolved *) -fun WARN (tac, msg) i st = - case Seq.pull ((SOLVES' tac) i st) of - NONE => (warning msg; Seq.single st) - | seqcell => Seq.make (fn () => seqcell) +lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" +by (simp add: QUOT_TRUE_def) -fun RANGE_WARN xs = RANGE (map WARN xs) -*} +lemma regularize_to_injection: "(QUOT_TRUE l \ y) \ (l = r) \ y" + by(auto simp add: QUOT_TRUE_def) +use "quotient_tacs.ML" section {* Atomize Infrastructure *} @@ -160,16 +157,6 @@ then show "A \ B" by (rule eq_reflection) qed -ML {* -fun atomize_thm thm = -let - val thm' = Thm.freezeT (forall_intr_vars thm) - val thm'' = ObjectLogic.atomize (cprop_of thm') -in - @{thm equal_elim_rule1} OF [thm'', thm'] -end -*} - section {* Infrastructure about id *} lemmas [id_simps] = @@ -177,902 +164,6 @@ id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] -section {* Computation of the Regularize Goal *} - -(* -Regularizing an rtrm means: - - quantifiers over a type that needs lifting are replaced by - bounded quantifiers, for example: - \x. P \ \x \ (Respects R). P / All (Respects R) P - - the relation R is given by the rty and qty; - - - abstractions over a type that needs lifting are replaced - by bounded abstractions: - \x. P \ Ball (Respects R) (\x. P) - - - equalities over the type being lifted are replaced by - corresponding relations: - A = B \ A \ B - - example with more complicated types of A, B: - A = B \ (op = \ op \) A B -*) - -ML {* -(* builds the relation that is the argument of respects *) -fun mk_resp_arg lthy (rty, qty) = -let - val thy = ProofContext.theory_of lthy -in - if rty = qty - then HOLogic.eq_const rty - else - case (rty, qty) of - (Type (s, tys), Type (s', tys')) => - if s = s' - then let - val SOME map_info = maps_lookup thy s - val args = map (mk_resp_arg lthy) (tys ~~ tys') - in - list_comb (Const (#relfun map_info, dummyT), args) - end - else let - val SOME qinfo = quotdata_lookup_thy thy s' - (* FIXME: check in this case that the rty and qty *) - (* FIXME: correspond to each other *) - val (s, _) = dest_Const (#rel qinfo) - (* FIXME: the relation should only be the string *) - (* FIXME: and the type needs to be calculated as below; *) - (* FIXME: maybe one should actually have a term *) - (* FIXME: and one needs to force it to have this type *) - in - Const (s, rty --> rty --> @{typ bool}) - end - | _ => HOLogic.eq_const dummyT - (* FIXME: check that the types correspond to each other? *) -end -*} - -ML {* -val mk_babs = Const (@{const_name Babs}, dummyT) -val mk_ball = Const (@{const_name Ball}, dummyT) -val mk_bex = Const (@{const_name Bex}, dummyT) -val mk_resp = Const (@{const_name Respects}, dummyT) -*} - -ML {* -(* - applies f to the subterm of an abstraction, *) -(* otherwise to the given term, *) -(* - used by regularize, therefore abstracted *) -(* variables do not have to be treated specially *) - -fun apply_subt f trm1 trm2 = - case (trm1, trm2) of - (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') - | _ => f trm1 trm2 - -(* the major type of All and Ex quantifiers *) -fun qnt_typ ty = domain_type (domain_type ty) -*} - -ML {* -(* produces a regularized version of rtrm *) -(* - the result is contains dummyT *) -(* - does not need any special treatment of *) -(* bound variables *) - -fun regularize_trm lthy rtrm qtrm = - case (rtrm, qtrm) of - (Abs (x, ty, t), Abs (x', ty', t')) => - let - val subtrm = Abs(x, ty, regularize_trm lthy t t') - in - if ty = ty' then subtrm - else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm - end - - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - in - if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm - else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - in - if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm - else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (* equalities need to be replaced by appropriate equivalence relations *) - (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => - if ty = ty' then rtrm - else mk_resp_arg lthy (domain_type ty, domain_type ty') - - | (* in this case we check whether the given equivalence relation is correct *) - (rel, Const (@{const_name "op ="}, ty')) => - let - val exc = LIFT_MATCH "regularise (relation mismatch)" - val rel_ty = (fastype_of rel) handle TERM _ => raise exc - val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') - in - if rel' = rel then rtrm else raise exc - end - - | (_, Const _) => - let - fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) - | same_name _ _ = false - (* TODO/FIXME: This test is not enough. *) - (* Why? *) - (* Because constants can have the same name but not be the same - constant. All overloaded constants have the same name but because - of different types they do differ. - - This code will let one write a theorem where plus on nat is - matched to plus on int, even if the latter is defined differently. - - This would result in hard to understand failures in injection and - cleaning. *) - (* cu: if I also test the type, then something else breaks *) - in - if same_name rtrm qtrm then rtrm - else - let - val thy = ProofContext.theory_of lthy - val qtrm_str = Syntax.string_of_term lthy qtrm - val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") - val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") - val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 - in - if Pattern.matches thy (rtrm', rtrm) - then rtrm else raise exc2 - end - end - - | (t1 $ t2, t1' $ t2') => - (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') - - | (Free (x, ty), Free (x', ty')) => - (* this case cannot arrise as we start with two fully atomized terms *) - raise (LIFT_MATCH "regularize (frees)") - - | (Bound i, Bound i') => - if i = i' then rtrm - else raise (LIFT_MATCH "regularize (bounds mismatch)") - - | _ => - let - val rtrm_str = Syntax.string_of_term lthy rtrm - val qtrm_str = Syntax.string_of_term lthy qtrm - in - raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) - end -*} - -section {* Regularize Tactic *} - -ML {* -fun equiv_tac ctxt = - REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) - -fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) -val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac -*} - -ML {* -fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) -*} - -ML {* -fun matching_prs thy pat trm = -let - val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ - val tenv = Vartab.dest (Envir.term_env env) - val tyenv = Vartab.dest (Envir.type_env env) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end -*} - -ML {* -fun calculate_instance ctxt thm redex R1 R2 = -let - val thy = ProofContext.theory_of ctxt - val goal = Const (@{const_name "equivp"}, dummyT) $ R2 - |> Syntax.check_term ctxt - |> HOLogic.mk_Trueprop - val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) - val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) - val R1c = cterm_of thy R1 - val thmi = Drule.instantiate' [] [SOME R1c] thm - val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) -in - SOME thm2 -end -handle _ => NONE -(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) -*} - -ML {* -fun ball_bex_range_simproc ss redex = -let - val ctxt = Simplifier.the_context ss -in - case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 - - | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 - | _ => NONE -end -*} - -lemma eq_imp_rel: - shows "equivp R \ a = b \ R a b" -by (simp add: equivp_reflp) - -ML {* -(* test whether DETERM makes any difference *) -fun quotient_tac ctxt = SOLVES' - (REPEAT_ALL_NEW (FIRST' - [rtac @{thm identity_quotient}, - resolve_tac (quotient_rules_get ctxt)])) - -fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac -*} - -ML {* -fun solve_quotient_assum ctxt thm = - case Seq.pull (quotient_tac ctxt 1 thm) of - SOME (t, _) => t - | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" -*} - - -(* 0. preliminary simplification step according to *) -thm ball_reg_eqv bex_reg_eqv babs_reg_eqv - ball_reg_eqv_range bex_reg_eqv_range -(* 1. eliminating simple Ball/Bex instances*) -thm ball_reg_right bex_reg_left -(* 2. monos *) -(* 3. commutation rules for ball and bex *) -thm ball_all_comm bex_ex_comm -(* 4. then rel-equality (which need to be instantiated to avoid loops) *) -thm eq_imp_rel -(* 5. then simplification like 0 *) -(* finally jump back to 1 *) - -ML {* -fun regularize_tac ctxt = -let - val thy = ProofContext.theory_of ctxt - val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} - val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} - val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) - val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} - addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver - val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) -in - simp_tac simpset THEN' - REPEAT_ALL_NEW (CHANGED o FIRST' [ - resolve_tac @{thms ball_reg_right bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - resolve_tac @{thms ball_all_comm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simpset]) -end -*} - -section {* Calculation of the Injected Goal *} - -(* -Injecting repabs means: - - For abstractions: - * If the type of the abstraction doesn't need lifting we recurse. - * If it does we add RepAbs around the whole term and check if the - variable needs lifting. - * If it doesn't then we recurse - * If it does we recurse and put 'RepAbs' around all occurences - of the variable in the obtained subterm. This in combination - with the RepAbs above will let us change the type of the - abstraction with rewriting. - For applications: - * If the term is 'Respects' applied to anything we leave it unchanged - * If the term needs lifting and the head is a constant that we know - how to lift, we put a RepAbs and recurse - * If the term needs lifting and the head is a free applied to subterms - (if it is not applied we treated it in Abs branch) then we - put RepAbs and recurse - * Otherwise just recurse. -*) - -ML {* -fun mk_repabs lthy (T, T') trm = - Quotient_Def.get_fun repF lthy (T, T') - $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) -*} - -ML {* -(* bound variables need to be treated properly, *) -(* as the type of subterms need to be calculated *) -(* in the abstraction case *) - -fun inj_repabs_trm lthy (rtrm, qtrm) = - case (rtrm, qtrm) of - (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - in - mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) - end - - | (Abs (x, T, t), Abs (x', T', t')) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - val (y, s) = Term.dest_abs (x, T, t) - val (_, s') = Term.dest_abs (x', T', t') - val yvar = Free (y, T) - val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) - in - if rty = qty then result - else mk_repabs lthy (rty, qty) result - end - - | (t $ s, t' $ s') => - (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) - - | (Free (_, T), Free (_, T')) => - if T = T' then rtrm - else mk_repabs lthy (T, T') rtrm - - | (_, Const (@{const_name "op ="}, _)) => rtrm - - | (_, Const (_, T')) => - let - val rty = fastype_of rtrm - in - if rty = T' then rtrm - else mk_repabs lthy (rty, T') rtrm - end - - | _ => raise (LIFT_MATCH "injection") -*} - -section {* Injection Tactic *} - -definition - "QUOT_TRUE x \ True" - -ML {* -(* looks for QUOT_TRUE assumtions, and in case its argument *) -(* is an application, it returns the function and the argument *) -fun find_qt_asm asms = -let - fun find_fun trm = - case trm of - (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true - | _ => false -in - case find_first find_fun asms of - SOME (_ $ (_ $ (f $ a))) => SOME (f, a) - | _ => NONE -end -*} - -text {* -To prove that the regularised theorem implies the abs/rep injected, -we try: - - 1) theorems 'trans2' from the appropriate QUOT_TYPE - 2) remove lambdas from both sides: lambda_rsp_tac - 3) remove Ball/Bex from the right hand side - 4) use user-supplied RSP theorems - 5) remove rep_abs from the right side - 6) reflexivity of equality - 7) split applications of lifted type (apply_rsp) - 8) split applications of non-lifted type (cong_tac) - 9) apply extentionality - A) reflexivity of the relation - B) assumption - (Lambdas under respects may have left us some assumptions) - C) proving obvious higher order equalities by simplifying fun_rel - (not sure if it is still needed?) - D) unfolding lambda on one side - E) simplifying (= ===> =) for simpler respectfulness -*} - -lemma quot_true_dests: - shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" - and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" - and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" - and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" -by (simp_all add: QUOT_TRUE_def ext) - -lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" -by (simp add: QUOT_TRUE_def) - -lemma regularize_to_injection: "(QUOT_TRUE l \ y) \ (l = r) \ y" - by(auto simp add: QUOT_TRUE_def) - -ML {* -fun quot_true_simple_conv ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ x) => - let - val fx = fnctn x; - val thy = ProofContext.theory_of ctxt; - val cx = cterm_of thy x; - val cfx = cterm_of thy fx; - val cxt = ctyp_of thy (fastype_of x); - val cfxt = ctyp_of thy (fastype_of fx); - val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} - in - Conv.rewr_conv thm ctrm - end -*} - -ML {* -fun quot_true_conv ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ _) => - quot_true_simple_conv ctxt fnctn ctrm - | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun quot_true_tac ctxt fnctn = - CONVERSION - ((Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) -*} - -ML {* fun dest_comb (f $ a) = (f, a) *} -ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} -(* TODO: Can this be done easier? *) -ML {* -fun unlam t = - case t of - (Abs a) => snd (Term.dest_abs a) - | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) -*} - -ML {* -fun dest_fun_type (Type("fun", [T, S])) = (T, S) - | dest_fun_type _ = error "dest_fun_type" -*} - -ML {* -val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -*} - -ML {* -(* we apply apply_rsp only in case if the type needs lifting, *) -(* which is the case if the type of the data in the QUOT_TRUE *) -(* assumption is different from the corresponding type in the goal *) -val apply_rsp_tac = - Subgoal.FOCUS (fn {concl, asms, context,...} => - let - val bare_concl = HOLogic.dest_Trueprop (term_of concl) - val qt_asm = find_qt_asm (map term_of asms) - in - case (bare_concl, qt_asm) of - (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => - if (fastype_of qt_fun) = (fastype_of f) - then no_tac - else - let - val ty_x = fastype_of x - val ty_b = fastype_of qt_arg - val ty_f = range_type (fastype_of f) - val thy = ProofContext.theory_of context - val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] - val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} - in - (rtac inst_thm THEN' quotient_tac context) 1 - end - | _ => no_tac - end) -*} - -thm equals_rsp - -ML {* -fun equals_rsp_tac R ctxt = -let - val ty = domain_type (fastype_of R); - val thy = ProofContext.theory_of ctxt - val thm = Drule.instantiate' - [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} -in - rtac thm THEN' quotient_tac ctxt -end -(* raised by instantiate' *) -handle THM _ => K no_tac - | TYPE _ => K no_tac - | TERM _ => K no_tac -*} - -ML {* -fun rep_abs_rsp_tac ctxt = - SUBGOAL (fn (goal, i) => - case (bare_concl goal) of - (rel $ _ $ (rep $ (abs $ _))) => - (let - val thy = ProofContext.theory_of ctxt; - val (ty_a, ty_b) = dest_fun_type (fastype_of abs); - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; - val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} - in - (rtac inst_thm THEN' quotient_tac ctxt) i - end - handle THM _ => no_tac | TYPE _ => no_tac) - | _ => no_tac) -*} - -ML {* -fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => -(case (bare_concl goal) of - (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) -| (Const (@{const_name "op ="},_) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} - - (* (R1 ===> op =) (Ball\) (Ball\) ----> \R1 x y\ \ (Ball\x) = (Ball\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) -| Const (@{const_name "op ="},_) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} - - (* (R1 ===> op =) (Bex\) (Bex\) ----> \R1 x y\ \ (Bex\x) = (Bex\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - -| (_ $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] - -| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => - (rtac @{thm refl} ORELSE' - (equals_rsp_tac R ctxt THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) - - (* reflexivity of operators arising from Cong_tac *) -| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} - - (* respectfulness of constants; in particular of a simple relation *) -| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) - => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt - - (* R (\) (Rep (Abs \)) ----> R (\) (\) *) - (* observe ---> *) -| _ $ _ $ _ - => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) - ORELSE' rep_abs_rsp_tac ctxt - -| _ => K no_tac -) i) -*} - -ML {* -fun inj_repabs_step_tac ctxt rel_refl = - (FIRST' [ - inj_repabs_tac_match ctxt, - (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) - - apply_rsp_tac ctxt THEN' - RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], - - (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) - (* merge with previous tactic *) - Cong_Tac.cong_tac @{thm cong} THEN' - RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], - - (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) - rtac @{thm ext} THEN' quot_true_tac ctxt unlam, - - (* resolving with R x y assumptions *) - atac, - - (* reflexivity of the basic relations *) - (* R \ \ *) - resolve_tac rel_refl]) -*} - -ML {* -fun inj_repabs_tac ctxt = -let - val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) -in - inj_repabs_step_tac ctxt rel_refl -end - -fun all_inj_repabs_tac ctxt = - REPEAT_ALL_NEW (inj_repabs_tac ctxt) -*} - -section {* Cleaning of the Theorem *} - -ML {* -(* expands all fun_maps, except in front of bound variables *) - -fun fun_map_simple_conv xs ctxt ctrm = - case (term_of ctrm) of - ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => - if (member (op=) xs h) - then Conv.all_conv ctrm - else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm - | _ => Conv.all_conv ctrm - -fun fun_map_conv xs ctxt ctrm = - case (term_of ctrm) of - _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv - fun_map_simple_conv xs ctxt) ctrm - | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm - | _ => Conv.all_conv ctrm - -fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) -*} - -ML {* -fun mk_abs u i t = - if incr_boundvars i u aconv t then Bound i - else (case t of - t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) - | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') - | Bound j => if i = j then error "make_inst" else t - | _ => t) - -fun make_inst lhs t = -let - val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; - val _ $ (Abs (_, _, (_ $ g))) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end - -fun make_inst_id lhs t = -let - val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; - val _ $ (Abs (_, _, g)) = t; -in - (f, Abs ("x", T, mk_abs u 0 g)) -end -*} - -ML {* -(* Simplifies a redex using the 'lambda_prs' theorem. *) -(* First instantiates the types and known subterms. *) -(* Then solves the quotient assumptions to get Rep2 and Abs1 *) -(* Finally instantiates the function f using make_inst *) -(* If Rep2 is identity then the pattern is simpler and make_inst_id is used *) -fun lambda_prs_simple_conv ctxt ctrm = - case (term_of ctrm) of - (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => - (let - val thy = ProofContext.theory_of ctxt - val (ty_b, ty_a) = dest_fun_type (fastype_of r1) - val (ty_c, ty_d) = dest_fun_type (fastype_of a2) - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] - val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] - val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} - val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] - val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te - val make_inst = if ty_c = ty_d then make_inst_id else make_inst - val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) - val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts - in - Conv.rewr_conv ti ctrm - end - handle _ => Conv.all_conv ctrm) - | _ => Conv.all_conv ctrm -*} - -ML {* -val lambda_prs_conv = - More_Conv.top_conv lambda_prs_simple_conv - -fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) -*} - -(* 1. folding of definitions and preservation lemmas; *) -(* and simplification with *) -thm babs_prs all_prs ex_prs -(* 2. unfolding of ---> in front of everything, except *) -(* bound variables (this prevents lambda_prs from *) -(* becoming stuck *) -thm fun_map.simps -(* 3. simplification with *) -thm lambda_prs -(* 4. simplification with *) -thm Quotient_abs_rep Quotient_rel_rep id_simps -(* 5. Test for refl *) - -ML {* -fun clean_tac lthy = - let - val thy = ProofContext.theory_of lthy; - val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) - - val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} - val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) - fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver - in - EVERY' [simp_tac (simps thms1), - fun_map_tac lthy, - lambda_prs_tac lthy, - simp_tac (simps thms2), - TRY o rtac refl] - end -*} - -section {* Tactic for Genralisation of Free Variables in a Goal *} - -ML {* -fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} - -fun inst_spec_tac ctrms = - EVERY' (map (dtac o inst_spec) ctrms) - -fun all_list xs trm = - fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm - -fun apply_under_Trueprop f = - HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop - -fun gen_frees_tac ctxt = - SUBGOAL (fn (concl, i) => - let - val thy = ProofContext.theory_of ctxt - val vrs = Term.add_frees concl [] - val cvrs = map (cterm_of thy o Free) vrs - val concl' = apply_under_Trueprop (all_list vrs) concl - val goal = Logic.mk_implies (concl', concl) - val rule = Goal.prove ctxt [] [] goal - (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) - in - rtac rule i - end) -*} - -section {* The General Shape of the Lifting Procedure *} - -(* - A is the original raw theorem *) -(* - B is the regularized theorem *) -(* - C is the rep/abs injected version of B *) -(* - D is the lifted theorem *) -(* *) -(* - 1st prem is the regularization step *) -(* - 2nd prem is the rep/abs injection step *) -(* - 3rd prem is the cleaning part *) -(* *) -(* the QUOT_TRUE premise in 2 records the lifted theorem *) - -ML {* -val lifting_procedure = - @{lemma "\A; - A \ B; - QUOT_TRUE D \ B = C; - C = D\ \ D" - by (simp add: QUOT_TRUE_def)} -*} - -ML {* -fun lift_match_error ctxt fun_str rtrm qtrm = -let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, - "", "does not match with original theorem", rtrm_str] -in - error msg -end -*} - -ML {* -fun procedure_inst ctxt rtrm qtrm = -let - val thy = ProofContext.theory_of ctxt - val rtrm' = HOLogic.dest_Trueprop rtrm - val qtrm' = HOLogic.dest_Trueprop qtrm - val reg_goal = - Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val inj_goal = - Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm -in - Drule.instantiate' [] - [SOME (cterm_of thy rtrm'), - SOME (cterm_of thy reg_goal), - NONE, - SOME (cterm_of thy inj_goal)] lifting_procedure -end -*} - -ML {* -(* the tactic leaves three subgoals to be proved *) -fun procedure_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (goal, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) - in - (rtac rule THEN' rtac rthm') i - end) -*} - -section {* Automatic Proofs *} - - -ML {* -local - -val msg1 = "Regularize proof failed." -val msg2 = cat_lines ["Injection proof failed.", - "This is probably due to missing respects lemmas.", - "Try invoking the injection method manually to see", - "which lemmas are missing."] -val msg3 = "Cleaning proof failed." - -in - -fun lift_tac ctxt rthm = - procedure_tac ctxt rthm - THEN' RANGE_WARN - [(regularize_tac ctxt, msg1), - (all_inj_repabs_tac ctxt, msg2), - (clean_tac ctxt, msg3)] - -end -*} - section {* Methods / Interface *} ML {* @@ -1084,23 +175,23 @@ *} method_setup lifting = - {* Attrib.thm >> (mk_method1 lift_tac) *} + {* Attrib.thm >> (mk_method1 Quotient_Tacs.lift_tac) *} {* Lifting of theorems to quotient types. *} method_setup lifting_setup = - {* Attrib.thm >> (mk_method1 procedure_tac) *} + {* Attrib.thm >> (mk_method1 Quotient_Tacs.procedure_tac) *} {* Sets up the three goals for the lifting procedure. *} method_setup regularize = - {* Scan.succeed (mk_method2 regularize_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.regularize_tac) *} {* Proves automatically the regularization goals from the lifting procedure. *} method_setup injection = - {* Scan.succeed (mk_method2 all_inj_repabs_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *} {* Proves automatically the rep/abs injection goals from the lifting procedure. *} method_setup cleaning = - {* Scan.succeed (mk_method2 clean_tac) *} + {* Scan.succeed (mk_method2 Quotient_Tacs.clean_tac) *} {* Proves automatically the cleaning goals from the lifting procedure. *} end diff -r c129354f2ff6 -r 3104d62e7a16 Quot/quotient_tacs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/quotient_tacs.ML Thu Dec 17 14:58:33 2009 +0100 @@ -0,0 +1,619 @@ +signature QUOTIENT_TACS = +sig + val regularize_tac: Proof.context -> int -> tactic + val all_inj_repabs_tac: Proof.context -> int -> tactic + val clean_tac: Proof.context -> int -> tactic + val procedure_tac: Proof.context -> thm -> int -> tactic + val lift_tac: Proof.context ->thm -> int -> tactic + val quotient_tac: Proof.context -> int -> tactic +end; + +structure Quotient_Tacs: QUOTIENT_TACS = +struct + +(* Since HOL_basic_ss is too "big" for us, *) +(* we need to set up our own minimal simpset. *) +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) + + + +(* various helper functions *) +fun OF1 thm1 thm2 = thm2 RS thm1 + +(* makes sure a subgoal is solved *) +fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac) + +(* prints warning, if goal is unsolved *) +fun WARN (tac, msg) i st = + case Seq.pull ((SOLVES' tac) i st) of + NONE => (warning msg; Seq.single st) + | seqcell => Seq.make (fn () => seqcell) + +fun RANGE_WARN xs = RANGE (map WARN xs) + +fun atomize_thm thm = +let + val thm' = Thm.freezeT (forall_intr_vars thm) + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + @{thm equal_elim_rule1} OF [thm'', thm'] +end + + + + +(* Regularize Tactic *) + +fun equiv_tac ctxt = + REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) + +fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) +val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac + +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) + +fun matching_prs thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end + +fun calculate_instance ctxt thm redex R1 R2 = +let + val thy = ProofContext.theory_of ctxt + val goal = Const (@{const_name "equivp"}, dummyT) $ R2 + |> Syntax.check_term ctxt + |> HOLogic.mk_Trueprop + val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1) + val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) + val R1c = cterm_of thy R1 + val thmi = Drule.instantiate' [] [SOME R1c] thm + val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) +in + SOME thm2 +end +handle _ => NONE +(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *) + +fun ball_bex_range_simproc ss redex = +let + val ctxt = Simplifier.the_context ss +in + case redex of + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 + + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 + | _ => NONE +end + +(* test whether DETERM makes any difference *) +fun quotient_tac ctxt = SOLVES' + (REPEAT_ALL_NEW (FIRST' + [rtac @{thm identity_quotient}, + resolve_tac (quotient_rules_get ctxt)])) + +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) +val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac + +fun solve_quotient_assum ctxt thm = + case Seq.pull (quotient_tac ctxt 1 thm) of + SOME (t, _) => t + | _ => error "solve_quotient_assum failed. Maybe a quotient_thm is missing" + + +(* 0. preliminary simplification step according to *) +(* thm ball_reg_eqv bex_reg_eqv babs_reg_eqv *) +(* ball_reg_eqv_range bex_reg_eqv_range *) +(* *) +(* 1. eliminating simple Ball/Bex instances *) +(* thm ball_reg_right bex_reg_left *) +(* *) +(* 2. monos *) +(* 3. commutation rules for ball and bex *) +(* thm ball_all_comm bex_ex_comm *) +(* *) +(* 4. then rel-equality (which need to be *) +(* instantiated to avoid loops) *) +(* thm eq_imp_rel *) +(* *) +(* 5. then simplification like 0 *) +(* *) +(* finally jump back to 1 *) + +fun regularize_tac ctxt = +let + val thy = ProofContext.theory_of ctxt + val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} + val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} + val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) + val simpset = (mk_minimal_ss ctxt) + addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} + addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver + val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt) +in + simp_tac simpset THEN' + REPEAT_ALL_NEW (CHANGED o FIRST' [ + resolve_tac @{thms ball_reg_right bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + resolve_tac @{thms ball_all_comm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) +end + + + +(* Injection Tactic *) + +(* looks for QUOT_TRUE assumtions, and in case its parameter *) +(* is an application, it returns the function and the argument *) +fun find_qt_asm asms = +let + fun find_fun trm = + case trm of + (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true + | _ => false +in + case find_first find_fun asms of + SOME (_ $ (_ $ (f $ a))) => SOME (f, a) + | _ => NONE +end + +fun quot_true_simple_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ x) => + let + val fx = fnctn x; + val thy = ProofContext.theory_of ctxt; + val cx = cterm_of thy x; + val cfx = cterm_of thy fx; + val cxt = ctyp_of thy (fastype_of x); + val cfxt = ctyp_of thy (fastype_of fx); + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} + in + Conv.rewr_conv thm ctrm + end + +fun quot_true_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ _) => + quot_true_simple_conv ctxt fnctn ctrm + | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun quot_true_tac ctxt fnctn = + CONVERSION + ((Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) + +fun dest_comb (f $ a) = (f, a) +fun dest_bcomb ((_ $ l) $ r) = (l, r) + +(* TODO: Can this be done easier? *) +fun unlam t = + case t of + (Abs a) => snd (Term.dest_abs a) + | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) + +fun dest_fun_type (Type("fun", [T, S])) = (T, S) + | dest_fun_type _ = error "dest_fun_type" + +val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl + + +(* we apply apply_rsp only in case if the type needs lifting, *) +(* which is the case if the type of the data in the QUOT_TRUE *) +(* assumption is different from the corresponding type in the goal *) +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + let + val bare_concl = HOLogic.dest_Trueprop (term_of concl) + val qt_asm = find_qt_asm (map term_of asms) + in + case (bare_concl, qt_asm) of + (R2 $ (f $ x) $ (g $ y), SOME (qt_fun, qt_arg)) => + if (fastype_of qt_fun) = (fastype_of f) + then no_tac + else + let + val ty_x = fastype_of x + val ty_b = fastype_of qt_arg + val ty_f = range_type (fastype_of f) + val thy = ProofContext.theory_of context + val ty_inst = map (SOME o (ctyp_of thy)) [ty_x, ty_b, ty_f] + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} + in + (rtac inst_thm THEN' quotient_tac context) 1 + end + | _ => no_tac + end) + +fun equals_rsp_tac R ctxt = +let + val ty = domain_type (fastype_of R); + val thy = ProofContext.theory_of ctxt + val thm = Drule.instantiate' + [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp} +in + rtac thm THEN' quotient_tac ctxt +end +(* raised by instantiate' *) +handle THM _ => K no_tac + | TYPE _ => K no_tac + | TERM _ => K no_tac + + +fun rep_abs_rsp_tac ctxt = + SUBGOAL (fn (goal, i) => + case (bare_concl goal) of + (rel $ _ $ (rep $ (abs $ _))) => + (let + val thy = ProofContext.theory_of ctxt; + val (ty_a, ty_b) = dest_fun_type (fastype_of abs); + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; + val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; + val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} + in + (rtac inst_thm THEN' quotient_tac ctxt) i + end + handle THM _ => no_tac | TYPE _ => no_tac) + | _ => no_tac) + + +(* FIXME /TODO needs to be adapted *) +(* +To prove that the regularised theorem implies the abs/rep injected, +we try: + + 1) theorems 'trans2' from the appropriate QUOT_TYPE + 2) remove lambdas from both sides: lambda_rsp_tac + 3) remove Ball/Bex from the right hand side + 4) use user-supplied RSP theorems + 5) remove rep_abs from the right side + 6) reflexivity of equality + 7) split applications of lifted type (apply_rsp) + 8) split applications of non-lifted type (cong_tac) + 9) apply extentionality + A) reflexivity of the relation + B) assumption + (Lambdas under respects may have left us some assumptions) + C) proving obvious higher order equalities by simplifying fun_rel + (not sure if it is still needed?) + D) unfolding lambda on one side + E) simplifying (= ===> =) for simpler respectfulness +*) + + +fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => +(case (bare_concl goal) of + (* (R1 ===> R2) (%x...) (%x...) ----> [|R1 x y|] ==> R2 (...x) (...y) *) + (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Ball...) (Ball...) ----> (op =) (...) (...) *) +| (Const (@{const_name "op ="},_) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} + + (* (R1 ===> op =) (Ball...) (Ball...) ----> [|R1 x y|] ==> (Ball...x) = (Ball...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Bex...) (Bex...) ----> (op =) (...) (...) *) +| Const (@{const_name "op ="},_) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} + + (* (R1 ===> op =) (Bex...) (Bex...) ----> [|R1 x y|] ==> (Bex...x) = (Bex...y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + +| (_ $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] + +| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => + (rtac @{thm refl} ORELSE' + (equals_rsp_tac R ctxt THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])) + + (* reflexivity of operators arising from Cong_tac *) +| Const (@{const_name "op ="},_) $ _ $ _ => rtac @{thm refl} + + (* respectfulness of constants; in particular of a simple relation *) +| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) + => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt + + (* R (...) (Rep (Abs ...)) ----> R (...) (...) *) + (* observe fun_map *) +| _ $ _ $ _ + => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) + ORELSE' rep_abs_rsp_tac ctxt + +| _ => K no_tac +) i) + +fun inj_repabs_step_tac ctxt rel_refl = + FIRST' [ + inj_repabs_tac_match ctxt, + (* R (t $ ...) (t' $ ...) ----> apply_rsp provided type of t needs lifting *) + + apply_rsp_tac ctxt THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *) + (* merge with previous tactic *) + Cong_Tac.cong_tac @{thm cong} THEN' + RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)], + + (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *) + rtac @{thm ext} THEN' quot_true_tac ctxt unlam, + + (* resolving with R x y assumptions *) + atac, + + (* reflexivity of the basic relations *) + (* R ... ... *) + resolve_tac rel_refl] + +fun inj_repabs_tac ctxt = +let + val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) +in + inj_repabs_step_tac ctxt rel_refl +end + +fun all_inj_repabs_tac ctxt = + REPEAT_ALL_NEW (inj_repabs_tac ctxt) + + +(* Cleaning of the Theorem *) + + +(* expands all fun_maps, except in front of bound variables *) +fun fun_map_simple_conv xs ctrm = + case (term_of ctrm) of + ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => + if (member (op=) xs h) + then Conv.all_conv ctrm + else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_conv xs ctxt ctrm = + case (term_of ctrm) of + _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv + fun_map_simple_conv xs) ctrm + | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm + +fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) + +fun mk_abs u i t = + if incr_boundvars i u aconv t then Bound i + else (case t of + t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2) + | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t) + +fun make_inst lhs t = +let + val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs; + val _ $ (Abs (_, _, (_ $ g))) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +fun make_inst_id lhs t = +let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; +in + (f, Abs ("x", T, mk_abs u 0 g)) +end + +(* Simplifies a redex using the 'lambda_prs' theorem. *) +(* First instantiates the types and known subterms. *) +(* Then solves the quotient assumptions to get Rep2 and Abs1 *) +(* Finally instantiates the function f using make_inst *) +(* If Rep2 is identity then the pattern is simpler and *) +(* make_inst_id is used *) +fun lambda_prs_simple_conv ctxt ctrm = + case (term_of ctrm) of + (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => + (let + val thy = ProofContext.theory_of ctxt + val (ty_b, ty_a) = dest_fun_type (fastype_of r1) + val (ty_c, ty_d) = dest_fun_type (fastype_of a2) + val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} + val te = @{thm eq_reflection} OF [solve_quotient_assum ctxt (solve_quotient_assum ctxt lpi)] + val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te + val make_inst = if ty_c = ty_d then make_inst_id else make_inst + val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm) + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts + in + Conv.rewr_conv ti ctrm + end + handle _ => Conv.all_conv ctrm) + | _ => Conv.all_conv ctrm + +val lambda_prs_conv = + More_Conv.top_conv lambda_prs_simple_conv + +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) + + +(* 1. folding of definitions and preservation lemmas; *) +(* and simplification with *) +(* thm babs_prs all_prs ex_prs *) +(* *) +(* 2. unfolding of ---> in front of everything, except *) +(* bound variables (this prevents lambda_prs from *) +(* becoming stuck *) +(* thm fun_map.simps *) +(* *) +(* 3. simplification with *) +(* thm lambda_prs *) +(* *) +(* 4. simplification with *) +(* thm Quotient_abs_rep Quotient_rel_rep id_simps *) +(* *) +(* 5. Test for refl *) + +fun clean_tac lthy = + let + val thy = ProofContext.theory_of lthy; + val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) + (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *) + + val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs} + val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) + fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver + in + EVERY' [simp_tac (simps thms1), + fun_map_tac lthy, + lambda_prs_tac lthy, + simp_tac (simps thms2), + TRY o rtac refl] + end + + + +(* Tactic for Genralisation of Free Variables in a Goal *) + +fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + +fun inst_spec_tac ctrms = + EVERY' (map (dtac o inst_spec) ctrms) + +fun all_list xs trm = + fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm + +fun apply_under_Trueprop f = + HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop + +fun gen_frees_tac ctxt = + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) + + +(* The General Shape of the Lifting Procedure *) + +(* - A is the original raw theorem *) +(* - B is the regularized theorem *) +(* - C is the rep/abs injected version of B *) +(* - D is the lifted theorem *) +(* *) +(* - 1st prem is the regularization step *) +(* - 2nd prem is the rep/abs injection step *) +(* - 3rd prem is the cleaning part *) +(* *) +(* the QUOT_TRUE premise in 2 records the lifted theorem *) + +val lifting_procedure = + @{lemma "[|A; + A --> B; + QUOT_TRUE D ==> B = C; + C = D|] ==> D" + by (simp add: QUOT_TRUE_def)} + +fun lift_match_error ctxt fun_str rtrm qtrm = +let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, + "", "does not match with original theorem", rtrm_str] +in + error msg +end + + +fun procedure_inst ctxt rtrm qtrm = +let + val thy = ProofContext.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = + Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm + val inj_goal = + Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm +in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + NONE, + SOME (cterm_of thy inj_goal)] lifting_procedure +end + + +(* the tactic leaves three subgoals to be proved *) +fun procedure_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (goal, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of goal) + in + (rtac rule THEN' rtac rthm') i + end) + + +(* Automatic Proofs *) + +val msg1 = "Regularize proof failed." +val msg2 = cat_lines ["Injection proof failed.", + "This is probably due to missing respects lemmas.", + "Try invoking the injection method manually to see", + "which lemmas are missing."] +val msg3 = "Cleaning proof failed." + +fun lift_tac ctxt rthm = + procedure_tac ctxt rthm + THEN' RANGE_WARN + [(regularize_tac ctxt, msg1), + (all_inj_repabs_tac ctxt, msg2), + (clean_tac ctxt, msg3)] + + + +end; \ No newline at end of file diff -r c129354f2ff6 -r 3104d62e7a16 Quot/quotient_term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/quotient_term.ML Thu Dec 17 14:58:33 2009 +0100 @@ -0,0 +1,278 @@ +signature QUOTIENT_TERM = +sig + val regularize_trm: Proof.context -> term -> term -> term + val inj_repabs_trm: Proof.context -> (term * term) -> term +end; + +structure Quotient_Term: QUOTIENT_TERM = +struct + +(* +Regularizing an rtrm means: + + - Quantifiers over a type that need lifting are replaced + by bounded quantifiers, for example: + + All P ===> All (Respects R) P + + where the relation R is given by the rty and qty; + + - Abstractions over a type that needs lifting are replaced + by bounded abstractions: + + %x. P ===> Ball (Respects R) %x. P + + - Equalities over the type being lifted are replaced by + corresponding equivalence relations: + + A = B ===> R A B + + or + + A = B ===> (R ===> R) A B + + for more complicated types of A and B +*) + +(* builds the relation that is the argument of respects *) +fun mk_resp_arg lthy (rty, qty) = +let + val thy = ProofContext.theory_of lthy +in + if rty = qty + then HOLogic.eq_const rty + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then let + val SOME map_info = maps_lookup thy s + (* FIXME dont return an option, raise an exception *) + val args = map (mk_resp_arg lthy) (tys ~~ tys') + in + list_comb (Const (#relfun map_info, dummyT), args) + end + else let + val SOME qinfo = quotdata_lookup_thy thy s' + (* FIXME: check in this case that the rty and qty *) + (* FIXME: correspond to each other *) + val (s, _) = dest_Const (#rel qinfo) + (* FIXME: the relation should only be the string *) + (* FIXME: and the type needs to be calculated as below; *) + (* FIXME: maybe one should actually have a term *) + (* FIXME: and one needs to force it to have this type *) + in + Const (s, rty --> rty --> @{typ bool}) + end + | _ => HOLogic.eq_const dummyT + (* FIXME: check that the types correspond to each other? *) +end + +val mk_babs = Const (@{const_name Babs}, dummyT) +val mk_ball = Const (@{const_name Ball}, dummyT) +val mk_bex = Const (@{const_name Bex}, dummyT) +val mk_resp = Const (@{const_name Respects}, dummyT) + +(* - applies f to the subterm of an abstraction, *) +(* otherwise to the given term, *) +(* - used by regularize, therefore abstracted *) +(* variables do not have to be treated specially *) +fun apply_subt f trm1 trm2 = + case (trm1, trm2) of + (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t') + | _ => f trm1 trm2 + +(* the major type of All and Ex quantifiers *) +fun qnt_typ ty = domain_type (domain_type ty) + + +(* produces a regularized version of rtrm *) +(* *) +(* - the result is still contains dummyT *) +(* *) +(* - for regularisation we do not need any *) +(* special treatment of bound variables *) + +fun regularize_trm lthy rtrm qtrm = + case (rtrm, qtrm) of + (Abs (x, ty, t), Abs (_, ty', t')) => + let + val subtrm = Abs(x, ty, regularize_trm lthy t t') + in + if ty = ty' then subtrm + else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm + end + + | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm lthy) t t' + in + if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm + else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm lthy) t t' + in + if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm + else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (* equalities need to be replaced by appropriate equivalence relations *) + (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => + if ty = ty' then rtrm + else mk_resp_arg lthy (domain_type ty, domain_type ty') + + | (* in this case we check whether the given equivalence relation is correct *) + (rel, Const (@{const_name "op ="}, ty')) => + let + val exc = LIFT_MATCH "regularise (relation mismatch)" + val rel_ty = (fastype_of rel) handle TERM _ => raise exc + val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') + in + if rel' = rel then rtrm else raise exc + end + + | (_, Const _) => + let + fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*) + | same_name _ _ = false + (* TODO/FIXME: This test is not enough. *) + (* Why? *) + (* Because constants can have the same name but not be the same + constant. All overloaded constants have the same name but because + of different types they do differ. + + This code will let one write a theorem where plus on nat is + matched to plus on int, even if the latter is defined differently. + + This would result in hard to understand failures in injection and + cleaning. *) + (* cu: if I also test the type, then something else breaks *) + in + if same_name rtrm qtrm then rtrm + else + let + val thy = ProofContext.theory_of lthy + val qtrm_str = Syntax.string_of_term lthy qtrm + val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)") + val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)") + val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 + in + if Pattern.matches thy (rtrm', rtrm) + then rtrm else raise exc2 + end + end + + | (t1 $ t2, t1' $ t2') => + (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') + + | (Free (x, ty), Free (x', ty')) => + (* this case cannot arrise as we start with two fully atomized terms *) + raise (LIFT_MATCH "regularize (frees)") + + | (Bound i, Bound i') => + if i = i' then rtrm + else raise (LIFT_MATCH "regularize (bounds mismatch)") + + | _ => + let + val rtrm_str = Syntax.string_of_term lthy rtrm + val qtrm_str = Syntax.string_of_term lthy qtrm + in + raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) + end + + + +(* +Injecting of Rep/Abs means: + + For abstractions +: + * If the type of the abstraction doesn't need lifting we recurse. + + * If it needs lifting then we add Rep/Abs around the whole term and + check if the bound variable needs lifting. + + * If it does we recurse and put Rep/Abs around all occurences + of the variable in the obtained subterm. This in combination + with the Rep/Abs from above will let us change the type of + the abstraction with rewriting. + + For applications: + + * If the term is Respects applied to anything we leave it unchanged + + * If the term needs lifting and the head is a constant that we know + how to lift, we put a Rep/Abs and recurse + + * If the term needs lifting and the head is a Free applied to subterms + (if it is not applied we treated it in Abs branch) then we + put Rep/Abs and recurse + + * Otherwise just recurse. +*) + +fun mk_repabs lthy (T, T') trm = + Quotient_Def.get_fun repF lthy (T, T') + $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) + + +(* bound variables need to be treated properly, *) +(* as the type of subterms needs to be calculated *) + +fun inj_repabs_trm lthy (rtrm, qtrm) = + case (rtrm, qtrm) of + (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => + Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => + Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + in + mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))) + end + + | (Abs (x, T, t), Abs (x', T', t')) => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + val (y, s) = Term.dest_abs (x, T, t) + val (_, s') = Term.dest_abs (x', T', t') + val yvar = Free (y, T) + val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) + in + if rty = qty then result + else mk_repabs lthy (rty, qty) result + end + + | (t $ s, t' $ s') => + (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) + + | (Free (_, T), Free (_, T')) => + if T = T' then rtrm + else mk_repabs lthy (T, T') rtrm + + | (_, Const (@{const_name "op ="}, _)) => rtrm + + | (_, Const (_, T')) => + let + val rty = fastype_of rtrm + in + if rty = T' then rtrm + else mk_repabs lthy (rty, T') rtrm + end + + | _ => raise (LIFT_MATCH "injection") + +end; (* structure *) + +open Quotient_Term; + +