theory QuotMainimports QuotScript QuotList Proveuses ("quotient.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 *}use "quotient.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" *}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 {* lifting of constants *}ML {*(* whether ty1 is an instance of ty2 *)fun matches (ty1, ty2) = Type.raw_instance (ty1, Logic.varifyT ty2)fun lookup_snd _ [] _ = NONE | lookup_snd eq ((value, key)::xs) key' = if eq (key', key) then SOME value else lookup_snd eq xs key';fun lookup_qenv qenv qty = (case (AList.lookup matches qenv qty) of SOME rty => SOME (qty, rty) | NONE => NONE)*}ML {*(* calculates the aggregate abs and rep functions for a given type; repF is for constants' arguments; absF is for constants; function types need to be treated specially, since repF and absF change*)datatype flag = absF | repFfun negF absF = repF | negF repF = absFfun get_fun flag qenv lthy ty =let fun get_fun_aux s fs_tys = let val (fs, tys) = split_list fs_tys val (otys, ntys) = split_list tys val oty = Type (s, otys) val nty = Type (s, ntys) val ftys = map (op -->) tys in (case (maps_lookup (ProofContext.theory_of lthy) s) of SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty)) | NONE => raise ERROR ("no map association for type " ^ s)) end fun get_fun_fun fs_tys = let val (fs, tys) = split_list fs_tys val ([oty1, oty2], [nty1, nty2]) = split_list tys val oty = nty1 --> oty2 val nty = oty1 --> nty2 val ftys = map (op -->) tys in (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) end fun get_const flag (qty, rty) = 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), rty --> qty), (rty, qty)) | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) end fun mk_identity ty = Abs ("", ty, Bound 0)in if (AList.defined matches qenv ty) then (get_const flag (the (lookup_qenv qenv ty))) else (case ty of TFree _ => (mk_identity ty, (ty, ty)) | Type (_, []) => (mk_identity ty, (ty, ty)) | Type ("fun" , [ty1, ty2]) => get_fun_fun [get_fun (negF flag) qenv lthy ty1, get_fun flag qenv lthy ty2] | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys) | _ => raise ERROR ("no type variables") )end*}text {* produces the definition for a lifted constant *}ML {*fun get_const_def nconst otrm qenv lthy =let val ty = fastype_of nconst val (arg_tys, res_ty) = strip_type ty val rep_fns = map (fst o get_fun repF qenv lthy) arg_tys val abs_fn = (fst o get_fun absF qenv lthy) res_ty fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2 val fns = Library.foldr mk_fun_map (rep_fns, abs_fn) |> Syntax.check_term lthyin fns $ otrmend*}ML {* lookup_snd *}ML {*fun exchange_ty qenv ty = case (lookup_snd matches qenv ty) of SOME qty => qty | NONE => (case ty of Type (s, tys) => Type (s, map (exchange_ty qenv) tys) | _ => ty )*}ML {*fun make_const_def nconst_bname otrm mx qenv lthy =let val otrm_ty = fastype_of otrm val nconst_ty = exchange_ty qenv otrm_ty val nconst = Const (Binding.name_of nconst_bname, nconst_ty) val def_trm = get_const_def nconst otrm qenv lthyin define (nconst_bname, mx, def_trm) lthyend*}ML {*fun build_qenv lthy qtys = let val qenv = map (fn {qtyp, rtyp, ...} => (qtyp, rtyp)) (quotdata_lookup lthy) fun find_assoc qty = case (AList.lookup matches qenv qty) of SOME rty => (qty, rty) | NONE => error (implode ["Quotient type ", quote (Syntax.string_of_typ lthy qty), " does not exists"])in map find_assoc qtysend*}ML {*(* taken from isar_syn.ML *)val constdecl = OuterParse.binding -- (OuterParse.where_ >> K (NONE, NoSyn) || OuterParse.$$$ "::" |-- OuterParse.!!! ((OuterParse.typ >> SOME) -- OuterParse.opt_mixfix' --| OuterParse.where_) || Scan.ahead (OuterParse.$$$ "(") |-- OuterParse.!!! (OuterParse.mixfix' --| OuterParse.where_ >> pair NONE))*}ML {*val qd_parser = (Args.parens (OuterParse.$$$ "for" |-- (Scan.repeat OuterParse.typ))) -- (constdecl -- (SpecParse.opt_thm_name ":" -- OuterParse.prop))*}ML {* fun pair lthy (ty1, ty2) = "(" ^ (Syntax.string_of_typ lthy ty1) ^ "," ^ (Syntax.string_of_typ lthy ty2) ^ ")"*}ML {*fun parse_qd_spec (qtystrs, ((bind, (typstr__, mx)), (attr__, propstr))) lthy = let val qtys = map (Syntax.check_typ lthy o Syntax.parse_typ lthy) qtystrs val qenv = build_qenv lthy qtys val prop = Syntax.parse_prop lthy propstr |> Syntax.check_prop lthy val (lhs, rhs) = Logic.dest_equals propin make_const_def bind rhs mx qenv lthy |> sndend*}ML {*val _ = OuterSyntax.local_theory "quotient_def" "lifted definition of constants" OuterKeyword.thy_decl (qd_parser >> parse_qd_spec)*}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 *}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 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)*}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 {*(* trm \<Rightarrow> new_trm *)fun regularise trm rty rel lthy = case trm of Abs (x, T, t) => if (needs_lift rty T) then let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; val lam_term = Term.lambda_name (x, v) rec_term; val sub_res_term = tyRel T rty rel lthy; val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); val res_term = respects $ sub_res_term; val ty = fastype_of trm; val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty); val rabs_term = (rabs $ res_term) $ lam_term; in rabs_term end else let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; in Term.lambda_name (x, v) rec_term end | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) => if (needs_lift rty T) then let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; val lam_term = Term.lambda_name (x, v) rec_term; val sub_res_term = tyRel T rty rel lthy; val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); val res_term = respects $ sub_res_term; val ty = fastype_of lam_term; val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool}); val rall_term = (rall $ res_term) $ lam_term; in rall_term end else let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; val lam_term = Term.lambda_name (x, v) rec_term in Const(@{const_name "All"}, at) $ lam_term end | ((Const (@{const_name "All"}, at)) $ P) => let val (_, [al, _]) = dest_Type (fastype_of P); val ([x], lthy2) = Variable.variant_fixes [""] lthy; val v = (Free (x, al)); val abs = Term.lambda_name (x, v) (P $ v); in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) => if (needs_lift rty T) then let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; val lam_term = Term.lambda_name (x, v) rec_term; val sub_res_term = tyRel T rty rel lthy; val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool}); val res_term = respects $ sub_res_term; val ty = fastype_of lam_term; val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool}); val rall_term = (rall $ res_term) $ lam_term; in rall_term end else let val ([x'], lthy2) = Variable.variant_fixes [x] lthy; val v = Free (x', T); val t' = subst_bound (v, t); val rec_term = regularise t' rty rel lthy2; val lam_term = Term.lambda_name (x, v) rec_term in Const(@{const_name "Ex"}, at) $ lam_term end | ((Const (@{const_name "Ex"}, at)) $ P) => let val (_, [al, _]) = dest_Type (fastype_of P); val ([x], lthy2) = Variable.variant_fixes [""] lthy; val v = (Free (x, al)); val abs = Term.lambda_name (x, v) (P $ v); in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy) | _ => trm*}(* my version of regularise *)(****************************)(* some helper functions *)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: assumes always the typ is qty! *)(* FIXME: if there are more than one quotient, then you have to look up the relation *)ML {*fun my_reg rel trm = case trm of Abs (x, T, t) => let val ty1 = fastype_of trm in (mk_babs ty1 T) $ (mk_resp T $ rel) $ (apply_subt (my_reg rel) trm) end | Const (@{const_name "All"}, ty) $ t => let val ty1 = domain_type ty val ty2 = domain_type ty1 in (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) end | Const (@{const_name "Ex"}, ty) $ t => let val ty1 = domain_type ty val ty2 = domain_type ty1 in (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t) end | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2) | _ => trm*}(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this) trm == new_trm*)text {* Assumes that the given theorem is atomized *}ML {* fun build_regularize_goal thm rty rel lthy = Logic.mk_implies ((prop_of thm), (regularise (prop_of thm) rty rel lthy))*}ML {*fun regularize thm rty rel rel_eqv lthy = let val g = build_regularize_goal thm rty rel lthy; fun tac ctxt = (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps [(@{thm equiv_res_forall} OF [rel_eqv]), (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); 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_const_def nconst_bname otrm mx [(qty, rty)] lthy*}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 MetaSimplifier.rewrite_term @{theory} @{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 res_forall_rsp_tac ctxt = (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}))*}ML {*fun res_exists_rsp_tac ctxt = (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}))*}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 {*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, ( (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) THEN_ALL_NEW (fn _ => no_tac) ), (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 *}text {* Does the same as 'subst' in a given theorem *}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*}text {* 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} g; val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h in thm :: (add_lower_defs_aux ctxt i) 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*}text {* the proper way to do it *}ML {* fun findabs rty tm = case tm of Abs(_, T, b) => let val b' = subst_bound ((Free ("x", T)), b); val tys = findabs rty b' val ty = fastype_of tm in if needs_lift rty ty then (ty :: tys) else tys end | f $ a => (findabs rty f) @ (findabs rty a) | _ => []*}ML {*fun make_simp_lam_prs_thm lthy quot_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 LAMBDA_PRS}; val tac = (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW (quotient_tac quot_thm); val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); val ts = @{thm HOL.sym} OF [t] in MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts end*}ML {* fun simp_allex_prs lthy quot thm = let val rwf = @{thm FORALL_PRS} OF [quot]; val rwfs = @{thm "HOL.sym"} OF [rwf]; val rwe = @{thm EXISTS_PRS} OF [quot]; val rwes = @{thm "HOL.sym"} OF [rwe] in (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) end handle _ => thm*}ML {*fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let val t_a = atomize_thm t; val t_r = regularize t_a rty rel rel_eqv lthy; val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; val abs = findabs rty (prop_of t_a); val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; val t_l = repeat_eqsubst_thm lthy simp_lam_prs_thms t_t; val t_a = simp_allex_prs lthy quot t_l; val t_defs_sym = add_lower_defs lthy t_defs; val t_d = repeat_eqsubst_thm lthy t_defs_sym t_a; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;in ObjectLogic.rulify t_rend*}end