diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotMain.thy --- a/QuotMain.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1191 +0,0 @@ -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 -