theory QuotMainimports QuotScript QuotList Proveuses ("quotient_info.ML") ("quotient.ML") ("quotient_def.ML")beginML {*let val parser = Args.context -- Scan.lift Args.name_source fun term_pat (ctxt, str) = str |> ProofContext.read_term_pattern ctxt |> ML_Syntax.print_term |> ML_Syntax.atomicin ML_Antiquote.inline "term_pat" (parser >> term_pat)end*}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 {* val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"}; val trm2 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (h (g x) ((g::nat\<Rightarrow>nat) x)))"}*}ML {*fun test trm = case trm of (_ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u))) => (1,f) | (_ $ (Abs (_, _, (f as (Var (_, _)) $ u)))) => (2,f) | (_ $ (Abs (_, _, (f $ u)))) => (3,f)*}ML {* test trm1 *}ML {* make_inst trm1 trm2 |> pairself (Syntax.string_of_term @{context}) |> pairself writeln*}locale QUOT_TYPE = fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" assumes equiv: "EQUIV R" and rep_prop: "\<And>y. \<exists>x. Rep y = R x" and rep_inverse: "\<And>x. Abs (Rep x) = x" and abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)" and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"begindefinition ABS::"'a \<Rightarrow> 'b"where "ABS x \<equiv> Abs (R x)"definition REP::"'b \<Rightarrow> 'a"where "REP a = Eps (Rep a)"lemma lem9: shows "R (Eps (R x)) = R x"proof - have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) then have "R x (Eps (R x))" by (rule someI) then show "R (Eps (R x)) = R x" using equiv unfolding EQUIV_def by simpqedtheorem thm10: shows "ABS (REP a) \<equiv> a" apply (rule eq_reflection) unfolding ABS_def REP_defproof - 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 "\<dots> = Abs (R x)" using lem9 by simp also have "\<dots> = Abs (Rep a)" using eq by simp also have "\<dots> = a" using rep_inverse by simp finally show "Abs (R (Eps (Rep a))) = a" by simpqedlemma REP_refl: shows "R (REP a) (REP a)"unfolding REP_defby (simp add: equiv[simplified EQUIV_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)donetheorem thm11: shows "R r r' = (ABS r = ABS r')"unfolding ABS_defby (simp only: equiv[simplified EQUIV_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: equiv[simplified EQUIV_def])donelemma R_trans: assumes ab: "R a b" and bc: "R b c" shows "R a c"proof - have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[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 TRANS_def by blastqedlemma R_sym: assumes ab: "R a b" shows "R b a"proof - have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp then show "R b a" using ab unfolding SYM_def by blastqedlemma R_trans2: assumes ac: "R a c" and bd: "R b d" shows "R a b = R c d"using ac bdby (blast intro: R_trans R_sym)lemma REPS_same: shows "R (REP a) (REP b) \<equiv> (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 "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto qed then show "R (REP a) (REP b) \<equiv> (a = b)" by simpqedend(* EQUALS_RSP is stronger *)lemma equiv_trans2: assumes e: "EQUIV R" and ac: "R a c" and bd: "R b d" shows "R a b = R c d"using ac bd eunfolding EQUIV_REFL_SYM_TRANS TRANS_def SYM_defby (blast)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)]]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"(* TODO: Consider defining it with an "if"; sth like: Babs p m = \<lambda>x. if x \<in> p then m x else undefined*)definition Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"where "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"section {* ATOMIZE *}lemma atomize_eqv[atomize]: shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"proof assume "A \<equiv> B" then show "Trueprop A \<equiv> Trueprop B" by unfoldnext assume *: "Trueprop A \<equiv> 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 "\<not>A" by fact then show "A = B" using * by auto qed then show "A \<equiv> B" by (rule eq_reflection)qedML {*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 \<equiv> id" by (rule eq_reflection) (simp add: prod_fun_def)lemma map_id: "map id \<equiv> id" apply (rule eq_reflection) apply (rule ext) apply (rule_tac list="x" in list.induct) apply (simp_all) donelemmas id_simps = FUN_MAP_I[THEN eq_reflection] id_apply[THEN eq_reflection] id_def[THEN eq_reflection,symmetric] prod_fun_id map_idML {*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 thmend *}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_linesin EVERY [tac i, my_print_tac ctxt before_msg i] thmendfun NDT ctxt s tac thm = tac thm *}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 (* cu: Changed the lookup\<dots>not sure whether this works *) (* 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 EQUIV_REFL} 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*}ML {*fun lookup_quot_consts defs = let fun dest_term (a $ b) = (a, b); val def_terms = map (snd o Logic.dest_equals o concl_of) defs; in map (fst o dest_Const o snd o dest_term) def_terms end*}section {* Regularization *} (*Regularizing an rtrm means: - quantifiers over a type that needs lifting are replaced by bounded quantifiers, for example: \<forall>x. P \<Longrightarrow> \<forall>x \<in> (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: \<lambda>x. P \<Longrightarrow> Ball (Respects R) (\<lambda>x. P) - equalities over the type being lifted are replaced by corresponding relations: A = B \<Longrightarrow> A \<approx> B example with more complicated types of A, B: A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) 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 lthyin 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 = regularize_trm lthy t t' in if ty = ty' then Abs (x, ty, 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 (* FIXME: Should = only be replaced, when fully applied? *) (* Then there must be a 2nd argument *) | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') => let val subtrm = regularize_trm lthy t t' in if ty = ty' then Const (@{const_name "op ="}, ty) $ subtrm else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm 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)") | (Const (s, ty), Const (s', ty')) => if s = s' andalso ty = ty' then rtrm else rtrm (* FIXME: check correspondence according to definitions *) | (rt, qt) => raise (LIFT_MATCH "regularize (default)")*}(*FIXME / TODO: needs to be adaptedTo 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 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q*)(* FIXME: they should be in in the new Isabelle *)lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"by blastlemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"by auto(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)ML {*fun equiv_tac rel_eqvs = REPEAT_ALL_NEW (FIRST' [resolve_tac rel_eqvs, rtac @{thm IDENTITY_EQUIV}, rtac @{thm LIST_EQUIV}])*}ML {*fun ball_reg_eqv_simproc rel_eqvs ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt in case redex of (ogl as ((Const (@{const_name "Ball"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => (let val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in SOME thm end handle _ => NONE ) | _ => NONE end*}ML {*fun bex_reg_eqv_simproc rel_eqvs ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt in case redex of (ogl as ((Const (@{const_name "Bex"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => (let val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) in SOME thm end handle _ => NONE ) | _ => NONE end*}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 ball_reg_eqv_range_simproc rel_eqvs ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt in case redex of (ogl as ((Const (@{const_name "Ball"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => (let val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val _ = tracing (Syntax.string_of_term ctxt glc); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm;(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl val _ = tracing "AAA"; val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); in SOME thm2 end handle _ => NONE ) | _ => NONE end*}ML {*fun bex_reg_eqv_range_simproc rel_eqvs ss redex = let val ctxt = Simplifier.the_context ss val thy = ProofContext.theory_of ctxt in case redex of (ogl as ((Const (@{const_name "Bex"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => (let val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val _ = tracing (Syntax.string_of_term ctxt glc); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]); val R1c = cterm_of thy R1; val thmi = Drule.instantiate' [] [SOME R1c] thm;(* val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *) val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl val _ = tracing "AAA"; val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi); val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); in SOME thm2 end handle _ => NONE ) | _ => NONE end*}lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"by (simp add: EQUIV_REFL)ML {*fun regularize_tac ctxt rel_eqvs = let val pat1 = [@{term "Ball (Respects R) P"}]; val pat2 = [@{term "Bex (Respects R) P"}]; val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; val thy = ProofContext.theory_of ctxt val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs)) val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs)) val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs)) val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs)) val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4] (* 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]) rel_eqvs in ObjectLogic.full_atomize_tac THEN' simp_tac simp_ctxt 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 simp_ctxt ]) 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 *)fun inj_repabs_trm lthy (rtrm, qtrm) =let val rty = fastype_of rtrm val qty = fastype_of qtrmin 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') => Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) | (Abs (x, T, t), Abs (x', T', t')) => let 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 | _ => let val (rhead, rargs) = strip_comb rtrm val (qhead, qargs) = strip_comb qtrm val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs) in case (rhead, qhead) of (Const _, Const _) => if rty = qty then list_comb (rhead, rargs') else mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) | (Free (x, T), Free (x', T')) => if T = T' then list_comb (rhead, rargs') else list_comb (mk_repabs lthy (T, T') rhead, rargs') | (Abs _, Abs _) => list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') | _ => raise (LIFT_MATCH "injection") endend*}section {* RepAbs Injection Tactic *}(* TODO: check if it still works with first_order_match *)ML {*fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => let val pat = Drule.strip_imp_concl (cprop_of thm) val insts = Thm.match (pat, concl) in rtac (Drule.instantiate insts thm) 1 end handle _ => no_tac)*}ML {*fun quotient_tac ctxt quot_thms = REPEAT_ALL_NEW (FIRST' [rtac @{thm FUN_QUOTIENT}, resolve_tac quot_thms, rtac @{thm IDENTITY_QUOTIENT}, (* For functional identity quotients, (op = ---> op =) *) (* TODO: think about the other way around, if we need to shorten the relation *) CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])*}lemma FUN_REL_I: assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" shows "(R1 ===> R2) f g"using a by simpML {*val lambda_res_tac = SUBGOAL (fn (goal, i) => case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} i | _ => no_tac)*}ML {*val weak_lambda_res_tac = SUBGOAL (fn (goal, i) => case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i | _ => no_tac)*}ML {*val ball_rsp_tac = SUBGOAL (fn (goal, i) => case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i |_ => no_tac)*}ML {*val bex_rsp_tac = SUBGOAL (fn (goal, i) => case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i | _ => no_tac)*}ML {* (* Legacy *)fun needs_lift (rty as Type (rty_s, _)) ty = case ty of Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys) | _ => false*}ML {*fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => case HOLogic.dest_Trueprop (term_of concl) of (_ $ (f $ _) $ (_ $ _)) => let val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); val insts = Thm.match (pat, concl) in if needs_lift rty (fastype_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 else no_tac end | _ => no_tac)*}ML {*fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)*}(*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_res_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*)definition "QUOT_TRUE x \<equiv> True"lemma quot_true_dests: shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" and QT_appL: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE A" and QT_appR: "QUOT_TRUE (A B) \<Longrightarrow> QUOT_TRUE B" and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"apply(simp_all add: QUOT_TRUE_def)donelemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P"by (simp add: QUOT_TRUE_def)lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"by (simp add: QUOT_TRUE_def)ML {*fun quot_true_tac ctxt fnctn = SUBGOAL (fn (gl, i) => let val thy = ProofContext.theory_of ctxt; fun find_fun trm = case trm of (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true | _ => false in case find_first find_fun (Logic.strip_imp_prems gl) of SOME (_ $ (_ $ x)) => let val fx = fnctn x; val ctrm1 = cterm_of thy x; val cty1 = ctyp_of thy (fastype_of x); val ctrm2 = cterm_of thy fx; val cty2 = ctyp_of thy (fastype_of fx); val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp} in dtac thm i end | NONE => error "quot_true_tac!" | _ => error "quot_true_tac!!" end)*}ML {*fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = (FIRST' [ (* "cong" rule of the of the relation / transitivity*) (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *) DT ctxt "1" (resolve_tac trans2), (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) NDT ctxt "2" (lambda_res_tac), (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) NDT ctxt "3" (rtac @{thm ball_rsp}), (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) NDT ctxt "4" (ball_rsp_tac), (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *) NDT ctxt "5" (rtac @{thm bex_rsp}), (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) NDT ctxt "6" (bex_rsp_tac), (* respectfulness of constants *) NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)), (* reflexivity of operators arising from Cong_tac *) NDT ctxt "8" (rtac @{thm refl}), (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *) (* observe ---> *) NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))), (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP provided type of t needs lifting *) NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))), (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong provided type of t does not need lifting *) (* merge with previous tactic *) NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}), (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *) NDT ctxt "C" (rtac @{thm ext}), (* reflexivity of the basic relations *) (* R \<dots> \<dots> *) NDT ctxt "D" (resolve_tac rel_refl), (* resolving with R x y assumptions *) NDT ctxt "E" (atac), (* (op =) ===> (op =) \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *) (* global simplification *) NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])*}ML {*fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 = REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)*}section {* Cleaning of the theorem *}(* TODO: This is slow *)ML {*fun allex_prs_tac ctxt quot = (EqSubst.eqsubst_tac ctxt [0] @{thms all_prs ex_prs}) THEN' (quotient_tac ctxt quot)*}(* Rewrites the term with LAMBDA_PRS thm.Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) with: fIt proves the QUOTIENT assumptions by calling quotient_tac *)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;fun lambda_prs_conv1 ctxt quot_thms ctrm = case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => let val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); val thy = ProofContext.theory_of ctxt; val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_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 tac = (compose_tac (false, lpi, 2)) THEN_ALL_NEW (quotient_tac ctxt quot_thms); val gc = Drule.strip_imp_concl (cprop_of lpi); val t = Goal.prove_internal [] gc (fn _ => tac 1) val te = @{thm eq_reflection} OF [t] val ts = MetaSimplifier.rewrite_rule @{thms id_simps} 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 _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) in Conv.rewr_conv ti ctrm end*}(* quot stands for the QUOTIENT theorems: *)(* could be potentially all of them *)ML {*fun lambda_prs_conv ctxt quot ctrm = case (term_of ctrm) of (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) => (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) then_conv (lambda_prs_conv1 ctxt quot)) ctrm | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm | _ => Conv.all_conv ctrm*}ML {*fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => CONVERSION (Conv.params_conv ~1 (fn ctxt => (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i)*}(* Cleaning the theorem consists of 6 kinds of rewrites. The first two need to be done before fun_map is unfolded - LAMBDA_PRS: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f - FORALL_PRS (and the same for exists: EXISTS_PRS) \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f - Rewriting with definitions from the argument defs NewConst ----> (rep ---> abs) oldConst - QUOTIENT_REL_REP: Rel (Rep x) (Rep y) ----> x = y - ABS_REP Abs (Rep x) ----> x - id_simps; fun_map.simps The first one is implemented as a conversion (fast). The second one is an EqSubst (slow). The rest are a simp_tac and are fast.*)thm all_prs ex_prsML {*fun clean_tac lthy quot defs = let val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) in EVERY' [lambda_prs_tac lthy quot, TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot), TRY o simp_tac simp_ctxt, 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 trmfun apply_under_Trueprop f = HOLogic.dest_Trueprop #> f #> HOLogic.mk_Truepropfun 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 \<Longrightarrow> B" and c: "B = C" and d: "C = D" shows "D" using a b c d by simpML {*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 inj_goal = Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrmin 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 lthy rthm = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => let val rthm' = atomize_thm rthm val rule = procedure_inst context (prop_of rthm') (term_of concl) in EVERY1 [rtac rule, rtac rthm'] end) lthy*}thm EQUIV_REFLthm equiv_trans2ML {*(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)fun lift_tac lthy rthm rel_eqv rty quot defs = ObjectLogic.full_atomize_tac THEN' gen_frees_tac lthy THEN' Subgoal.FOCUS (fn {context, concl, ...} => let val rthm' = atomize_thm rthm val rule = procedure_inst context (prop_of rthm') (term_of concl) val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv in EVERY1 [rtac rule, RANGE [rtac rthm', regularize_tac lthy rel_eqv, all_inj_repabs_tac lthy rty quot rel_refl trans2, clean_tac lthy quot defs]] end) lthy*}end