--- 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 \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b fset \<Rightarrow> bool"
- where "cr_fset' R = list_all2 R OO cr_fset"
-
-lemma right_unique_cr_fset' [transfer_rule]:
- "right_unique A \<Longrightarrow> right_unique (cr_fset' A)"
- unfolding cr_fset'_def
+lemma right_unique_pcr_fset [transfer_rule]:
+ "right_unique A \<Longrightarrow> 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 \<Longrightarrow> right_total (cr_fset' A)"
- unfolding cr_fset'_def
+lemma right_total_pcr_fset [transfer_rule]:
+ "right_total A \<Longrightarrow> 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 \<Longrightarrow> bi_total (cr_fset' A)"
- unfolding cr_fset'_def
+lemma bi_total_pcr_fset [transfer_rule]:
+ "bi_total A \<Longrightarrow> 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)
--- 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:"
--- 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", _) =>
--- 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;