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 x \<equiv> Abs (R x)"definition "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"proof assume "R a b" then have "R b a" using R_sym by blast then have "R b c" using ac R_trans by blast then have "R c b" using R_sym by blast then show "R c d" using bd R_trans by blastnext assume "R c d" then have "R a d" using ac R_trans by blast then have "R d a" using R_sym by blast then have "R b a" using bd R_trans by blast then show "R a b" using R_sym by blastqedlemma 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 *}ML {* Toplevel.theory *}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" *}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 {**}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 rty qty lthy ty =let val qty_name = Long_Name.base_name (fst (dest_Type qty)) 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 val thy = ProofContext.theory_of lthy fun get_const absF = (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) | get_const repF = (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) fun mk_identity ty = Abs ("", ty, Bound 0)in if ty = qty then (get_const flag) 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) rty qty lthy ty1, get_fun flag rty qty lthy ty2] | Type (s, tys) => get_fun_aux s (map (get_fun flag rty qty lthy) tys) | _ => raise ERROR ("no type variables") )end*}text {* produces the definition for a lifted constant *}ML {*fun get_const_def nconst oconst rty qty lthy =let val ty = fastype_of nconst val (arg_tys, res_ty) = strip_type ty val fresh_args = arg_tys |> map (pair "x") |> Variable.variant_frees lthy [nconst, oconst] |> map Free val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys val abs_fn = (fst o get_fun absF rty qty 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 $ oconstend*}ML {*fun exchange_ty rty qty ty = if ty = rty then qty else (case ty of Type (s, tys) => Type (s, map (exchange_ty rty qty) tys) | _ => ty )*}ML {*fun make_const_def nconst_bname oconst mx rty qty lthy =let val oconst_ty = fastype_of oconst val nconst_ty = exchange_ty rty qty oconst_ty val nconst = Const (Binding.name_of nconst_bname, nconst_ty) val def_trm = get_const_def nconst oconst rty qty lthyin define (nconst_bname, mx, def_trm) lthyend*}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' = forall_intr_vars thm val thm'' = ObjectLogic.atomize (cprop_of thm')in Thm.freezeT (Simplifier.rewrite_rule [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))*}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 build_repabs_term lthy thm constructors rty qty = let fun mk_rep tm = let val ty = exchange_ty rty qty (fastype_of tm) in fst (get_fun repF rty qty lthy ty) $ tm end fun mk_abs tm = let val ty = exchange_ty rty qty (fastype_of tm) in fst (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))*}end