# HG changeset patch # User kuncar # Date 1353936051 -3600 # Node ID 01d545993e8ccfdbe5a8b4627c7d2aa3de3b4868 # Parent 536ab2e82eade785ad86b13b01bae6c8ebeadf2f generate a parameterized correspondence relation diff -r 536ab2e82ead -r 01d545993e8c src/HOL/Quotient_Examples/Lift_FSet.thy --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Nov 26 14:20:36 2012 +0100 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Mon Nov 26 14:20:51 2012 +0100 @@ -98,27 +98,26 @@ @{text "list"} and @{text "fset"} types with the same element type. To relate nested types like @{text "'a list list"} and @{text "'a fset fset"}, we define a parameterized version of the - correspondence relation, @{text "cr_fset'"}. *} + correspondence relation, @{text "pcr_fset"}. *} + +thm pcr_fset_def -definition cr_fset' :: "('a \ 'b \ bool) \ 'a list \ 'b fset \ bool" - where "cr_fset' R = list_all2 R OO cr_fset" - -lemma right_unique_cr_fset' [transfer_rule]: - "right_unique A \ right_unique (cr_fset' A)" - unfolding cr_fset'_def +lemma right_unique_pcr_fset [transfer_rule]: + "right_unique A \ right_unique (pcr_fset A)" + unfolding pcr_fset_def by (intro right_unique_OO right_unique_list_all2 fset.right_unique) -lemma right_total_cr_fset' [transfer_rule]: - "right_total A \ right_total (cr_fset' A)" - unfolding cr_fset'_def +lemma right_total_pcr_fset [transfer_rule]: + "right_total A \ right_total (pcr_fset A)" + unfolding pcr_fset_def by (intro right_total_OO right_total_list_all2 fset.right_total) -lemma bi_total_cr_fset' [transfer_rule]: - "bi_total A \ bi_total (cr_fset' A)" - unfolding cr_fset'_def +lemma bi_total_pcr_fset [transfer_rule]: + "bi_total A \ bi_total (pcr_fset A)" + unfolding pcr_fset_def by (intro bi_total_OO bi_total_list_all2 fset.bi_total) -text {* Transfer rules for @{text "cr_fset'"} can be derived from the +text {* Transfer rules for @{text "pcr_fset"} can be derived from the existing transfer rules for @{text "cr_fset"} together with the transfer rules for the polymorphic raw constants. *} @@ -126,16 +125,16 @@ could potentially be automated. *} lemma fnil_transfer [transfer_rule]: - "(cr_fset' A) [] fnil" - unfolding cr_fset'_def + "(pcr_fset A) [] fnil" + unfolding pcr_fset_def apply (rule relcomppI) apply (rule Nil_transfer) apply (rule fnil.transfer) done lemma fcons_transfer [transfer_rule]: - "(A ===> cr_fset' A ===> cr_fset' A) Cons fcons" - unfolding cr_fset'_def + "(A ===> pcr_fset A ===> pcr_fset A) Cons fcons" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (rule relcomppI) @@ -144,8 +143,8 @@ done lemma fappend_transfer [transfer_rule]: - "(cr_fset' A ===> cr_fset' A ===> cr_fset' A) append fappend" - unfolding cr_fset'_def + "(pcr_fset A ===> pcr_fset A ===> pcr_fset A) append fappend" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (rule relcomppI) @@ -154,8 +153,8 @@ done lemma fmap_transfer [transfer_rule]: - "((A ===> B) ===> cr_fset' A ===> cr_fset' B) map fmap" - unfolding cr_fset'_def + "((A ===> B) ===> pcr_fset A ===> pcr_fset B) map fmap" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (rule relcomppI) @@ -164,8 +163,8 @@ done lemma ffilter_transfer [transfer_rule]: - "((A ===> op =) ===> cr_fset' A ===> cr_fset' A) filter ffilter" - unfolding cr_fset'_def + "((A ===> op =) ===> pcr_fset A ===> pcr_fset A) filter ffilter" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (rule relcomppI) @@ -174,8 +173,8 @@ done lemma fset_transfer [transfer_rule]: - "(cr_fset' A ===> set_rel A) set fset" - unfolding cr_fset'_def + "(pcr_fset A ===> set_rel A) set fset" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (drule fset.transfer [THEN fun_relD, unfolded relator_eq]) @@ -184,8 +183,8 @@ done lemma fconcat_transfer [transfer_rule]: - "(cr_fset' (cr_fset' A) ===> cr_fset' A) concat fconcat" - unfolding cr_fset'_def + "(pcr_fset (pcr_fset A) ===> pcr_fset A) concat fconcat" + unfolding pcr_fset_def unfolding list_all2_OO apply (intro fun_relI) apply (elim relcomppE) @@ -202,8 +201,8 @@ lemma fset_eq_transfer [transfer_rule]: assumes "bi_unique A" - shows "(cr_fset' A ===> cr_fset' A ===> op =) list_eq (op =)" - unfolding cr_fset'_def + shows "(pcr_fset A ===> pcr_fset A ===> op =) list_eq (op =)" + unfolding pcr_fset_def apply (intro fun_relI) apply (elim relcomppE) apply (rule trans) diff -r 536ab2e82ead -r 01d545993e8c src/HOL/Tools/Lifting/lifting_info.ML --- a/src/HOL/Tools/Lifting/lifting_info.ML Mon Nov 26 14:20:36 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_info.ML Mon Nov 26 14:20:51 2012 +0100 @@ -11,7 +11,7 @@ val lookup_quotmaps_global: theory -> string -> quotmaps option val print_quotmaps: Proof.context -> unit - type quotients = {quot_thm: thm} + type quotients = {quot_thm: thm, pcrel_def: thm option} val transform_quotients: morphism -> quotients -> quotients val lookup_quotients: Proof.context -> string -> quotients option val lookup_quotients_global: theory -> string -> quotients option @@ -118,7 +118,7 @@ end (* info about quotient types *) -type quotients = {quot_thm: thm} +type quotients = {quot_thm: thm, pcrel_def: thm option} structure Quotients = Generic_Data ( @@ -128,8 +128,8 @@ fun merge data = Symtab.merge (K true) data ) -fun transform_quotients phi {quot_thm} = - {quot_thm = Morphism.thm phi quot_thm} +fun transform_quotients phi {quot_thm, pcrel_def} = + {quot_thm = Morphism.thm phi quot_thm, pcrel_def = Option.map (Morphism.thm phi) pcrel_def} val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory @@ -144,8 +144,8 @@ val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name in case maybe_stored_quot_thm of - SOME {quot_thm = stored_quot_thm} => - if Thm.eq_thm_prop (stored_quot_thm, quot_thm) then + SOME data => + if Thm.eq_thm_prop (#quot_thm data, quot_thm) then Quotients.map (Symtab.delete qty_full_name) ctxt else ctxt @@ -157,12 +157,14 @@ fun print_quotients ctxt = let - fun prt_quot (qty_name, {quot_thm}) = + fun prt_quot (qty_name, {quot_thm, pcrel_def}) = Pretty.block (separate (Pretty.brk 2) [Pretty.str "type:", Pretty.str qty_name, Pretty.str "quot. thm:", - Syntax.pretty_term ctxt (prop_of quot_thm)]) + Syntax.pretty_term ctxt (prop_of quot_thm), + Pretty.str "pcrel_def thm:", + option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of) pcrel_def]) in map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt))) |> Pretty.big_list "quotients:" diff -r 536ab2e82ead -r 01d545993e8c src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 14:20:36 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Mon Nov 26 14:20:51 2012 +0100 @@ -22,20 +22,62 @@ exception SETUP_LIFTING_INFR of string -fun define_cr_rel rep_fun lthy = +fun define_crel rep_fun lthy = let val (qty, rty) = (dest_funT o fastype_of) rep_fun val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)); val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty - val cr_rel_name = Binding.prefix_name "cr_" qty_name + val crel_name = Binding.prefix_name "cr_" qty_name val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy val ((_, (_ , def_thm)), lthy'') = - Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy' + Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy' in (def_thm, lthy'') end +fun print_define_pcrel_warning msg = + let + val warning_msg = cat_lines + ["Generation of a parametrized correspondence relation failed.", + (Pretty.string_of (Pretty.block + [Pretty.str "Reason:", Pretty.brk 2, msg]))] + in + warning warning_msg + end + +fun define_pcrel crel lthy = + let + val pcrel = Morphism.term (Local_Theory.target_morphism lthy) crel + val [crel_poly] = Variable.polymorphic lthy [pcrel] + val rty_raw = (domain_type o fastype_of) crel_poly + val (quot_thm, assms) = Lifting_Term.prove_param_quot_thm lthy rty_raw + val args = map (fn (_, q_thm) => quot_thm_crel q_thm) assms + val parametrized_relator = quot_thm_crel quot_thm + val [rty, rty'] = (binder_types o fastype_of) parametrized_relator + val thy = Proof_Context.theory_of lthy + val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty + val crel_subst = Envir.subst_term (tyenv_match,Vartab.empty) crel_poly + val lthy = Variable.declare_names parametrized_relator lthy + val (crel_typed, lthy) = yield_singleton Variable.importT_terms crel_subst lthy + val qty = (domain_type o range_type o fastype_of) crel_typed + val relcomp_op = Const (@{const_name "relcompp"}, + (rty --> rty' --> HOLogic.boolT) --> + (rty' --> qty --> HOLogic.boolT) --> + rty --> qty --> HOLogic.boolT) + val relator_type = foldr1 (op -->) ((map type_of args) @ [rty, qty, HOLogic.boolT]) + val qty_name = (fst o dest_Type) qty + val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name) + val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args) + val rhs = relcomp_op $ parametrized_relator $ crel_typed + val definition_term = Logic.mk_equals (lhs, rhs) + val ((_, (_, def_thm)), lthy) = Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), + ((Binding.empty, []), definition_term)) lthy + in + (SOME def_thm, lthy) + end + handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy)) + fun define_code_constr gen_code quot_thm lthy = let val abs = quot_thm_abs quot_thm @@ -95,10 +137,11 @@ let val _ = quot_thm_sanity_check lthy quot_thm val (_, qtyp) = quot_thm_rty_qty quot_thm - val qty_full_name = (fst o dest_Type) qtyp - val quotients = { quot_thm = quot_thm } + val (pcrel_def, lthy) = define_pcrel (quot_thm_crel quot_thm) lthy + val quotients = { quot_thm = quot_thm, pcrel_def = pcrel_def } + val qty_full_name = (fst o dest_Type) qtyp fun quot_info phi = Lifting_Info.transform_quotients phi quotients - val lthy' = case maybe_reflp_thm of + val lthy = case maybe_reflp_thm of SOME reflp_thm => lthy |> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]), [reflp_thm]) @@ -108,7 +151,7 @@ | NONE => lthy |> define_abs_type gen_code quot_thm in - lthy' + lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) end @@ -130,7 +173,7 @@ val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty fun qualify suffix = Binding.qualified true suffix qty_name - val lthy' = case maybe_reflp_thm of + val lthy = case maybe_reflp_thm of SOME reflp_thm => lthy |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]), [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}]) @@ -150,7 +193,7 @@ |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]), [quot_thm RS @{thm Quotient_abs_induct}]) in - lthy' + lthy |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]), [quot_thm RS @{thm Quotient_right_unique}]) |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]), @@ -172,7 +215,7 @@ let val transfer_attr = Attrib.internal (K Transfer.transfer_add) val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o prop_of) typedef_thm - val (T_def, lthy') = define_cr_rel rep_fun lthy + val (T_def, lthy') = define_crel rep_fun lthy val quot_thm = case typedef_set of Const ("Orderings.top_class.top", _) => diff -r 536ab2e82ead -r 01d545993e8c src/HOL/Tools/Lifting/lifting_term.ML --- a/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 26 14:20:36 2012 +0100 +++ b/src/HOL/Tools/Lifting/lifting_term.ML Mon Nov 26 14:20:51 2012 +0100 @@ -7,6 +7,7 @@ signature LIFTING_TERM = sig exception QUOT_THM of typ * typ * Pretty.T + exception PARAM_QUOT_THM of typ * Pretty.T exception CHECK_RTY of typ * typ val prove_quot_thm: Proof.context -> typ * typ -> thm @@ -14,17 +15,19 @@ val abs_fun: Proof.context -> typ * typ -> term val equiv_relation: Proof.context -> typ * typ -> term + + val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list end structure Lifting_Term: LIFTING_TERM = struct - open Lifting_Util infix 0 MRSL exception QUOT_THM_INTERNAL of Pretty.T exception QUOT_THM of typ * typ * Pretty.T +exception PARAM_QUOT_THM of typ * Pretty.T exception CHECK_RTY of typ * typ fun match ctxt err ty_pat ty = @@ -235,4 +238,51 @@ fun equiv_relation ctxt (rty, qty) = quot_thm_rel (prove_quot_thm ctxt (rty, qty)) +fun get_fresh_Q_t ctxt = + let + val Q_t = Syntax.read_term ctxt "Trueprop (Quotient R Abs Rep T)" + val ctxt = Variable.declare_names Q_t ctxt + val frees_Q_t = Term.add_free_names Q_t [] + val (_, ctxt) = Variable.variant_fixes frees_Q_t ctxt + in + (Q_t, ctxt) + end + +fun prove_param_quot_thm ctxt ty = + let + fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = + if null tys + then + let + val thy = Proof_Context.theory_of ctxt + val instantiated_id_quot_thm = instantiate' [SOME (ctyp_of thy ty)] [] @{thm identity_quotient} + in + (instantiated_id_quot_thm, (table, ctxt)) + end + else + let + val (args, table_ctxt) = fold_map generate tys table_ctxt + in + (args MRSL (get_rel_quot_thm ctxt s), table_ctxt) + end + | generate (ty as (TVar _)) (table, ctxt) = + if AList.defined (op=) table ty + then (the (AList.lookup (op=) table ty), (table, ctxt)) + else + let + val thy = Proof_Context.theory_of ctxt + val (Q_t, ctxt') = get_fresh_Q_t ctxt + val Q_thm = Thm.assume (cterm_of thy Q_t) + val table' = (ty, Q_thm)::table + in + (Q_thm, (table', ctxt')) + end + | generate _ _ = error "generate_param_quot_thm: TFree" + + val (param_quot_thm, (table, _)) = generate ty ([], ctxt) + in + (param_quot_thm, rev table) + end + handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) + end;