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 pretty_helper aux env = env |> Vartab.dest |> map ((fn (s1, s2) => s1 ^ " := " ^ s2) o aux) |> commas |> enclose "[" "]" |> tracing*}ML {*fun pretty_env ctxt env =let fun get_trms (v, (T, t)) = (Var (v, T), t) val print = pairself (Syntax.string_of_term ctxt)in pretty_helper (print o get_trms) envend*}ML {* val pat = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). (?f) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}ML {* val trm = @{term_pat "\<lambda>(x::'a list \<Rightarrow> bool). (f::('a List.list \<Rightarrow> bool) \<Rightarrow> ('a List.list \<Rightarrow> bool) \<Rightarrow> 'b) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x) ((g::('a list \<Rightarrow> bool)\<Rightarrow>'a list \<Rightarrow> bool) x)"} *}ML {* val univ = let val init = Envir.empty 0in Unify.unifiers (@{theory}, init, [(pat, trm)])end*}ML {* val SOME ((u1, _), next) = Seq.pull univ *}ML {* val NEXT = Seq.pull next *}ML {* show_types := true *}ML {* pretty_env @{context} (Envir.term_env u1); *}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 simpqedendsection {* 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"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 Pure.equal_elim_rule1} OF [thm'', thm']end*}ML {* atomize_thm @{thm list.induct} *}section {* REGULARIZE *}(*Regularizing a theorem 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 - 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 appropriate relations: A = B \<Longrightarrow> A \<approx> B Example with more complicated types of A, B: A = B \<Longrightarrow> (op = \<Longrightarrow> op \<approx>) A BRegularizing is done in 3 phases: - First a regularized term is created - Next we prove that the original theorem implies the new one - Finally using MP we get the new theorem.To prove that the old theorem implies the new one, we firstatomize it and then try: - 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*)text {* tyRel takes a type and builds a relation that a quantifier over this type needs to respect. *}ML {*fun tyRel ty rty rel lthy = if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) then rel else (case ty of Type (s, tys) => let val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; val ty_out = ty --> ty --> @{typ bool}; val tys_out = tys_rel ---> ty_out; in (case (maps_lookup (ProofContext.theory_of lthy) s) of SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys) | NONE => HOLogic.eq_const ty ) end | _ => HOLogic.eq_const ty)*}(* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *)definition Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"where "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"(* TODO: Consider defining it with an "if"; sth like: Babs p m = \<lambda>x. if x \<in> p then m x else undefined*)ML {*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 mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})*}(* applies f to the subterm of an abstractions, otherwise to the given term *)ML {*fun apply_subt f trm = case trm of Abs (x, T, t) => let val (x', t') = Term.dest_abs (x, T, t) in Term.absfree (x', T, f t') end | _ => f trm*}(* FIXME: if there are more than one quotient, then you have to look up the relation *)ML {*fun my_reg lthy rel rty trm = case trm of Abs (x, T, t) => if (needs_lift rty T) then let val rrel = tyRel T rty rel lthy in (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) end else Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => let val ty1 = domain_type ty val ty2 = domain_type ty1 val rrel = tyRel T rty rel lthy in if (needs_lift rty T) then (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) else Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t end | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => let val ty1 = domain_type ty val ty2 = domain_type ty1 val rrel = tyRel T rty rel lthy in if (needs_lift rty T) then (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) else Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t end | Const (@{const_name "op ="}, ty) $ t => if needs_lift rty (fastype_of t) then (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *) else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) | _ => trm*}(* For polymorphic types we need to find the type of the Relation term. *)(* TODO: we assume that the relation is a Constant. Is this always true? *)ML {*fun my_reg_inst lthy rel rty trm = case rel of Const (n, _) => Syntax.check_term lthy (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)*}(*ML {* val r = Free ("R", dummyT); val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); val t2 = Syntax.check_term @{context} t; cterm_of @{theory} t2*}*)text {* Assumes that the given theorem is atomized *}ML {* fun build_regularize_goal thm rty rel lthy = Logic.mk_implies ((prop_of thm), (my_reg_inst lthy rel rty (prop_of thm)))*}lemma universal_twice: assumes *: "\<And>x. (P x \<longrightarrow> Q x)" shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"using * by autolemma implication_twice: assumes a: "c \<longrightarrow> a" assumes b: "a \<Longrightarrow> b \<longrightarrow> d" shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"using a b by autoML {*fun regularize thm rty rel rel_eqv rel_refl lthy = let val goal = build_regularize_goal thm rty rel lthy; fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' REPEAT_ALL_NEW (FIRST' [ rtac rel_refl, atac, rtac @{thm universal_twice}, (rtac @{thm impI} THEN' atac), rtac @{thm implication_twice}, EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])], (* For a = b \<longrightarrow> a \<approx> b *) (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]); val cthm = Goal.prove lthy [] [] goal (fn {context, ...} => tac context 1); in cthm OF [thm] end*}section {* RepAbs injection *}(*RepAbs injection is done in the following phases: 1) build_repabs_term inserts rep-abs pairs in the term 2) we prove the equality between the original theorem and this one 3) we use Pure.equal_elim_rule1 to get the new theorem.build_repabs_term does: 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.To prove that the old theorem implies the new one, we firstatomize it and then 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 extentionality10) reflexivity of the relation11) assumption (Lambdas under respects may have left us some assumptions)12) proving obvious higher order equalities by simplifying fun_rel (not sure if it is still needed?)13) unfolding lambda on one side14) simplifying (= ===> =) for simpler respectfullness*)(* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)ML {*fun exchange_ty lthy rty qty ty = let val thy = ProofContext.theory_of lthy in if Sign.typ_instance thy (ty, rty) then let val inst = Sign.typ_match thy (rty, ty) Vartab.empty in Envir.subst_type inst qty end else let val (s, tys) = dest_Type ty in Type (s, map (exchange_ty lthy rty qty) tys) end end handle TYPE _ => ty (* for dest_Type *)*}(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"axioms Rl_eq: "EQUIV Rl"quotient ql = "'a list" / "Rl" by (rule Rl_eq)ML {* ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})*}*)ML {*fun find_matching_types rty ty = if Type.raw_instance (Logic.varifyT ty, rty) then [ty] else let val (s, tys) = dest_Type ty in flat (map (find_matching_types rty) tys) end handle TYPE _ => []*}ML {*fun negF absF = repF | negF repF = absFfun get_fun flag qenv lthy ty =let fun get_fun_aux s fs = (case (maps_lookup (ProofContext.theory_of lthy) s) of SOME info => list_comb (Const (#mapfun info, dummyT), fs) | NONE => error ("no map association for type " ^ s)) fun get_const flag qty = let val thy = ProofContext.theory_of lthy val qty_name = Long_Name.base_name (fst (dest_Type qty)) in case flag of absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT) | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT) end fun mk_identity ty = Abs ("", ty, Bound 0)in if (AList.defined (op=) qenv ty) then (get_const flag ty) else (case ty of TFree _ => mk_identity ty | Type (_, []) => mk_identity ty | Type ("fun" , [ty1, ty2]) => let val fs_ty1 = get_fun (negF flag) qenv lthy ty1 val fs_ty2 = get_fun flag qenv lthy ty2 in get_fun_aux "fun" [fs_ty1, fs_ty2] end | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) | _ => error ("no type variables allowed"))end(* returns all subterms where two types differ *)fun diff (T, S) Ds = case (T, S) of (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds | (Type (a, Ts), Type (b, Us)) => if a = b then diffs (Ts, Us) Ds else (T, S)::Ds | _ => (T, S)::Dsand diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) | diffs ([], []) Ds = Ds | diffs _ _ = error "Unequal length of type arguments"*}ML {*fun get_fun_OLD flag (rty, qty) lthy ty = let val tys = find_matching_types rty ty; val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; val xchg_ty = exchange_ty lthy rty qty ty in get_fun flag qenv lthy xchg_ty end*}text {* Does the same as 'subst' in a given prop or theorem *}ML {*fun eqsubst_prop ctxt thms t = let val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t) val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of NONE => error "eqsubst_prop" | SOME th => cprem_of th 1 in term_of a' end*}ML {* fun repeat_eqsubst_prop ctxt thms t = repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t) handle _ => t*}ML {*fun eqsubst_thm ctxt thms thm = let val goalstate = Goal.init (Thm.cprop_of thm) val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of NONE => error "eqsubst_thm" | SOME th => cprem_of th 1 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); val cgoal = cterm_of (ProofContext.theory_of ctxt) goal val rt = Goal.prove_internal [] cgoal (fn _ => tac); in @{thm Pure.equal_elim_rule1} OF [rt, thm] end*}ML {* fun repeat_eqsubst_thm ctxt thms thm = repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) handle _ => thm*}(* Needed to have a meta-equality *)lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"by (simp add: id_def)(* TODO: can be also obtained with: *)ML {* symmetric (eq_reflection OF @{thms id_def}) *}ML {*fun build_repabs_term lthy thm consts rty qty = let (* TODO: The rty and qty stored in the quotient_info should be varified, so this will soon not be needed *) val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; fun mk_abs tm = let val ty = fastype_of tm in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end fun mk_repabs tm = let val ty = fastype_of tm in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end fun is_lifted_const (Const (x, _)) = member (op =) consts x | is_lifted_const _ = false; fun build_aux lthy tm = case tm of Abs (a as (_, vty, _)) => let val (vs, t) = Term.dest_abs a; val v = Free(vs, vty); val t' = lambda v (build_aux lthy t) in if (not (needs_lift rty (fastype_of tm))) then t' else mk_repabs ( if not (needs_lift rty vty) then t' else let val v' = mk_repabs v; (* TODO: I believe 'beta' is not needed any more *) val t1 = (* Envir.beta_norm *) (t' $ v') in lambda v t1 end) end | x => case Term.strip_comb tm of (Const(@{const_name Respects}, _), _) => tm | (opp, tms0) => let val tms = map (build_aux lthy) tms0 val ty = fastype_of tm in if (is_lifted_const opp andalso needs_lift rty ty) then mk_repabs (list_comb (opp, tms)) else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then mk_repabs (list_comb (opp, tms)) else if tms = [] then opp else list_comb(opp, tms) end in repeat_eqsubst_prop lthy @{thms id_def_sym} (build_aux lthy (Thm.prop_of thm)) end*}text {* Builds provable goals for regularized theorems *}ML {*fun build_repabs_goal ctxt thm cons rty qty = Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))*}ML {*fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => let val pat = Drule.strip_imp_concl (cprop_of thm) val insts = Thm.match (pat, concl) in rtac (Drule.instantiate insts thm) 1 end handle _ => no_tac)*}ML {*fun CHANGED' tac = (fn i => CHANGED (tac i))*}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)doneML {*fun quotient_tac quot_thm = REPEAT_ALL_NEW (FIRST' [ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT}, (* For functional identity quotients, (op = ---> op =) *) CHANGED' ( (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} ))) ])*}ML {*fun LAMBDA_RES_TAC ctxt i st = (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | _ => fn _ => no_tac) i st*}ML {*fun WEAK_LAMBDA_RES_TAC ctxt i st = (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of (_ $ (_ $ _ $ (Abs(_, _, _)))) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | (_ $ (_ $ (Abs(_, _, _)) $ _)) => (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) | _ => fn _ => no_tac) i st*}ML {*fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => let val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); val insts = Thm.match (pat, concl) in if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 else no_tac end handle _ => no_tac)*}ML {*val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl in ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 end handle _ => no_tac)*}ML {*val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl in ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 end handle _ => no_tac)*}ML {*fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)*}ML {*fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ rtac trans_thm, LAMBDA_RES_TAC ctxt, ball_rsp_tac ctxt, bex_rsp_tac ctxt, FIRST' (map rtac rsp_thms), rtac refl, (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])), (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, rtac reflex_thm, atac, SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), WEAK_LAMBDA_RES_TAC ctxt, CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})) ])*}ML {*fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm consts rty qty; val rg = Logic.mk_equals ((Thm.prop_of thm), rt); fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); in @{thm Pure.equal_elim_rule1} OF [cthm, thm] end*}section {* Cleaning the goal *}ML {*fun simp_ids lthy thm = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm*}ML {*fun simp_ids_trm trm = trm |> MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} |> cprop_of |> Thm.dest_equals |> snd*}text {* expects atomized definition *}ML {*fun add_lower_defs_aux lthy thm = let val e1 = @{thm fun_cong} OF [thm]; val f = eqsubst_thm lthy @{thms fun_map.simps} e1; val g = simp_ids lthy f in (simp_ids lthy thm) :: (add_lower_defs_aux lthy g) end handle _ => [simp_ids lthy thm]*}ML {*fun add_lower_defs lthy def = let val def_pre_sym = symmetric def val def_atom = atomize_thm def_pre_sym val defs_all = add_lower_defs_aux lthy def_atom in map Thm.varifyT defs_all end*}(* TODO: Check if it behaves properly with varifyed rty *)ML {*fun findabs_all rty tm = case tm of Abs(_, T, b) => let val b' = subst_bound ((Free ("x", T)), b); val tys = findabs_all rty b' val ty = fastype_of tm in if needs_lift rty ty then (ty :: tys) else tys end | f $ a => (findabs_all rty f) @ (findabs_all rty a) | _ => [];fun findabs rty tm = distinct (op =) (findabs_all rty tm)*}ML {*fun findaps_all rty tm = case tm of Abs(_, T, b) => findaps_all rty (subst_bound ((Free ("x", T)), b)) | (f $ a) => (findaps_all rty f @ findaps_all rty a) | Free (_, (T as (Type ("fun", (_ :: _))))) => (if needs_lift rty T then [T] else []) | _ => [];fun findaps rty tm = distinct (op =) (findaps_all rty tm)*}(* Currently useful only for LAMBDA_PRS *)ML {*fun make_simp_prs_thm lthy quot_thm thm typ = let val (_, [lty, rty]) = dest_Type typ; val thy = ProofContext.theory_of lthy; val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) val inst = [SOME lcty, NONE, SOME rcty]; val lpi = Drule.instantiate' inst [] thm; val tac = (compose_tac (false, lpi, 2)) THEN_ALL_NEW (quotient_tac quot_thm); val gc = Drule.strip_imp_concl (cprop_of lpi); val t = Goal.prove_internal [] gc (fn _ => tac 1) in MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t end*}ML {*fun findallex_all rty qty tm = case tm of Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => let val (tya, tye) = findallex_all rty qty s in if needs_lift rty T then ((T :: tya), tye) else (tya, tye) end | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => let val (tya, tye) = findallex_all rty qty s in if needs_lift rty T then (tya, (T :: tye)) else (tya, tye) end | Abs(_, T, b) => findallex_all rty qty (subst_bound ((Free ("x", T)), b)) | f $ a => let val (a1, e1) = findallex_all rty qty f; val (a2, e2) = findallex_all rty qty a; in (a1 @ a2, e1 @ e2) end | _ => ([], []);*}ML {*fun findallex lthy rty qty tm = let val (a, e) = findallex_all rty qty tm; val (ad, ed) = (map domain_type a, map domain_type e); val (au, eu) = (distinct (op =) ad, distinct (op =) ed); val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) in (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) end*}ML {*fun make_allex_prs_thm lthy quot_thm thm typ = let val (_, [lty, rty]) = dest_Type typ; val thy = ProofContext.theory_of lthy; val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) val inst = [NONE, SOME lcty]; val lpi = Drule.instantiate' inst [] thm; val tac = (compose_tac (false, lpi, 1)) THEN_ALL_NEW (quotient_tac quot_thm); val gc = Drule.strip_imp_concl (cprop_of lpi); val t = Goal.prove_internal [] gc (fn _ => tac 1) val t_noid = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t; val t_sym = @{thm "HOL.sym"} OF [t_noid]; val t_eq = @{thm "eq_reflection"} OF [t_sym] in t_eq end*}ML {*fun applic_prs lthy rty qty absrep ty = let val rty = Logic.varifyT rty; val qty = Logic.varifyT qty; fun absty ty = exchange_ty lthy rty qty ty fun mk_rep tm = let val ty = exchange_ty lthy qty rty (fastype_of tm) in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end; fun mk_abs tm = let val ty = fastype_of tm in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end val (l, ltl) = Term.strip_type ty; val nl = map absty l; val vs = map (fn _ => "x") l; val ((fname :: vfs), lthy') = Variable.variant_fixes ("f" :: vs) lthy; val args = map Free (vfs ~~ nl); val lhs = list_comb((Free (fname, nl ---> ltl)), args); val rargs = map mk_rep args; val f = Free (fname, nl ---> ltl); val rhs = mk_abs (list_comb((mk_rep f), rargs)); val eq = Logic.mk_equals (rhs, lhs); val ceq = cterm_of (ProofContext.theory_of lthy') eq; val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps}); val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; in singleton (ProofContext.export lthy' lthy) t_id end*}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_pre = @{thm EQUIV_REFL} OF [rel_eqv] val rel_refl = @{thm spec} OF [MetaSimplifier.rewrite_rule [@{thm REFL_def}] rel_refl_pre] 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*}ML {*fun lift_thm lthy qty qty_name rsp_thms defs rthm = let val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; val consts = lookup_quot_consts defs; val t_a = atomize_thm rthm; val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) val (alls, exs) = findallex lthy rty qty (prop_of t_a); val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) val abs = findabs rty (prop_of t_a); val aps = findaps rty (prop_of t_a); val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) val defs_sym = flat (map (add_lower_defs lthy) defs); val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; val t_id = simp_ids lthy t_l; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) val t_rv = ObjectLogic.rulify t_r val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))in Thm.varifyT t_rvend*}ML {*fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = let val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; val (_, lthy2) = note (name, lifted_thm) lthy; in lthy2 end*}(******************************************)(******************************************)(* version with explicit qtrm *)(******************************************)(******************************************)ML {*fun atomize_goal thy gl = let val vars = map Free (Term.add_frees gl []); val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all; fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm; val glv = fold lambda_all vars gl val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv)) val glf = Type.legacy_freeze gla in if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf end*}ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}ML {*(* builds the relation for 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 *) 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 {*fun trm_lift_error lthy rtrm qtrm =let val rtrm_str = quote (Syntax.string_of_term lthy rtrm) val qtrm_str = quote (Syntax.string_of_term lthy qtrm) val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]in raise error (space_implode " " msg)end *}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) *}(*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 {*(* 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')) => if x = x' then rtrm (* FIXME: check whether types corresponds *) else trm_lift_error lthy rtrm qtrm | (Bound i, Bound i') => if i = i' then rtrm else trm_lift_error lthy rtrm qtrm | (Const (s, ty), Const (s', ty')) => if s = s' andalso ty = ty' then rtrm else rtrm (* FIXME: check correspondence according to definitions *) | _ => trm_lift_error lthy rtrm qtrm*}ML {*fun mk_REGULARIZE_goal lthy rtrm qtrm = Logic.mk_implies (rtrm, Syntax.check_term lthy (REGULARIZE_trm lthy rtrm qtrm))*}(*To prove that the old theorem implies the new one, we firstatomize it and then try: - 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*)lemma my_equiv_res_forall2: fixes P::"'a \<Rightarrow> bool" fixes Q::"'b \<Rightarrow> bool" assumes a: "(All Q) \<longrightarrow> (All P)" shows "(All Q) \<longrightarrow> Ball (Respects E) P"using a by autolemma my_equiv_res_exists: fixes P::"'a \<Rightarrow> bool" fixes Q::"'b \<Rightarrow> bool" assumes a: "EQUIV E" and b: "(Ex Q) \<longrightarrow> (Ex P)" shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"apply(subst equiv_res_exists)apply(rule a)apply(rule b)doneML {*(* FIXME: get_rid of rel_refl rel_eqv *)fun REGULARIZE_tac lthy rel_refl rel_eqv = (REPEAT1 o FIRST1) [rtac rel_refl, atac, rtac @{thm universal_twice}, rtac @{thm impI} THEN' atac, rtac @{thm implication_twice}, rtac @{thm my_equiv_res_forall2}, rtac (rel_eqv RS @{thm my_equiv_res_exists}), (* For a = b \<longrightarrow> a \<approx> b *) rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, rtac @{thm RIGHT_RES_FORALL_REGULAR}]*}(* version of REGULARIZE_tac including debugging information *)ML {*fun my_print_tac ctxt s thm =let val prems_str = prems_of thm |> map (Syntax.string_of_term ctxt) |> cat_lines val _ = tracing (s ^ "\n" ^ prems_str)in Seq.single thmendfun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]*}ML {*fun REGULARIZE_tac' lthy rel_refl rel_eqv = (REPEAT1 o FIRST1) [(K (print_tac "start")) THEN' (K no_tac), DT lthy "1" (rtac rel_refl), DT lthy "2" atac, DT lthy "3" (rtac @{thm universal_twice}), DT lthy "4" (rtac @{thm impI} THEN' atac), DT lthy "5" (rtac @{thm implication_twice}), DT lthy "6" (rtac @{thm my_equiv_res_forall2}), DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), (* For a = b \<longrightarrow> a \<approx> b *) DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]*}ML {*fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy = let val goal = mk_REGULARIZE_goal lthy rtrm qtrm in Goal.prove lthy [] [] goal (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv) end*}(* rep-abs injection *)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 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 lthy (t, t')) | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t')) | (Const (@{const_name "Babs"}, T) $ r $ t, t') => Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS 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 = lambda yvar (inj_REPABS lthy (s, s')) in if rty = qty then result else mk_repabs lthy (rty, qty) result end | _ => (* FIXME / TODO: this is a case that needs to be looked at *) (* - variables get a rep-abs insde and outside an application *) (* - constants only get a rep-abs on the outside of the application *) (* - applications get a rep-abs insde and outside an application *) let val (rhead, rargs) = strip_comb rtrm val (qhead, qargs) = strip_comb qtrm val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs) in if rty = qty then case (rhead, qhead) of (Free (_, T), Free (_, T')) => if T = T' then list_comb (rhead, rargs') else list_comb (mk_repabs lthy (T, T') rhead, rargs') | _ => list_comb (rhead, rargs') else case (rhead, qhead, length rargs') of (Const _, Const _, 0) => mk_repabs lthy (rty, qty) rhead | (Free (_, T), Free (_, T'), 0) => mk_repabs lthy (T, T') rhead | (Const _, Const _, _) => mk_repabs lthy (rty, qty) (list_comb (rhead, rargs')) | (Free (x, T), Free (x', T'), _) => mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs')) | (Abs _, Abs _, _ ) => mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) | _ => trm_lift_error lthy rtrm qtrm endend*}ML {*fun mk_inj_REPABS_goal lthy (rtrm, qtrm) = Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))*}(* Final wrappers *)ML {*fun regularize_tac ctxt rel_eqv rel_refl = (ObjectLogic.full_atomize_tac) THEN' REPEAT_ALL_NEW (FIRST' [ rtac rel_refl, atac, rtac @{thm universal_twice}, (rtac @{thm impI} THEN' atac), rtac @{thm implication_twice}, EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])], (* For a = b \<longrightarrow> a \<approx> b *) (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]);*}ML {*fun regularize_goal lthy thm rel_eqv rel_refl qtrm = let val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; fun tac lthy = regularize_tac lthy rel_eqv rel_refl; val cthm = Goal.prove lthy [] [] reg_trm (fn {context, ...} => tac context 1); in cthm OF [thm] end*}ML {*fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = let val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); in @{thm Pure.equal_elim_rule1} OF [cthm, thm] end*}ML {*fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =let val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; val t_a = atomize_thm rthm; val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; val (alls, exs) = findallex lthy rty qty (prop_of t_a); val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t val abs = findabs rty (prop_of t_a); val aps = findaps rty (prop_of t_a); val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; val defs_sym = flat (map (add_lower_defs lthy) defs); val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; val t_id = simp_ids lthy t_l; val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; val t_rv = ObjectLogic.rulify t_rin Thm.varifyT t_rvend*}ML {*fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = let val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; val (_, lthy2) = note (name, lifted_thm) lthy; in lthy2 end*}ML {*fun spec_frees_tac [] = [] | spec_frees_tac (x::xs) = let val spec' = Drule.instantiate' [SOME (ctyp_of_term x)] [NONE, SOME x] @{thm spec} in (rtac spec')::(spec_frees_tac xs) end*} ML {*val prepare_tac = CSUBGOAL (fn (concl, i) => let val vrs = Thm.add_cterm_frees concl [] in EVERY' (ObjectLogic.full_atomize_tac::spec_frees_tac vrs) i end)*}lemma 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 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') val inj_goal = Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))in Drule.instantiate' [] [SOME (cterm_of thy rtrm'), SOME (cterm_of thy reg_goal), SOME (cterm_of thy inj_goal)] @{thm procedure}end*}ML {*fun procedure_tac rthm ctxt = prepare_tac 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) ctxt*}ML {*(* FIXME: allex_prs and lambda_prs can be one function *)fun allex_prs_tac lthy quot = (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) THEN' (quotient_tac quot);*}ML {*fun lambda_prs_tac lthy quot = (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} THEN' (RANGE [quotient_tac quot, quotient_tac quot]));*}ML {* fun TRY' tac = fn i => TRY (tac i)*}ML {*fun clean_tac lthy quot defs reps_same = let val lower = flat (map (add_lower_defs lthy) defs) in TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' simp_tac (HOL_ss addsimps [reps_same]) end*}ML {*fun lift_tac lthy thm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs = (procedure_tac thm lthy) THEN' (regularize_tac lthy rel_eqv rel_refl) THEN' (REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms)) THEN' (clean_tac lthy quot defs reps_same)*}end