theory QuotMainimports QuotScript QuotList Proveuses ("quotient_info.ML") ("quotient.ML") ("quotient_def.ML")beginlocale 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"text {* FIXME: auxiliary function *}ML {*val no_vars = Thm.rule_attribute (fn context => fn th => let val ctxt = Variable.set_body false (Context.proof_of context); val ((_, [th']), _) = Variable.import true [th] ctxt; in th' end);*}section {* ATOMIZE *}text {* Unabs_def converts a definition given as c \<equiv> %x. %y. f x y to a theorem of the form c x y \<equiv> f x y This function is needed to rewrite the right-hand side to the left-hand side.*}ML {*fun unabs_def ctxt def =let val (lhs, rhs) = Thm.dest_equals (cprop_of def) val xs = strip_abs_vars (term_of rhs) val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt val thy = ProofContext.theory_of ctxt' val cxs = map (cterm_of thy o Free) xs val new_lhs = Drule.list_comb (lhs, cxs) fun get_conv [] = Conv.rewr_conv def | get_conv (x::xs) = Conv.fun_conv (get_conv xs)in get_conv xs new_lhs |> singleton (ProofContext.export ctxt' ctxt)end*}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 abstactions: \<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 matches (ty1, ty2) = Type.raw_instance (ty1, Logic.varifyT ty2);fun tyRel ty rty rel lthy = if matches (rty, ty) 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)*}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 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*}ML {*fun my_reg_inst lthy rel rty trm = case rel of Const (n, _) => Syntax.check_term lthy (my_reg lthy (Const (n, dummyT)) rty trm)*}(*ML {* (*val r = term_of @{cpat "R::?'a list \<Rightarrow> ?'a list \<Rightarrow>bool"};*) val r = Free ("R", dummyT); val t = (my_reg @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); val t2 = Syntax.check_term @{context} t; Toplevel.program (fn () => 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: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"by autolemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"by auto(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"by auto*)ML {*fun regularize thm rty rel rel_eqv rel_refl lthy = let val g = 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}, (*rtac @{thm equality_twice},*) EqSubst.eqsubst_tac ctxt [0] [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])], (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl), (rtac @{thm RIGHT_RES_FORALL_REGULAR}) ]); val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); in cthm OF [thm] end*}section {* RepAbs injection *}(* Needed to have a meta-equality *)lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"by (simp add: id_def)ML {*fun old_exchange_ty rty qty ty = if ty = rty then qty else (case ty of Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) | _ => ty )*}ML {*fun old_get_fun flag rty qty lthy ty = get_fun flag [(qty, rty)] lthy ty fun old_make_const_def nconst_bname otrm mx rty qty lthy = make_def nconst_bname otrm qty mx Attrib.empty_binding [(qty, rty)] lthy*}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 cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) val rt = Toplevel.program (fn () => 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*}ML {*fun build_repabs_term lthy thm constructors rty qty = let fun mk_rep tm = let val ty = old_exchange_ty rty qty (fastype_of tm) in fst (old_get_fun repF rty qty lthy ty) $ tm end fun mk_abs tm = let val ty = old_exchange_ty rty qty (fastype_of tm) in fst (old_get_fun absF rty qty lthy ty) $ tm end fun is_constructor (Const (x, _)) = member (op =) constructors x | is_constructor _ = 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_rep (mk_abs ( if not (needs_lift rty vty) then t' else let val v' = mk_rep (mk_abs v); val t1 = Envir.beta_norm (t' $ v') in lambda v t1 end )) end | x => let val (opp, tms0) = Term.strip_comb tm val tms = map (build_aux lthy) tms0 val ty = fastype_of tm in if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false) then (list_comb (opp, (hd tms0) :: (tl tms))) else if (is_constructor opp andalso needs_lift rty ty) then mk_rep (mk_abs (list_comb (opp,tms))) else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then mk_rep(mk_abs(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 {* Assumes that it is given a regularized theorem *}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) 1endhandle _ => no_tac)*}ML {*fun quotient_tac quot_thm = REPEAT_ALL_NEW (FIRST' [ rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT} ])*}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_tacendhandle _ => no_tac)*}ML {*val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl in ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 end handle _ => no_tac )*}ML {*val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => let val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl in ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 end handle _ => no_tac )*}ML {*fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [(* rtac @{thm FUN_QUOTIENT}, rtac quot_thm, rtac @{thm IDENTITY_QUOTIENT},*) rtac trans_thm, LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, res_exists_rsp_tac ctxt, FIRST' (map rtac rsp_thms), (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), rtac refl,(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), Cong_Tac.cong_tac @{thm cong}, rtac @{thm ext}, rtac reflex_thm, atac, ( (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) THEN_ALL_NEW (fn _ => no_tac) ), WEAK_LAMBDA_RES_TAC ctxt ])*}ML {*fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = let val rt = build_repabs_term lthy thm constructors 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 *}lemma prod_fun_id: "prod_fun id id = id" apply (simp add: prod_fun_def)donelemma map_id: "map id x = x" apply (induct x) apply (simp_all add: map.simps)donetext {* expects atomized definition *}ML {* fun add_lower_defs_aux ctxt thm = let val e1 = @{thm fun_cong} OF [thm]; val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I id_apply prod_fun_id map_id} g in thm :: (add_lower_defs_aux ctxt h) end handle _ => [thm]*}ML {*fun add_lower_defs ctxt defs = let val defs_pre_sym = map symmetric defs val defs_atom = map atomize_thm defs_pre_sym val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom) in map Thm.varifyT defs_all end*}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)*}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 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) in (map (old_exchange_ty rty qty) au, map (old_exchange_ty 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 fun absty ty = old_exchange_ty rty qty ty fun mk_rep tm = let val ty = old_exchange_ty rty qty (fastype_of tm) in fst (old_get_fun repF rty qty lthy ty) $ tm end; fun mk_abs tm = let val ty = old_exchange_ty rty qty (fastype_of tm) in fst (old_get_fun 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 = (Simplifier.context lthy' 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 SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) 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 t = 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 consts = lookup_quot_consts defs; val t_a = atomize_thm t; val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val (alls, exs) = findallex 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 = add_lower_defs lthy defs; val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;in ObjectLogic.rulify t_rend*}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;*}end