diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/QuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotMain.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,1191 @@ +theory QuotMain +imports QuotScript QuotList QuotProd Prove +uses ("quotient_info.ML") + ("quotient.ML") + ("quotient_def.ML") +begin + + +locale QUOT_TYPE = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equivp: "equivp R" + and rep_prop: "\y. \x. Rep y = R x" + and rep_inverse: "\x. Abs (Rep x) = x" + and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +begin + +definition + ABS::"'a \ 'b" +where + "ABS x \ Abs (R x)" + +definition + REP::"'b \ 'a" +where + "REP a = Eps (Rep a)" + +lemma lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equivp unfolding equivp_def by simp +qed + +theorem thm10: + shows "ABS (REP a) \ a" + apply (rule eq_reflection) + unfolding ABS_def REP_def +proof - + from rep_prop + obtain x where eq: "Rep a = R x" by auto + have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp + also have "\ = Abs (R x)" using lem9 by simp + also have "\ = Abs (Rep a)" using eq by simp + also have "\ = a" using rep_inverse by simp + finally + show "Abs (R (Eps (Rep a))) = a" by simp +qed + +lemma REP_refl: + shows "R (REP a) (REP a)" +unfolding REP_def +by (simp add: equivp[simplified equivp_def]) + +lemma lem7: + shows "(R x = R y) = (Abs (R x) = Abs (R y))" +apply(rule iffI) +apply(simp) +apply(drule rep_inject[THEN iffD2]) +apply(simp add: abs_inverse) +done + +theorem thm11: + shows "R r r' = (ABS r = ABS r')" +unfolding ABS_def +by (simp only: equivp[simplified equivp_def] lem7) + + +lemma REP_ABS_rsp: + shows "R f (REP (ABS g)) = R f g" + and "R (REP (ABS g)) f = R g f" +by (simp_all add: thm10 thm11) + +lemma Quotient: + "Quotient R ABS REP" +apply(unfold Quotient_def) +apply(simp add: thm10) +apply(simp add: REP_refl) +apply(subst thm11[symmetric]) +apply(simp add: equivp[simplified equivp_def]) +done + +lemma R_trans: + assumes ab: "R a b" + and bc: "R b c" + shows "R a c" +proof - + have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp + moreover have ab: "R a b" by fact + moreover have bc: "R b c" by fact + ultimately show "R a c" unfolding transp_def by blast +qed + +lemma R_sym: + assumes ab: "R a b" + shows "R b a" +proof - + have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp + then show "R b a" using ab unfolding symp_def by blast +qed + +lemma R_trans2: + assumes ac: "R a c" + and bd: "R b d" + shows "R a b = R c d" +using ac bd +by (blast intro: R_trans R_sym) + +lemma REPS_same: + shows "R (REP a) (REP b) \ (a = b)" +proof - + have "R (REP a) (REP b) = (a = b)" + proof + assume as: "R (REP a) (REP b)" + from rep_prop + obtain x y + where eqs: "Rep a = R x" "Rep b = R y" by blast + from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp + then have "R x (Eps (R y))" using lem9 by simp + then have "R (Eps (R y)) x" using R_sym by blast + then have "R y x" using lem9 by simp + then have "R x y" using R_sym by blast + then have "ABS x = ABS y" using thm11 by simp + then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp + then show "a = b" using rep_inverse by simp + next + assume ab: "a = b" + have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp + then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto + qed + then show "R (REP a) (REP b) \ (a = b)" by simp +qed + +end + +section {* type definition for the quotient type *} + +(* the auxiliary data for the quotient types *) +use "quotient_info.ML" + +declare [[map list = (map, list_rel)]] +declare [[map * = (prod_fun, prod_rel)]] +declare [[map "fun" = (fun_map, fun_rel)]] + +(* identity quotient is not here as it has to be applied first *) +lemmas [quotient_thm] = + fun_quotient list_quotient prod_quotient + +lemmas [quotient_rsp] = + quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp + +(* fun_map is not here since equivp is not true *) +(* TODO: option, ... *) +lemmas [quotient_equiv] = + identity_equivp list_equivp prod_equivp + + +ML {* maps_lookup @{theory} "List.list" *} +ML {* maps_lookup @{theory} "*" *} +ML {* maps_lookup @{theory} "fun" *} + + +(* definition of the quotient types *) +(* FIXME: should be called quotient_typ.ML *) +use "quotient.ML" + + +(* lifting of constants *) +use "quotient_def.ML" + +section {* Simset setup *} + +(* since HOL_basic_ss is too "big", we need to set up *) +(* our own minimal simpset *) +ML {* +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) +*} + +section {* atomize *} + +lemma atomize_eqv[atomize]: + shows "(Trueprop A \ Trueprop B) \ (A \ B)" +proof + assume "A \ B" + then show "Trueprop A \ Trueprop B" by unfold +next + assume *: "Trueprop A \ Trueprop B" + have "A = B" + proof (cases A) + case True + have "A" by fact + then show "A = B" using * by simp + next + case False + have "\A" by fact + then show "A = B" using * by auto + qed + 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 *} + +lemma prod_fun_id: "prod_fun id id \ id" + by (rule eq_reflection) (simp add: prod_fun_def) + +lemma map_id: "map id \ id" + apply (rule eq_reflection) + apply (rule ext) + apply (rule_tac list="x" in list.induct) + apply (simp_all) + done + +lemmas id_simps = + fun_map_id[THEN eq_reflection] + id_apply[THEN eq_reflection] + id_def[THEN eq_reflection,symmetric] + prod_fun_id map_id + +ML {* +fun simp_ids thm = + MetaSimplifier.rewrite_rule @{thms id_simps} thm +*} + +section {* Debugging infrastructure for testing tactics *} + +ML {* +fun my_print_tac ctxt s i thm = +let + val prem_str = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + handle Subscript => "no subgoal" + val _ = tracing (s ^ "\n" ^ prem_str) +in + Seq.single thm +end *} + +ML {* +fun DT ctxt s tac i thm = +let + val before_goal = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] + |> cat_lines +in + EVERY [tac i, my_print_tac ctxt before_msg i] thm +end + +fun NDT ctxt s tac thm = tac thm +*} + +section {* Matching of terms and types *} + +ML {* +fun matches_typ (ty, ty') = + case (ty, ty') of + (_, TVar _) => true + | (TFree x, TFree x') => x = x' + | (Type (s, tys), Type (s', tys')) => + s = s' andalso + if (length tys = length tys') + then (List.all matches_typ (tys ~~ tys')) + else false + | _ => false +*} + +ML {* +fun matches_term (trm, trm') = + case (trm, trm') of + (_, Var _) => true + | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') + | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') + | (Bound i, Bound j) => i = j + | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') + | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') + | _ => false +*} + +section {* Infrastructure for collecting theorems for starting the lifting *} + +ML {* +fun lookup_quot_data lthy qty = + let + val qty_name = fst (dest_Type qty) + val SOME quotdata = quotdata_lookup lthy qty_name + (* TODO: Should no longer be needed *) + val rty = Logic.unvarifyT (#rtyp quotdata) + val rel = #rel quotdata + val rel_eqv = #equiv_thm quotdata + val rel_refl = @{thm equivp_reflp} OF [rel_eqv] + in + (rty, rel, rel_refl, rel_eqv) + end +*} + +ML {* +fun lookup_quot_thms lthy qty_name = + let + val thy = ProofContext.theory_of lthy; + val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") + val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") + val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") + val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) + in + (trans2, reps_same, absrep, quot) + end +*} + +section {* Regularization *} + +(* +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 rtm *) +(* - the result is still not completely typed *) +(* - 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 (s, _)) => + let + fun same_name (Const (s, _)) (Const (s', _)) = (s = s') + | same_name _ _ = false + in + if same_name rtrm qtrm + then rtrm + else + let + fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") + val exc2 = LIFT_MATCH ("regularize (constant mismatch)") + val thy = ProofContext.theory_of lthy + val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) + in + if matches_term (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)") + + | (rt, qt) => + raise (LIFT_MATCH "regularize (default)") +*} + +ML {* +fun equiv_tac ctxt = + REPEAT_ALL_NEW (FIRST' + [resolve_tac (equiv_rules_get ctxt)]) +*} + +ML {* +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 {context,...} => equiv_tac context 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 can be 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) + +(* FIXME/TODO: How does regularizing work? *) +(* FIXME/TODO: needs to be adapted + +To prove that the raw theorem implies the regularised one, +we try in order: + + - Reflexivity of the relation + - Assumption + - Elimnating quantifiers on both sides of toplevel implication + - Simplifying implications on both sides of toplevel implication + - Ball (Respects ?E) ?P = All ?P + - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q + +*) +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} + addsimprocs [simproc] addSolver equiv_solver + (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) +in + ObjectLogic.full_atomize_tac THEN' + simp_tac simpset THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm ball_reg_right}, + rtac @{thm bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + rtac @{thm ball_all_comm}, + rtac @{thm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) +end +*} + +section {* Injections of rep and abses *} + +(* +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 _)) => + Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (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 + + (* FIXME: check here that rtrm is the corresponding definition for the const *) + | (_, 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 {* RepAbs Injection Tactic *} + +ML {* +fun quotient_tac ctxt = + REPEAT_ALL_NEW (FIRST' + [rtac @{thm identity_quotient}, + resolve_tac (quotient_rules_get ctxt)]) +*} + +(* solver for the simplifier *) +ML {* +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_assums ctxt thm = + let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in + thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] + end + handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" +*} + +(* Not used *) +(* It proves the Quotient assumptions by calling quotient_tac *) +ML {* +fun solve_quotient_assum i ctxt thm = + let + val tac = + (compose_tac (false, thm, i)) THEN_ALL_NEW + (quotient_tac ctxt); + val gc = Drule.strip_imp_concl (cprop_of thm); + in + Goal.prove_internal [] gc (fn _ => tac 1) + end + handle _ => error "solve_quotient_assum" +*} + +definition + "QUOT_TRUE x \ True" + +ML {* +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))) => (f, a) + | SOME _ => error "find_qt_asm: no pair" + | NONE => error "find_qt_asm: no assumption" + end +*} + +(* +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)" +apply(simp_all add: QUOT_TRUE_def ext) +done + +lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \ P) \ P" +by (simp add: QUOT_TRUE_def) + +lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" +by (simp add: QUOT_TRUE_def) + +ML {* +fun quot_true_conv1 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_conv1 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 {* +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + case ((HOLogic.dest_Trueprop (term_of concl))) of + ((R2 $ (f $ x) $ (g $ y))) => + (let + val (asmf, asma) = find_qt_asm (map term_of asms); + in + if (fastype_of asmf) = (fastype_of f) then no_tac else let + val ty_a = fastype_of x; + val ty_b = fastype_of asma; + val ty_c = range_type (type_of f); + val thy = ProofContext.theory_of context; + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; + val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} + val te = solve_quotient_assums context thm + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val thm = Drule.instantiate' [] t_inst te + in + compose_tac (false, thm, 2) 1 + end + end + handle ERROR "find_qt_asm: no pair" => no_tac) + | _ => no_tac) +*} +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => 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 thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} + val te = solve_quotient_assums ctxt thm + in + rtac te i + end + handle _ => no_tac) + | _ => no_tac) +*} + +ML {* +fun inj_repabs_tac_match ctxt trans2 = 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] + + (* reflexivity of operators arising from Cong_tac *) +| Const (@{const_name "op ="},_) $ _ $ _ + => rtac @{thm refl} ORELSE' + (resolve_tac trans2 THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) + +(* TODO: These patterns should should be somehow combined and generalized... *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name fun_rel}, _) $ _ $ _) + => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt + +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name prod_rel}, _) $ _ $ _) $ + (Const (@{const_name prod_rel}, _) $ _ $ _) + => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt + + (* 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 ---> *) +| _ $ _ $ _ + => rep_abs_rsp_tac ctxt + +| _ => error "inj_repabs_tac not a relation" +) i) +*} + +ML {* +fun inj_repabs_tac ctxt rel_refl trans2 = + (FIRST' [ + inj_repabs_tac_match ctxt trans2, + (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) + NDT ctxt "A" (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 *) + NDT ctxt "B" (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 =) (\) (\) *) + NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + (* resolving with R x y assumptions *) + NDT ctxt "E" (atac), + (* reflexivity of the basic relations *) + (* R \ \ *) + NDT ctxt "D" (resolve_tac rel_refl) + ]) +*} + +ML {* +fun all_inj_repabs_tac ctxt rel_refl trans2 = + REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) +*} + +section {* Cleaning of the theorem *} + +ML {* +fun make_inst lhs t = + let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; + fun mk_abs i t = + if incr_boundvars i u aconv t then Bound i + else (case t of + t1 $ t2 => mk_abs i t1 $ mk_abs i t2 + | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t); + in (f, Abs ("x", T, mk_abs 0 g)) end; +*} + +ML {* +fun lambda_prs_simple_conv ctxt ctrm = + case (term_of ctrm) of + ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (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_assums ctxt (solve_quotient_assums ctxt lpi)] + val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); + val tl = Thm.lhs_of ts + val (insp, inst) = make_inst (term_of tl) (term_of ctrm) + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts + val _ = if not (s = @{const_name "id"}) then + (tracing "lambda_prs"; + tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); + tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); + tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); + tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); + tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) + else () + in + Conv.rewr_conv ti ctrm + end + | _ => 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) +*} + +(* + Cleaning the theorem consists of three rewriting steps. + The first two need to be done before fun_map is unfolded + + 1) lambda_prs: + (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f + + Implemented as conversion since it is not a pattern. + + 2) all_prs (the same for exists): + Ball (Respects R) ((abs ---> id) f) ----> All f + + Rewriting with definitions from the argument defs + (rep ---> abs) oldConst ----> newconst + + 3) Quotient_rel_rep: + Rel (Rep x) (Rep y) ----> x = y + + Quotient_abs_rep: + Abs (Rep x) ----> x + + id_simps; fun_map.simps +*) + +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: shouldn't the definitions already be varified? *) + val thms1 = @{thms all_prs ex_prs} @ defs + val thms2 = @{thms eq_reflection[OF fun_map.simps]} + @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver + in + EVERY' [lambda_prs_tac lthy, + simp_tac (simps thms1), + simp_tac (simps thms2), + TRY o rtac refl] + end +*} + +section {* 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 {* General outline 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 *) +(* *) +(* - b is the regularization step *) +(* - c is the rep/abs injection step *) +(* - d is the cleaning part *) + +lemma lifting_procedure: + assumes a: "A" + and b: "A \ B" + and c: "B = C" + and d: "C = D" + shows "D" + using a b c d + by simp + +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 = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, + "and the lifted theorem\n", rtrm_str, "do not match"] +in + error (space_implode " " 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 _ = warning "Regularization done." + 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 + val _ = warning "RepAbs Injection done." +in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} +end +*} + +(* Left for debugging *) +ML {* +fun procedure_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (gl, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) + val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + in + (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i + end) +*} + +ML {* +(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) + +fun lift_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (gl, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) + val quotients = quotient_rules_get ctxt + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients + val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + in + (rtac rule THEN' + RANGE [rtac rthm', + regularize_tac ctxt, + rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, + clean_tac ctxt]) i + end) +*} + +end +