lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
--- a/src/HOL/Lifting.thy Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Lifting.thy Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
theory Lifting
imports Equiv_Relations Transfer
keywords
+ "parametric" and
"print_quotmaps" "print_quotients" :: diag and
"lift_definition" :: thy_goal and
"setup_lifting" :: thy_decl
@@ -342,6 +343,16 @@
unfolding bi_unique_def T_def
by (simp add: type_definition.Rep_inject [OF type])
+(* the following two theorems are here only for convinience *)
+
+lemma typedef_right_unique: "right_unique T"
+ using T_def type Quotient_right_unique typedef_to_Quotient
+ by blast
+
+lemma typedef_right_total: "right_total T"
+ using T_def type Quotient_right_total typedef_to_Quotient
+ by blast
+
lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
unfolding fun_rel_def T_def by simp
@@ -410,6 +421,125 @@
lemma reflp_equality: "reflp (op =)"
by (auto intro: reflpI)
+text {* Proving a parametrized correspondence relation *}
+
+lemma eq_OO: "op= OO R = R"
+unfolding OO_def by metis
+
+definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+"POS A B \<equiv> A \<le> B"
+
+definition NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+"NEG A B \<equiv> B \<le> A"
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
+ where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
+(*
+ The following two rules are here because we don't have any proper
+ left-unique ant left-total relations. Left-unique and left-total
+ assumptions show up in distributivity rules for the function type.
+*)
+
+lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
+unfolding bi_unique_def left_unique_def by blast
+
+lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
+unfolding bi_total_def left_total_def by blast
+
+lemma pos_OO_eq:
+ shows "POS (A OO op=) A"
+unfolding POS_def OO_def by blast
+
+lemma pos_eq_OO:
+ shows "POS (op= OO A) A"
+unfolding POS_def OO_def by blast
+
+lemma neg_OO_eq:
+ shows "NEG (A OO op=) A"
+unfolding NEG_def OO_def by auto
+
+lemma neg_eq_OO:
+ shows "NEG (op= OO A) A"
+unfolding NEG_def OO_def by blast
+
+lemma POS_trans:
+ assumes "POS A B"
+ assumes "POS B C"
+ shows "POS A C"
+using assms unfolding POS_def by auto
+
+lemma NEG_trans:
+ assumes "NEG A B"
+ assumes "NEG B C"
+ shows "NEG A C"
+using assms unfolding NEG_def by auto
+
+lemma POS_NEG:
+ "POS A B \<equiv> NEG B A"
+ unfolding POS_def NEG_def by auto
+
+lemma NEG_POS:
+ "NEG A B \<equiv> POS B A"
+ unfolding POS_def NEG_def by auto
+
+lemma POS_pcr_rule:
+ assumes "POS (A OO B) C"
+ shows "POS (A OO B OO X) (C OO X)"
+using assms unfolding POS_def OO_def by blast
+
+lemma NEG_pcr_rule:
+ assumes "NEG (A OO B) C"
+ shows "NEG (A OO B OO X) (C OO X)"
+using assms unfolding NEG_def OO_def by blast
+
+lemma POS_apply:
+ assumes "POS R R'"
+ assumes "R f g"
+ shows "R' f g"
+using assms unfolding POS_def by auto
+
+text {* Proving a parametrized correspondence relation *}
+
+lemma fun_mono:
+ assumes "A \<ge> C"
+ assumes "B \<le> D"
+ shows "(A ===> B) \<le> (C ===> D)"
+using assms unfolding fun_rel_def by blast
+
+lemma pos_fun_distr: "((R ===> S) OO (R' ===> S')) \<le> ((R OO R') ===> (S OO S'))"
+unfolding OO_def fun_rel_def by blast
+
+lemma functional_relation: "right_unique R \<Longrightarrow> left_total R \<Longrightarrow> \<forall>x. \<exists>!y. R x y"
+unfolding right_unique_def left_total_def by blast
+
+lemma functional_converse_relation: "left_unique R \<Longrightarrow> right_total R \<Longrightarrow> \<forall>y. \<exists>!x. R x y"
+unfolding left_unique_def right_total_def by blast
+
+lemma neg_fun_distr1:
+assumes 1: "left_unique R" "right_total R"
+assumes 2: "right_unique R'" "left_total R'"
+shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S')) "
+ using functional_relation[OF 2] functional_converse_relation[OF 1]
+ unfolding fun_rel_def OO_def
+ apply clarify
+ apply (subst all_comm)
+ apply (subst all_conj_distrib[symmetric])
+ apply (intro choice)
+ by metis
+
+lemma neg_fun_distr2:
+assumes 1: "right_unique R'" "left_total R'"
+assumes 2: "left_unique S'" "right_total S'"
+shows "(R OO R' ===> S OO S') \<le> ((R ===> S) OO (R' ===> S'))"
+ using functional_converse_relation[OF 2] functional_relation[OF 1]
+ unfolding fun_rel_def OO_def
+ apply clarify
+ apply (subst all_comm)
+ apply (subst all_conj_distrib[symmetric])
+ apply (intro choice)
+ by metis
+
subsection {* ML setup *}
ML_file "Tools/Lifting/lifting_util.ML"
@@ -417,8 +547,12 @@
ML_file "Tools/Lifting/lifting_info.ML"
setup Lifting_Info.setup
+lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
+
+(* setup for the function type *)
declare fun_quotient[quot_map]
-lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
+declare fun_mono[relator_mono]
+lemmas [relator_distr] = pos_fun_distr neg_fun_distr1 neg_fun_distr2
ML_file "Tools/Lifting/lifting_term.ML"
@@ -426,6 +560,6 @@
ML_file "Tools/Lifting/lifting_setup.ML"
-hide_const (open) invariant
+hide_const (open) invariant POS NEG
end
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Mar 08 13:14:23 2013 +0100
@@ -6,11 +6,14 @@
signature LIFTING_DEF =
sig
+ val generate_parametric_transfer_rule:
+ Proof.context -> thm -> thm -> thm
+
val add_lift_def:
- (binding * mixfix) -> typ -> term -> thm -> local_theory -> local_theory
+ (binding * mixfix) -> typ -> term -> thm -> thm option -> local_theory -> local_theory
val lift_def_cmd:
- (binding * string option * mixfix) * string -> local_theory -> Proof.state
+ (binding * string option * mixfix) * string * (Facts.ref * Args.src list) option -> local_theory -> Proof.state
val can_generate_code_cert: thm -> bool
end;
@@ -22,6 +25,103 @@
infix 0 MRSL
+(* Generation of a transfer rule *)
+
+fun generate_parametric_transfer_rule ctxt transfer_rule parametric_transfer_rule =
+ let
+ fun preprocess ctxt thm =
+ let
+ val tm = (strip_args 2 o HOLogic.dest_Trueprop o concl_of) thm;
+ val param_rel = (snd o dest_comb o fst o dest_comb) tm;
+ val thy = Proof_Context.theory_of ctxt;
+ val free_vars = Term.add_vars param_rel [];
+
+ fun make_subst (var as (_, typ)) subst =
+ let
+ val [rty, rty'] = binder_types typ
+ in
+ if (Term.is_TVar rty andalso is_Type rty') then
+ (Var var, HOLogic.eq_const rty')::subst
+ else
+ subst
+ end;
+
+ val subst = fold make_subst free_vars [];
+ val csubst = map (pairself (cterm_of thy)) subst;
+ val inst_thm = Drule.cterm_instantiate csubst thm;
+ in
+ Conv.fconv_rule
+ ((Conv.concl_conv (nprems_of inst_thm) o HOLogic.Trueprop_conv o Conv.fun2_conv o Conv.arg1_conv)
+ (Raw_Simplifier.rewrite false (Transfer.get_sym_relator_eq ctxt))) inst_thm
+ end
+
+ fun inst_relcomppI thy ant1 ant2 =
+ let
+ val t1 = (HOLogic.dest_Trueprop o concl_of) ant1
+ val t2 = (HOLogic.dest_Trueprop o prop_of) ant2
+ val fun1 = cterm_of thy (strip_args 2 t1)
+ val args1 = map (cterm_of thy) (get_args 2 t1)
+ val fun2 = cterm_of thy (strip_args 2 t2)
+ val args2 = map (cterm_of thy) (get_args 1 t2)
+ val relcomppI = Drule.incr_indexes2 ant1 ant2 @{thm relcomppI}
+ val vars = (rev (Term.add_vars (prop_of relcomppI) []))
+ val subst = map (apfst ((cterm_of thy) o Var)) (vars ~~ ([fun1] @ args1 @ [fun2] @ args2))
+ in
+ Drule.cterm_instantiate subst relcomppI
+ end
+
+ fun zip_transfer_rules ctxt thm =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ fun mk_POS ty = Const (@{const_name POS}, ty --> ty --> HOLogic.boolT)
+ val rel = (Thm.dest_fun2 o Thm.dest_arg o cprop_of) thm
+ val typ = (typ_of o ctyp_of_term) rel
+ val POS_const = cterm_of thy (mk_POS typ)
+ val var = cterm_of thy (Var (("X", #maxidx (rep_cterm (rel)) + 1), typ))
+ val goal = Thm.apply (cterm_of thy HOLogic.Trueprop) (Thm.apply (Thm.apply POS_const rel) var)
+ in
+ [Lifting_Term.merge_transfer_relations ctxt goal, thm] MRSL @{thm POS_apply}
+ end
+
+ val thm = (inst_relcomppI (Proof_Context.theory_of ctxt) parametric_transfer_rule transfer_rule)
+ OF [parametric_transfer_rule, transfer_rule]
+ val preprocessed_thm = preprocess ctxt thm
+ val orig_ctxt = ctxt
+ val (fixed_thm, ctxt) = yield_singleton (apfst snd oo Variable.import true) preprocessed_thm ctxt
+ val assms = cprems_of fixed_thm
+ val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add
+ val ctxt = Context.proof_map(fold (add_transfer_rule o Thm.assume) assms) ctxt
+ val zipped_thm =
+ fixed_thm
+ |> undisch_all
+ |> zip_transfer_rules ctxt
+ |> implies_intr_list assms
+ |> singleton (Variable.export ctxt orig_ctxt)
+ in
+ zipped_thm
+ end
+
+fun print_generate_transfer_info msg =
+ let
+ val error_msg = cat_lines
+ ["Generation of a parametric transfer rule failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+ in
+ error error_msg
+ end
+
+fun generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm =
+ let
+ val transfer_rule =
+ ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
+ |> Morphism.thm (Local_Theory.target_morphism lthy)
+ |> Lifting_Term.parametrize_transfer_rule lthy
+ in
+ (option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm
+ handle Lifting_Term.MERGE_TRANSFER_REL msg => (print_generate_transfer_info msg; transfer_rule))
+ end
+
(* Generation of the code certificate from the rsp theorem *)
fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
@@ -233,8 +333,8 @@
else
lthy
-fun define_code_using_rep_eq maybe_rep_eq_thm lthy =
- case maybe_rep_eq_thm of
+fun define_code_using_rep_eq opt_rep_eq_thm lthy =
+ case opt_rep_eq_thm of
SOME rep_eq_thm =>
let
val add_abs_eqn_attribute =
@@ -267,7 +367,7 @@
false
end
-fun define_code abs_eq_thm maybe_rep_eq_thm (rty, qty) lthy =
+fun define_code abs_eq_thm opt_rep_eq_thm (rty, qty) lthy =
let
val (rty_body, qty_body) = get_body_types (rty, qty)
in
@@ -275,7 +375,7 @@
if null (Logic.strip_imp_prems(prop_of abs_eq_thm)) then
(snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [abs_eq_thm]) lthy
else
- (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the maybe_rep_eq_thm]) lthy
+ (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [the opt_rep_eq_thm]) lthy
else
let
val body_quot_thm = Lifting_Term.prove_quot_thm lthy (rty_body, qty_body)
@@ -283,7 +383,7 @@
if has_constr lthy body_quot_thm then
define_code_using_abs_eq abs_eq_thm lthy
else if has_abstr lthy body_quot_thm then
- define_code_using_rep_eq maybe_rep_eq_thm lthy
+ define_code_using_rep_eq opt_rep_eq_thm lthy
else
lthy
end
@@ -300,7 +400,7 @@
i.e. "(Lifting_Term.equiv_relation (fastype_of rhs, qty)) $ rhs $ rhs"
*)
-fun add_lift_def var qty rhs rsp_thm lthy =
+fun add_lift_def var qty rhs rsp_thm opt_par_thm lthy =
let
val rty = fastype_of rhs
val quot_thm = Lifting_Term.prove_quot_thm lthy (rty, qty)
@@ -316,10 +416,10 @@
Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) lthy'
- val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
+ val transfer_rule = generate_transfer_rule lthy quot_thm rsp_thm def_thm opt_par_thm
val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm
- val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
+ val opt_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty)
fun qualify defname suffix = Binding.qualified true suffix defname
@@ -327,17 +427,17 @@
val rsp_thm_name = qualify lhs_name "rsp"
val abs_eq_thm_name = qualify lhs_name "abs_eq"
val rep_eq_thm_name = qualify lhs_name "rep_eq"
- val transfer_thm_name = qualify lhs_name "transfer"
+ val transfer_rule_name = qualify lhs_name "transfer"
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
in
lthy'
|> (snd oo Local_Theory.note) ((rsp_thm_name, []), [rsp_thm])
- |> (snd oo Local_Theory.note) ((transfer_thm_name, [transfer_attr]), [transfer_thm])
+ |> (snd oo Local_Theory.note) ((transfer_rule_name, [transfer_attr]), [transfer_rule])
|> (snd oo Local_Theory.note) ((abs_eq_thm_name, []), [abs_eq_thm])
- |> (case maybe_rep_eq_thm of
+ |> (case opt_rep_eq_thm of
SOME rep_eq_thm => (snd oo Local_Theory.note) ((rep_eq_thm_name, []), [rep_eq_thm])
| NONE => I)
- |> define_code abs_eq_thm maybe_rep_eq_thm (rty_forced, qty)
+ |> define_code abs_eq_thm opt_rep_eq_thm (rty_forced, qty)
end
fun mk_readable_rsp_thm_eq tm lthy =
@@ -397,7 +497,7 @@
*)
-fun lift_def_cmd (raw_var, rhs_raw) lthy =
+fun lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy =
let
val ((binding, SOME qty, mx), lthy') = yield_singleton Proof_Context.read_vars raw_var lthy
val rhs = (Syntax.check_term lthy' o Syntax.parse_term lthy') rhs_raw
@@ -422,23 +522,24 @@
val forced_rhs = force_rty_type lthy' rty_forced rhs;
val internal_rsp_tm = HOLogic.mk_Trueprop (rsp_rel $ forced_rhs $ forced_rhs)
val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy'
- val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
+ val opt_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
val readable_rsp_tm_tnames = rename_to_tnames lthy' readable_rsp_tm
+ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy')) opt_par_xthm
fun after_qed thm_list lthy =
let
val internal_rsp_thm =
case thm_list of
- [] => the maybe_proven_rsp_thm
+ [] => the opt_proven_rsp_thm
| [[thm]] => Goal.prove lthy [] [] internal_rsp_tm
(fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
in
- add_lift_def (binding, mx) qty rhs internal_rsp_thm lthy
+ add_lift_def (binding, mx) qty rhs internal_rsp_thm opt_par_thm lthy
end
in
- case maybe_proven_rsp_thm of
+ case opt_proven_rsp_thm of
SOME _ => Proof.theorem NONE after_qed [] lthy'
| NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm_tnames,[])]] lthy'
end
@@ -480,17 +581,16 @@
error error_msg
end
-fun lift_def_cmd_with_err_handling (raw_var, rhs_raw) lthy =
- (lift_def_cmd (raw_var, rhs_raw) lthy
+fun lift_def_cmd_with_err_handling (raw_var, rhs_raw, opt_par_xthm) lthy =
+ (lift_def_cmd (raw_var, rhs_raw, opt_par_xthm) lthy
handle Lifting_Term.QUOT_THM (rty, qty, msg) => quot_thm_err lthy (rty, qty) msg)
handle Lifting_Term.CHECK_RTY (rty_schematic, rty_forced) =>
check_rty_err lthy (rty_schematic, rty_forced) (raw_var, rhs_raw)
(* parser and command *)
val liftdef_parser =
- ((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
- --| @{keyword "is"} -- Parse.term
-
+ (((Parse.binding -- (@{keyword "::"} |-- (Parse.typ >> SOME) -- Parse.opt_mixfix')) >> Parse.triple2)
+ --| @{keyword "is"} -- Parse.term -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)) >> Parse.triple1
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "lift_definition"}
"definition for constants over the quotient type"
--- a/src/HOL/Tools/Lifting/lifting_info.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML Fri Mar 08 13:14:23 2013 +0100
@@ -11,7 +11,8 @@
val lookup_quotmaps_global: theory -> string -> quotmaps option
val print_quotmaps: Proof.context -> unit
- type quotients = {quot_thm: thm, pcrel_def: thm option}
+ type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
+ type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
val transform_quotients: morphism -> quotients -> quotients
val lookup_quotients: Proof.context -> string -> quotients option
val lookup_quotients_global: theory -> string -> quotients option
@@ -25,6 +26,11 @@
val add_reflexivity_rule_attribute: attribute
val add_reflexivity_rule_attrib: Attrib.src
+ type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
+ pos_distr_rules: thm list, neg_distr_rules: thm list}
+ val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
+ val lookup_relator_distr_data_global: theory -> string -> relator_distr_data option
+
val setup: theory -> theory
end;
@@ -118,7 +124,8 @@
end
(* info about quotient types *)
-type quotients = {quot_thm: thm, pcrel_def: thm option}
+type pcrel_info = {pcrel_def: thm, pcr_cr_eq: thm}
+type quotients = {quot_thm: thm, pcrel_info: pcrel_info option}
structure Quotients = Generic_Data
(
@@ -128,8 +135,11 @@
fun merge data = Symtab.merge (K true) data
)
-fun transform_quotients phi {quot_thm, pcrel_def} =
- {quot_thm = Morphism.thm phi quot_thm, pcrel_def = Option.map (Morphism.thm phi) pcrel_def}
+fun transform_pcrel_info phi {pcrel_def, pcr_cr_eq} =
+ {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
+
+fun transform_quotients phi {quot_thm, pcrel_info} =
+ {quot_thm = Morphism.thm phi quot_thm, pcrel_info = Option.map (transform_pcrel_info phi) pcrel_info}
val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
@@ -141,9 +151,9 @@
val (_, qtyp) = quot_thm_rty_qty quot_thm
val qty_full_name = (fst o dest_Type) qtyp
val symtab = Quotients.get ctxt
- val maybe_stored_quot_thm = Symtab.lookup symtab qty_full_name
+ val opt_stored_quot_thm = Symtab.lookup symtab qty_full_name
in
- case maybe_stored_quot_thm of
+ case opt_stored_quot_thm of
SOME data =>
if Thm.eq_thm_prop (#quot_thm data, quot_thm) then
Quotients.map (Symtab.delete qty_full_name) ctxt
@@ -157,14 +167,16 @@
fun print_quotients ctxt =
let
- fun prt_quot (qty_name, {quot_thm, pcrel_def}) =
+ fun prt_quot (qty_name, {quot_thm, pcrel_info}) =
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),
Pretty.str "pcrel_def thm:",
- option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of) pcrel_def])
+ option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcrel_info,
+ Pretty.str "pcr_cr_eq thm:",
+ option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcrel_info])
in
map prt_quot (Symtab.dest (Quotients.get (Context.Proof ctxt)))
|> Pretty.big_list "quotients:"
@@ -193,6 +205,211 @@
val add_reflexivity_rule_attribute = Reflp_Preserve.add
val add_reflexivity_rule_attrib = Attrib.internal (K add_reflexivity_rule_attribute)
+(* info about relator distributivity theorems *)
+type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm,
+ pos_distr_rules: thm list, neg_distr_rules: thm list}
+
+fun map_relator_distr_data f1 f2 f3 f4
+ {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
+ {pos_mono_rule = f1 pos_mono_rule,
+ neg_mono_rule = f2 neg_mono_rule,
+ pos_distr_rules = f3 pos_distr_rules,
+ neg_distr_rules = f4 neg_distr_rules}
+
+fun map_pos_mono_rule f = map_relator_distr_data f I I I
+fun map_neg_mono_rule f = map_relator_distr_data I f I I
+fun map_pos_distr_rules f = map_relator_distr_data I I f I
+fun map_neg_distr_rules f = map_relator_distr_data I I I f
+
+structure Relator_Distr = Generic_Data
+(
+ type T = relator_distr_data Symtab.table
+ val empty = Symtab.empty
+ val extend = I
+ fun merge data = Symtab.merge (K true) data
+);
+
+fun introduce_polarities rule =
+ let
+ val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT
+ val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)
+ val equal_prems = filter op= prems_pairs
+ val _ = if null equal_prems then ()
+ else error "The rule contains reflexive assumptions."
+ val concl_pairs = rule
+ |> concl_of
+ |> HOLogic.dest_Trueprop
+ |> dest_less_eq
+ |> pairself (snd o strip_comb)
+ |> op~~
+ |> filter_out op=
+
+ val _ = if has_duplicates op= concl_pairs
+ then error "The rule contains duplicated variables in the conlusion." else ()
+
+ fun mem a l = member op= l a
+
+ fun rewrite_prem prem_pair =
+ if mem prem_pair concl_pairs
+ then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
+ else if mem (swap prem_pair) concl_pairs
+ then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
+ else error "The rule contains a non-relevant assumption."
+
+ fun rewrite_prems [] = Conv.all_conv
+ | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)
+
+ val rewrite_prems_conv = rewrite_prems prems_pairs
+ val rewrite_concl_conv =
+ Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))
+ in
+ (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule
+ end
+ handle
+ TERM _ => error "The rule has a wrong format."
+ | CTERM _ => error "The rule has a wrong format."
+
+fun negate_mono_rule mono_rule =
+ let
+ val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])
+ in
+ Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
+ end;
+
+fun add_mono_rule mono_rule ctxt =
+ let
+ val mono_rule = introduce_polarities mono_rule
+ val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
+ dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) mono_rule
+ val _ = if Symtab.defined (Relator_Distr.get ctxt) mono_ruleT_name
+ then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
+ else ()
+ val neg_mono_rule = negate_mono_rule mono_rule
+ val relator_distr_data = {pos_mono_rule = mono_rule, neg_mono_rule = neg_mono_rule,
+ pos_distr_rules = [], neg_distr_rules = []}
+ in
+ Relator_Distr.map (Symtab.update (mono_ruleT_name, relator_distr_data)) ctxt
+ end;
+
+local
+ fun add_distr_rule update_entry distr_rule ctxt =
+ let
+ val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o
+ dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
+ in
+ if Symtab.defined (Relator_Distr.get ctxt) distr_ruleT_name then
+ Relator_Distr.map (Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) ctxt
+ else error "The monoticity rule is not defined."
+ end
+
+ fun rewrite_concl_conv thm ctm =
+ Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
+ handle CTERM _ => error "The rule has a wrong format."
+
+in
+ fun add_pos_distr_rule distr_rule ctxt =
+ let
+ val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
+ fun update_entry distr_rule data =
+ map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
+ in
+ add_distr_rule update_entry distr_rule ctxt
+ end
+ handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
+
+
+ fun add_neg_distr_rule distr_rule ctxt =
+ let
+ val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
+ fun update_entry distr_rule data =
+ map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
+ in
+ add_distr_rule update_entry distr_rule ctxt
+ end
+ handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
+end
+
+local
+ val eq_refl2 = sym RS @{thm eq_refl}
+in
+ fun add_eq_distr_rule distr_rule ctxt =
+ let
+ val pos_distr_rule = @{thm eq_refl} OF [distr_rule]
+ val neg_distr_rule = eq_refl2 OF [distr_rule]
+ in
+ ctxt
+ |> add_pos_distr_rule pos_distr_rule
+ |> add_neg_distr_rule neg_distr_rule
+ end
+end;
+
+local
+ fun sanity_check rule =
+ let
+ val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
+ val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
+ val (lhs, rhs) = case concl of
+ Const ("Orderings.ord_class.less_eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs =>
+ (lhs, rhs)
+ | Const ("Orderings.ord_class.less_eq", _) $ rhs $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) =>
+ (lhs, rhs)
+ | Const ("HOL.eq", _) $ (lhs as Const ("Relation.relcompp",_) $ _ $ _) $ rhs => (lhs, rhs)
+ | _ => error "The rule has a wrong format."
+
+ val lhs_vars = Term.add_vars lhs []
+ val rhs_vars = Term.add_vars rhs []
+ val assms_vars = fold Term.add_vars assms [];
+ val _ = if has_duplicates op= lhs_vars then error "Left-hand side has variable duplicates" else ()
+ val _ = if subset op= (rhs_vars, lhs_vars) then ()
+ else error "Extra variables in the right-hand side of the rule"
+ val _ = if subset op= (assms_vars, lhs_vars) then ()
+ else error "Extra variables in the assumptions of the rule"
+ val rhs_args = (snd o strip_comb) rhs;
+ fun check_comp t = case t of
+ Const ("Relation.relcompp", _) $ Var (_, _) $ Var (_,_) => ()
+ | _ => error "There is an argument on the rhs that is not a composition."
+ val _ = map check_comp rhs_args
+ in
+ ()
+ end
+in
+
+ fun add_distr_rule distr_rule ctxt =
+ let
+ val _ = sanity_check distr_rule
+ val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
+ in
+ case concl of
+ Const ("Orderings.ord_class.less_eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
+ add_pos_distr_rule distr_rule ctxt
+ | Const ("Orderings.ord_class.less_eq", _) $ _ $ (Const ("Relation.relcompp",_) $ _ $ _) =>
+ add_neg_distr_rule distr_rule ctxt
+ | Const ("HOL.eq", _) $ (Const ("Relation.relcompp",_) $ _ $ _) $ _ =>
+ add_eq_distr_rule distr_rule ctxt
+ end
+end
+
+fun get_distr_rules_raw ctxt = Symtab.fold
+ (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules)
+ (Relator_Distr.get ctxt) []
+
+fun get_mono_rules_raw ctxt = Symtab.fold
+ (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules)
+ (Relator_Distr.get ctxt) []
+
+val lookup_relator_distr_data = Symtab.lookup o Relator_Distr.get o Context.Proof
+val lookup_relator_distr_data_global = Symtab.lookup o Relator_Distr.get o Context.Theory
+
+val relator_distr_attribute_setup =
+ Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
+ "declaration of relator's monoticity"
+ #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
+ "declaration of relator's distributivity over OO"
+ #> Global_Theory.add_thms_dynamic
+ (@{binding relator_distr_raw}, get_distr_rules_raw)
+ #> Global_Theory.add_thms_dynamic
+ (@{binding relator_mono_raw}, get_mono_rules_raw)
+
(* theory setup *)
val setup =
@@ -200,6 +417,7 @@
#> quot_del_attribute_setup
#> Invariant_Commute.setup
#> Reflp_Preserve.setup
+ #> relator_distr_attribute_setup
(* outer syntax commands *)
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Fri Mar 08 13:14:23 2013 +0100
@@ -8,7 +8,7 @@
sig
exception SETUP_LIFTING_INFR of string
- val setup_by_quotient: bool -> thm -> thm option -> local_theory -> local_theory
+ val setup_by_quotient: bool -> thm -> thm option -> thm option -> local_theory -> local_theory
val setup_by_typedef_thm: bool -> thm -> local_theory -> local_theory
end;
@@ -26,7 +26,7 @@
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 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 crel_name = Binding.prefix_name "cr_" qty_name
val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
@@ -69,7 +69,7 @@
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_fixed)
- val rhs = relcomp_op $ param_rel_fixed $ fixed_crel;
+ val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
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
@@ -78,16 +78,72 @@
end
handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy))
+
+local
+ val eq_OO_meta = mk_meta_eq @{thm eq_OO}
+
+ fun print_generate_pcr_cr_eq_error ctxt term =
+ let
+ val goal = (Const ("HOL.eq", dummyT)) $ term $ Const ("HOL.eq", dummyT)
+ val error_msg = cat_lines
+ ["Generation of a pcr_cr_eq failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])),
+ "Most probably a relator_eq rule for one of the involved types is missing."]
+ in
+ error error_msg
+ end
+in
+ fun define_pcr_cr_eq lthy pcr_rel_def =
+ let
+ val lhs = (term_of o Thm.lhs_of) pcr_rel_def
+ val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type o List.last o binder_types o fastype_of) lhs
+ val args = (snd o strip_comb) lhs
+
+ fun make_inst var ctxt =
+ let
+ val typ = (snd o relation_types o snd o dest_Var) var
+ val sort = Type.sort_of_atyp typ
+ val (fresh_var, ctxt) = yield_singleton Variable.invent_types sort ctxt
+ val thy = Proof_Context.theory_of ctxt
+ in
+ ((cterm_of thy var, cterm_of thy (HOLogic.eq_const (TFree fresh_var))), ctxt)
+ end
+
+ val orig_lthy = lthy
+ val (args_inst, lthy) = fold_map make_inst args lthy
+ val pcr_cr_eq =
+ pcr_rel_def
+ |> Drule.cterm_instantiate args_inst
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (bottom_rewr_conv (Transfer.get_relator_eq lthy))))
+ in
+ case (term_of o Thm.rhs_of) pcr_cr_eq of
+ Const (@{const_name "relcompp"}, _) $ Const ("HOL.eq", _) $ _ =>
+ let
+ val thm =
+ pcr_cr_eq
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta))
+ |> mk_HOL_eq
+ |> singleton (Variable.export lthy orig_lthy)
+ val ((_, [thm]), lthy) = Local_Theory.note ((Binding.qualified true "pcr_cr_eq" qty_name, []),
+ [thm]) lthy
+ in
+ (thm, lthy)
+ end
+ | Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t
+ | _ => error "generate_pcr_cr_eq: implementation error"
+ end
+end
+
fun define_code_constr gen_code quot_thm lthy =
let
val abs = quot_thm_abs quot_thm
- val abs_background = Morphism.term (Local_Theory.target_morphism lthy) abs
in
- if gen_code andalso is_Const abs_background then
+ if gen_code andalso is_Const abs then
let
- val (fixed_abs_background, lthy') = yield_singleton(Variable.importT_terms) abs_background lthy
+ val (fixed_abs, lthy') = yield_singleton(Variable.importT_terms) abs lthy
in
- Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs_background]) lthy'
+ Local_Theory.background_theory(Code.add_datatype [dest_Const fixed_abs]) lthy'
end
else
lthy
@@ -99,7 +155,7 @@
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
val add_abstype_attribute =
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
- val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+ val add_abstype_attrib = Attrib.internal (K add_abstype_attribute)
in
lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
@@ -133,15 +189,24 @@
@ (map Pretty.string_of errs)))
end
-fun setup_lifting_infr gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_lifting_infr gen_code quot_thm opt_reflp_thm lthy =
let
val _ = quot_thm_sanity_check lthy quot_thm
val (_, qtyp) = quot_thm_rty_qty 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 pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def
+ (**)
+ val (pcr_cr_eq, lthy) = case pcrel_def of
+ SOME pcrel_def => apfst SOME (define_pcr_cr_eq lthy pcrel_def)
+ | NONE => (NONE, lthy)
+ val pcrel_info = case pcrel_def of
+ SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq }
+ | NONE => NONE
+ val quotients = { quot_thm = quot_thm, pcrel_info = pcrel_info }
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 opt_reflp_thm of
SOME reflp_thm => lthy
|> (snd oo Local_Theory.note) ((Binding.empty, [Lifting_Info.add_reflexivity_rule_attrib]),
[reflp_thm])
@@ -156,51 +221,247 @@
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
end
+local
+ val OO_rules = [@{thm bi_total_OO}, @{thm bi_unique_OO}, @{thm right_total_OO}, @{thm right_unique_OO}]
+in
+ fun parametrize_class_constraint ctxt pcr_def constraint =
+ let
+ fun generate_transfer_rule pcr_def constraint goal ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val orig_ctxt = ctxt
+ val (fixed_goal, ctxt) = yield_singleton (Variable.import_terms true) goal ctxt
+ val init_goal = Goal.init (cterm_of thy fixed_goal)
+ val rules = Transfer.get_transfer_raw ctxt
+ val rules = constraint :: OO_rules @ rules
+ val tac = K (Local_Defs.unfold_tac ctxt [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac rules)
+ in
+ (singleton (Variable.export ctxt orig_ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal))
+ end
+
+ fun make_goal pcr_def constr =
+ let
+ val pred_name = (fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o prop_of) constr
+ val arg = (fst o Logic.dest_equals o prop_of) pcr_def
+ in
+ HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg)
+ end
+
+ val check_assms =
+ let
+ val right_names = ["bi_total", "bi_unique", "right_total", "right_unique"]
+
+ fun is_right_name name = member op= right_names (Long_Name.base_name name)
+
+ fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name
+ | is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name
+ | is_trivial_assm _ = false
+ in
+ fn thm =>
+ let
+ val prems = map HOLogic.dest_Trueprop (prems_of thm)
+ val thm_name = (Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o concl_of) thm
+ val non_trivial_assms = filter_out is_trivial_assm prems
+ in
+ if null non_trivial_assms then ()
+ else
+ let
+ val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ",
+ Pretty.str thm_name,
+ Pretty.str " transfer rule found:",
+ Pretty.brk 1] @
+ ((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @
+ [Pretty.str "."])
+ in
+ warning (Pretty.str_of pretty_msg)
+ end
+ end
+ end
+
+ val goal = make_goal pcr_def constraint
+ val thm = generate_transfer_rule pcr_def constraint goal ctxt
+ val _ = check_assms thm
+ in
+ thm
+ end
+end
+
+local
+ val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def}))
+in
+ fun generate_parametric_id lthy rty id_transfer_rule =
+ let
+ val orig_lthy = lthy
+ (* it doesn't raise an exception because it would have already raised it in define_pcrel *)
+ val (quot_thm, _, lthy) = Lifting_Term.prove_param_quot_thm lthy rty
+ val parametrized_relator = singleton (Variable.export_terms lthy orig_lthy) (quot_thm_crel quot_thm);
+ val lthy = orig_lthy
+ val id_transfer =
+ @{thm id_transfer}
+ |> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1)
+ |> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold))
+ val var = Var (hd (Term.add_vars (prop_of id_transfer) []));
+ val thy = Proof_Context.theory_of lthy;
+ val inst = [(cterm_of thy var, cterm_of thy parametrized_relator)]
+ val id_par_thm = Drule.cterm_instantiate inst id_transfer;
+ in
+ Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm
+ end
+ handle Lifting_Term.MERGE_TRANSFER_REL msg =>
+ let
+ val error_msg = cat_lines
+ ["Generation of a parametric transfer rule for the abs. or the rep. function failed.",
+ "A non-parametric version will be used.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+ in
+ (warning error_msg; id_transfer_rule)
+ end
+end
+
+fun parametrize_quantifier lthy quant_transfer_rule =
+ Lifting_Term.parametrize_transfer_rule lthy quant_transfer_rule
+
+fun get_pcrel_info ctxt qty_full_name =
+ #pcrel_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name))
+
(*
Sets up the Lifting package by a quotient theorem.
gen_code - flag if an abstract type given by quot_thm should be registred
as an abstract type in the code generator
quot_thm - a quotient theorem (Quotient R Abs Rep T)
- maybe_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
+ opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive
(in the form "reflp R")
*)
-fun setup_by_quotient gen_code quot_thm maybe_reflp_thm lthy =
+fun setup_by_quotient gen_code quot_thm opt_reflp_thm opt_par_thm lthy =
let
+ (**)
+ val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm
+ (**)
val transfer_attr = Attrib.internal (K Transfer.transfer_add)
- val (_, qty) = quot_thm_rty_qty quot_thm
+ val (rty, qty) = quot_thm_rty_qty quot_thm
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
+ val qty_full_name = (fst o dest_Type) qty
+ val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
fun qualify suffix = Binding.qualified true suffix qty_name
- 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}])
- |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_induct}])
- |> (snd oo Local_Theory.note) ((qualify "abs_eq_iff", []),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_total_abs_eq_iff}])
- | NONE => lthy
- |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_All_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_Ex_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_forall_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "abs_induct", [induct_attr]),
- [quot_thm RS @{thm Quotient_abs_induct}])
+ val lthy = case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val thms =
+ [("abs_induct", @{thm Quotient_total_abs_induct}, [induct_attr]),
+ ("abs_eq_iff", @{thm Quotient_total_abs_eq_iff}, [] )]
+ in
+ lthy
+ |> fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
+ [[quot_thm, reflp_thm] MRSL thm])) thms
+ end
+ | NONE =>
+ let
+ val thms =
+ [("abs_induct", @{thm Quotient_abs_induct}, [induct_attr])]
+ in
+ fold (fn (name, thm, attr) => (snd oo Local_Theory.note) ((qualify name, attr),
+ [quot_thm RS thm])) thms lthy
+ end
+
+ fun setup_transfer_rules_nonpar lthy =
+ let
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val thms =
+ [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+ ("bi_total", @{thm Quotient_bi_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm Quotient_All_transfer} ),
+ ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
+ ("forall_transfer",@{thm Quotient_forall_transfer})]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [quot_thm RS thm])) thms lthy
+ end
+ val thms =
+ [("rel_eq_transfer", @{thm Quotient_rel_eq_transfer}),
+ ("right_unique", @{thm Quotient_right_unique} ),
+ ("right_total", @{thm Quotient_right_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [quot_thm RS thm])) thms lthy
+ end
+
+ fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm =
+ option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm
+ handle Lifting_Term.MERGE_TRANSFER_REL msg =>
+ let
+ val error_msg = cat_lines
+ ["Generation of a parametric transfer rule for the quotient relation failed.",
+ (Pretty.string_of (Pretty.block
+ [Pretty.str "Reason:", Pretty.brk 2, msg]))]
+ in
+ error error_msg
+ end
+
+ fun setup_transfer_rules_par lthy =
+ let
+ val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val id_abs_transfer = generate_parametric_id lthy rty
+ (Lifting_Term.parametrize_transfer_rule lthy
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+ val bi_total = parametrize_class_constraint lthy pcrel_def
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val thms =
+ [("id_abs_transfer",id_abs_transfer),
+ ("bi_total", bi_total )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm Quotient_All_transfer} ),
+ ("Ex_transfer", @{thm Quotient_Ex_transfer} ),
+ ("forall_transfer",@{thm Quotient_forall_transfer})]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [parametrize_quantifier lthy (quot_thm RS thm)])) thms lthy
+ end
+ val rel_eq_transfer = generate_parametric_rel_eq lthy
+ (Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer}))
+ opt_par_thm
+ val right_unique = parametrize_class_constraint lthy pcrel_def
+ (quot_thm RS @{thm Quotient_right_unique})
+ val right_total = parametrize_class_constraint lthy pcrel_def
+ (quot_thm RS @{thm Quotient_right_total})
+ val thms =
+ [("rel_eq_transfer", rel_eq_transfer),
+ ("right_unique", right_unique ),
+ ("right_total", right_total )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+
+ fun setup_transfer_rules lthy =
+ if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
+ else setup_transfer_rules_nonpar lthy
in
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]),
- [quot_thm RS @{thm Quotient_right_total}])
- |> (snd oo Local_Theory.note) ((qualify "rel_eq_transfer", [transfer_attr]),
- [quot_thm RS @{thm Quotient_rel_eq_transfer}])
- |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
+ |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+ |> setup_transfer_rules
end
(*
@@ -215,8 +476,10 @@
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_crel rep_fun lthy
-
+ val (T_def, lthy) = define_crel rep_fun lthy
+ (**)
+ val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def
+ (**)
val quot_thm = case typedef_set of
Const ("Orderings.top_class.top", _) =>
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient}
@@ -224,49 +487,109 @@
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient}
| _ =>
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient}
-
- val (_, qty) = quot_thm_rty_qty quot_thm
- val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty
+ val (rty, qty) = quot_thm_rty_qty quot_thm
+ val qty_full_name = (fst o dest_Type) qty
+ val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
fun qualify suffix = Binding.qualified true suffix qty_name
val simplify = Raw_Simplifier.rewrite_rule [mk_meta_eq @{thm mem_Collect_eq}]
+ val opt_reflp_thm =
+ case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2})
+ | _ => NONE
- val (maybe_reflp_thm, lthy'') = case typedef_set of
- Const ("Orderings.top_class.top", _) =>
- let
- val equivp_thm = typedef_thm RS @{thm UNIV_typedef_to_equivp}
- val reflp_thm = equivp_thm RS @{thm equivp_reflp2}
- in
- lthy'
- |> (snd oo Local_Theory.note) ((qualify "bi_total", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}])
- |> (snd oo Local_Theory.note) ((qualify "id_abs_transfer", [transfer_attr]),
- [[quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}])
- |> pair (SOME reflp_thm)
- end
- | _ => lthy'
- |> (snd oo Local_Theory.note) ((qualify "All_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_All_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "Ex_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_Ex_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
- [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
- |> pair NONE
+ fun setup_transfer_rules_nonpar lthy =
+ let
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val thms =
+ [("id_abs_transfer",@{thm Quotient_id_abs_transfer}),
+ ("bi_total", @{thm Quotient_bi_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[quot_thm, reflp_thm] MRSL thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ [("All_transfer", @{thm typedef_All_transfer} ),
+ ("Ex_transfer", @{thm typedef_Ex_transfer} )]
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((qualify "forall_transfer", [transfer_attr]),
+ [simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer})])
+ |> fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[typedef_thm, T_def] MRSL thm])) thms
+ end
+ val thms =
+ [("rep_transfer", @{thm typedef_rep_transfer}),
+ ("bi_unique", @{thm typedef_bi_unique} ),
+ ("right_unique", @{thm typedef_right_unique}),
+ ("right_total", @{thm typedef_right_total} )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [[typedef_thm, T_def] MRSL thm])) thms lthy
+ end
+
+ fun setup_transfer_rules_par lthy =
+ let
+ val pcrel_def = #pcrel_def (the (get_pcrel_info lthy qty_full_name))
+ val lthy =
+ case opt_reflp_thm of
+ SOME reflp_thm =>
+ let
+ val id_abs_transfer = generate_parametric_id lthy rty
+ (Lifting_Term.parametrize_transfer_rule lthy
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer}))
+ val bi_total = parametrize_class_constraint lthy pcrel_def
+ ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total})
+ val thms =
+ [("id_abs_transfer",id_abs_transfer),
+ ("bi_total", bi_total )]
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+ | NONE =>
+ let
+ val thms =
+ ("forall_transfer", simplify ([typedef_thm, T_def] MRSL @{thm typedef_forall_transfer}))
+ ::
+ (map_snd (fn thm => [typedef_thm, T_def] MRSL thm)
+ [("All_transfer", @{thm typedef_All_transfer}),
+ ("Ex_transfer", @{thm typedef_Ex_transfer} )])
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [parametrize_quantifier lthy thm])) thms lthy
+ end
+ val thms =
+ ("rep_transfer", generate_parametric_id lthy rty
+ (Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL @{thm typedef_rep_transfer})))
+ ::
+ (map_snd (fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm))
+ [("bi_unique", @{thm typedef_bi_unique} ),
+ ("right_unique", @{thm typedef_right_unique}),
+ ("right_total", @{thm typedef_right_total} )])
+ in
+ fold (fn (name, thm) => (snd oo Local_Theory.note) ((qualify name, [transfer_attr]),
+ [thm])) thms lthy
+ end
+
+ fun setup_transfer_rules lthy =
+ if is_some (get_pcrel_info lthy qty_full_name) then setup_transfer_rules_par lthy
+ else setup_transfer_rules_nonpar lthy
+
in
- lthy''
+ lthy
|> (snd oo Local_Theory.note) ((Binding.prefix_name "Quotient_" qty_name, []),
- [quot_thm])
- |> (snd oo Local_Theory.note) ((qualify "bi_unique", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_bi_unique}])
- |> (snd oo Local_Theory.note) ((qualify "rep_transfer", [transfer_attr]),
- [[typedef_thm, T_def] MRSL @{thm typedef_rep_transfer}])
- |> (snd oo Local_Theory.note) ((qualify "right_unique", [transfer_attr]),
- [[quot_thm] MRSL @{thm Quotient_right_unique}])
- |> (snd oo Local_Theory.note) ((qualify "right_total", [transfer_attr]),
- [[quot_thm] MRSL @{thm Quotient_right_total}])
- |> setup_lifting_infr gen_code quot_thm maybe_reflp_thm
+ [quot_thm])
+ |> setup_lifting_infr gen_code quot_thm opt_reflp_thm
+ |> setup_transfer_rules
end
-fun setup_lifting_cmd gen_code xthm opt_reflp_xthm lthy =
+fun setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm lthy =
let
val input_thm = singleton (Attrib.eval_thms lthy) xthm
val input_term = (HOLogic.dest_Trueprop o prop_of) input_thm
@@ -283,15 +606,14 @@
end
fun setup_quotient () =
- case opt_reflp_xthm of
- SOME reflp_xthm =>
- let
- val reflp_thm = singleton (Attrib.eval_thms lthy) reflp_xthm
- val _ = sanity_check_reflp_thm reflp_thm
- in
- setup_by_quotient gen_code input_thm (SOME reflp_thm) lthy
- end
- | NONE => setup_by_quotient gen_code input_thm NONE lthy
+ let
+ val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm
+ val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else ()
+ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
+ in
+ setup_by_quotient gen_code input_thm opt_reflp_thm opt_par_thm lthy
+ end
+
fun setup_typedef () =
case opt_reflp_xthm of
@@ -310,6 +632,8 @@
val _ =
Outer_Syntax.local_theory @{command_spec "setup_lifting"}
"setup lifting infrastructure"
- (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm >>
- (fn ((gen_code, xthm), opt_reflp_xthm) => setup_lifting_cmd gen_code xthm opt_reflp_xthm))
+ (opt_gen_code -- Parse_Spec.xthm -- Scan.option Parse_Spec.xthm
+ -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm) >>
+ (fn (((gen_code, xthm), opt_reflp_xthm), opt_par_xthm) =>
+ setup_lifting_cmd gen_code xthm opt_reflp_xthm opt_par_xthm))
end;
--- a/src/HOL/Tools/Lifting/lifting_term.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_term.ML Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
sig
exception QUOT_THM of typ * typ * Pretty.T
exception PARAM_QUOT_THM of typ * Pretty.T
+ exception MERGE_TRANSFER_REL of Pretty.T
exception CHECK_RTY of typ * typ
val prove_quot_thm: Proof.context -> typ * typ -> thm
@@ -19,6 +20,10 @@
val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context
val generate_parametrized_relator: Proof.context -> typ -> term * term list
+
+ val merge_transfer_relations: Proof.context -> cterm -> thm
+
+ val parametrize_transfer_rule: Proof.context -> thm -> thm
end
structure Lifting_Term: LIFTING_TERM =
@@ -30,6 +35,7 @@
exception QUOT_THM_INTERNAL of Pretty.T
exception QUOT_THM of typ * typ * Pretty.T
exception PARAM_QUOT_THM of typ * Pretty.T
+exception MERGE_TRANSFER_REL of Pretty.T
exception CHECK_RTY of typ * typ
fun match ctxt err ty_pat ty =
@@ -53,16 +59,41 @@
Pretty.str "don't match."])
end
+fun get_quot_data ctxt s =
+ case Lifting_Info.lookup_quotients ctxt s of
+ SOME qdata => qdata
+ | NONE => raise QUOT_THM_INTERNAL (Pretty.block
+ [Pretty.str ("No quotient type " ^ quote s),
+ Pretty.brk 1,
+ Pretty.str "found."])
+
fun get_quot_thm ctxt s =
let
val thy = Proof_Context.theory_of ctxt
in
- (case Lifting_Info.lookup_quotients ctxt s of
- SOME qdata => Thm.transfer thy (#quot_thm qdata)
- | NONE => raise QUOT_THM_INTERNAL (Pretty.block
- [Pretty.str ("No quotient type " ^ quote s),
- Pretty.brk 1,
- Pretty.str "found."]))
+ Thm.transfer thy (#quot_thm (get_quot_data ctxt s))
+ end
+
+fun get_pcrel_info ctxt s =
+ case #pcrel_info (get_quot_data ctxt s) of
+ SOME pcrel_info => pcrel_info
+ | NONE => raise QUOT_THM_INTERNAL (Pretty.block
+ [Pretty.str ("No parametrized correspondce relation for " ^ quote s),
+ Pretty.brk 1,
+ Pretty.str "found."])
+
+fun get_pcrel_def ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ Thm.transfer thy (#pcrel_def (get_pcrel_info ctxt s))
+ end
+
+fun get_pcr_cr_eq ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ Thm.transfer thy (#pcr_cr_eq (get_pcrel_info ctxt s))
end
fun get_rel_quot_thm ctxt s =
@@ -77,6 +108,22 @@
Pretty.str "found."]))
end
+fun get_rel_distr_rules ctxt s tm =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ (case Lifting_Info.lookup_relator_distr_data ctxt s of
+ SOME rel_distr_thm => (
+ case tm of
+ Const (@{const_name POS}, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm)
+ | Const (@{const_name NEG}, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm)
+ )
+ | NONE => raise QUOT_THM_INTERNAL (Pretty.block
+ [Pretty.str ("No relator distr. data for the type " ^ quote s),
+ Pretty.brk 1,
+ Pretty.str "found."]))
+ end
+
fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
fun check_raw_types (provided_rty_name, rty_of_qty_name) qty_name =
@@ -145,6 +192,17 @@
rel_quot_thm_prems
end
+fun instantiate_rtys ctxt (Type (rty_name, _)) (qty as Type (qty_name, _)) =
+ let
+ val quot_thm = get_quot_thm ctxt qty_name
+ val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
+ val _ = check_raw_types (rty_name, rs) qty_name
+ val qtyenv = match ctxt equiv_match_err qty_pat qty
+ in
+ map (Envir.subst_type qtyenv) rtys
+ end
+ | instantiate_rtys _ _ _ = error "instantiate_rtys: not Type"
+
fun prove_schematic_quot_thm ctxt (rty, qty) =
(case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
@@ -161,18 +219,15 @@
end
else
let
- val quot_thm = get_quot_thm ctxt s'
- val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm
- val _ = check_raw_types (s, rs) s'
- val qtyenv = match ctxt equiv_match_err qty_pat qty
- val rtys' = map (Envir.subst_type qtyenv) rtys
+ val rtys' = instantiate_rtys ctxt rty qty
val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys')
in
if forall is_id_quot args
then
- quot_thm
+ get_quot_thm ctxt s'
else
let
+ val quot_thm = get_quot_thm ctxt s'
val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
in
[rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
@@ -286,7 +341,7 @@
in
(args MRSL (get_rel_quot_thm ctxt s), table_ctxt)
end
- | generate (ty as (TFree _)) (table, ctxt) =
+ | generate ty (table, ctxt) =
if AList.defined (op=) table ty
then (the (AList.lookup (op=) table ty), (table, ctxt))
else
@@ -298,7 +353,6 @@
in
(Q_thm, (table', ctxt'))
end
- | generate _ _ = error "generate_param_quot_thm: TVar"
val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt)
in
@@ -317,4 +371,156 @@
(hd exported_terms, tl exported_terms)
end
+(* Parametrization *)
+
+local
+ fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o cprop_of) rule;
+
+ fun no_imp _ = raise CTERM ("no implication", []);
+
+ infix 0 else_imp
+
+ fun (cv1 else_imp cv2) ct =
+ (cv1 ct
+ handle THM _ => cv2 ct
+ | CTERM _ => cv2 ct
+ | TERM _ => cv2 ct
+ | TYPE _ => cv2 ct);
+
+ fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp
+
+ fun rewr_imp rule ct =
+ let
+ val rule1 = Thm.incr_indexes (#maxidx (Thm.rep_cterm ct) + 1) rule;
+ val lhs_rule = get_lhs rule1;
+ val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1;
+ val lhs_ct = Thm.dest_fun ct
+ in
+ Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2
+ handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct])
+ end
+
+ fun rewrs_imp rules = first_imp (map rewr_imp rules)
+
+ fun map_interrupt f l =
+ let
+ fun map_interrupt' _ [] l = SOME (rev l)
+ | map_interrupt' f (x::xs) l = (case f x of
+ NONE => NONE
+ | SOME v => map_interrupt' f xs (v::l))
+ in
+ map_interrupt' f l []
+ end
+in
+ fun merge_transfer_relations ctxt ctm =
+ let
+ val ctm = Thm.dest_arg ctm
+ val tm = term_of ctm
+ val rel = (hd o get_args 2) tm
+
+ fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2
+ | same_constants _ _ = false
+
+ fun prove_extra_assms ctxt ctm distr_rule =
+ let
+ fun prove_assm assm = try (Goal.prove ctxt [] [] (term_of assm))
+ (fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac (Transfer.get_transfer_raw ctxt))) 1)
+
+ fun is_POS_or_NEG ctm =
+ case (head_of o term_of o Thm.dest_arg) ctm of
+ Const (@{const_name POS}, _) => true
+ | Const (@{const_name NEG}, _) => true
+ | _ => false
+
+ val inst_distr_rule = rewr_imp distr_rule ctm
+ val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule)
+ val proved_assms = map_interrupt prove_assm extra_assms
+ in
+ Option.map (curry op OF inst_distr_rule) proved_assms
+ end
+ handle CTERM _ => NONE
+
+ fun cannot_merge_error_msg () = Pretty.block
+ [Pretty.str "Rewriting (merging) of this term has failed:",
+ Pretty.brk 1,
+ Syntax.pretty_term ctxt rel]
+
+ in
+ case get_args 2 rel of
+ [Const (@{const_name "HOL.eq"}, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm
+ | [_, Const (@{const_name "HOL.eq"}, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm
+ | [_, trans_rel] =>
+ let
+ val (rty', qty) = (relation_types o fastype_of) trans_rel
+ val r = (fst o dest_Type) rty'
+ val q = (fst o dest_Type) qty
+ in
+ if r = q then
+ let
+ val distr_rules = get_rel_distr_rules ctxt r (head_of tm)
+ val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules
+ in
+ case distr_rule of
+ NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
+ | SOME distr_rule => (map (merge_transfer_relations ctxt) (cprems_of distr_rule))
+ MRSL distr_rule
+ end
+ else
+ let
+ val pcrel_def = get_pcrel_def ctxt q
+ val pcrel_const = (head_of o fst o Logic.dest_equals o prop_of) pcrel_def
+ in
+ if same_constants pcrel_const (head_of trans_rel) then
+ let
+ val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
+ val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
+ val result = (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) MRSL distr_rule
+ val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
+ in
+ Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv
+ (Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result
+ end
+ else
+ raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.")
+ end
+ end
+ end
+ handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
+end
+
+fun parametrize_transfer_rule ctxt thm =
+ let
+ fun parametrize_relation_conv ctm =
+ let
+ val (rty, qty) = (relation_types o fastype_of) (term_of ctm)
+ in
+ case (rty, qty) of
+ (Type (r, rargs), Type (q, qargs)) =>
+ if r = q then
+ if forall op= (rargs ~~ qargs) then
+ Conv.all_conv ctm
+ else
+ all_args_conv parametrize_relation_conv ctm
+ else
+ if forall op= (rargs ~~ (instantiate_rtys ctxt rty qty)) then
+ let
+ val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq ctxt q)
+ in
+ Conv.rewr_conv pcr_cr_eq ctm
+ end
+ handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
+ else
+ (let
+ val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
+ in
+ (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
+ end
+ handle QUOT_THM_INTERNAL _ =>
+ (Conv.arg1_conv (all_args_conv parametrize_relation_conv)) ctm)
+ | _ => Conv.all_conv ctm
+ end
+ in
+ Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
+ end
+
end;
--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Mar 08 13:14:23 2013 +0100
@@ -8,6 +8,7 @@
sig
val MRSL: thm list * thm -> thm
val option_fold: 'b -> ('a -> 'b) -> 'a option -> 'b
+ val map_snd: ('b -> 'c) -> ('a * 'b) list -> ('a * 'c) list
val dest_Quotient: term -> term * term * term * term
val quot_thm_rel: thm -> term
@@ -15,6 +16,19 @@
val quot_thm_rep: thm -> term
val quot_thm_crel: thm -> term
val quot_thm_rty_qty: thm -> typ * typ
+
+ val undisch: thm -> thm
+ val undisch_all: thm -> thm
+ val is_fun_type: typ -> bool
+ val get_args: int -> term -> term list
+ val strip_args: int -> term -> term
+ val all_args_conv: conv -> conv
+ val is_Type: typ -> bool
+ val is_fun_rel: term -> bool
+ val relation_types: typ -> typ * typ
+ val bottom_rewr_conv: thm list -> conv
+ val mk_HOL_eq: thm -> thm
+ val safe_HOL_meta_eq: thm -> thm
end;
@@ -28,6 +42,8 @@
fun option_fold a _ NONE = a
| option_fold _ f (SOME x) = f x
+fun map_snd f xs = map (fn (a, b) => (a, f b)) xs
+
fun dest_Quotient (Const (@{const_name Quotient}, _) $ rel $ abs $ rep $ cr)
= (rel, abs, rep, cr)
| dest_Quotient t = raise TERM ("dest_Quotient", [t])
@@ -61,4 +77,40 @@
(domain_type abs_type, range_type abs_type)
end
+fun undisch thm =
+ let
+ val assm = Thm.cprem_of thm 1
+ in
+ Thm.implies_elim thm (Thm.assume assm)
+ end
+
+fun undisch_all thm = funpow (nprems_of thm) undisch thm
+
+fun is_fun_type (Type (@{type_name fun}, _)) = true
+ | is_fun_type _ = false
+
+fun get_args n = rev o fst o funpow_yield n (swap o dest_comb)
+
+fun strip_args n = funpow n (fst o dest_comb)
+
+fun all_args_conv conv ctm =
+ (Conv.combination_conv (Conv.try_conv (all_args_conv conv)) conv) ctm
+
+fun is_Type (Type _) = true
+ | is_Type _ = false
+
+fun is_fun_rel (Const (@{const_name "fun_rel"}, _) $ _ $ _) = true
+ | is_fun_rel _ = false
+
+fun relation_types typ =
+ case strip_type typ of
+ ([typ1, typ2], @{typ bool}) => (typ1, typ2)
+ | _ => error "relation_types: not a relation"
+
+fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}
+
+fun mk_HOL_eq r = r RS @{thm meta_eq_to_obj_eq}
+
+fun safe_HOL_meta_eq r = mk_HOL_eq r handle Thm.THM _ => r
+
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 08 13:14:23 2013 +0100
@@ -7,13 +7,13 @@
signature QUOTIENT_TYPE =
sig
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
+ ((binding * binding) option * bool * thm option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
val quotient_type: (string list * binding * mixfix) * (typ * term * bool) *
- ((binding * binding) option * bool) -> Proof.context -> Proof.state
+ ((binding * binding) option * bool * thm option) -> Proof.context -> Proof.state
- val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
- (binding * binding) option -> Proof.context -> Proof.state
+ val quotient_type_cmd: ((((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
+ (binding * binding) option) * (Facts.ref * Args.src list) option -> Proof.context -> Proof.state
end;
structure Quotient_Type: QUOTIENT_TYPE =
@@ -110,7 +110,7 @@
(def_thm, lthy'')
end;
-fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
+fun setup_lifting_package gen_code quot3_thm equiv_thm opt_par_thm lthy =
let
val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
@@ -128,11 +128,11 @@
)
in
lthy'
- |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
+ |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm opt_par_thm
|> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
end
-fun init_quotient_infr gen_code quot_thm equiv_thm lthy =
+fun init_quotient_infr gen_code quot_thm equiv_thm opt_par_thm lthy =
let
val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
val (qtyp, rtyp) = (dest_funT o fastype_of) rep
@@ -147,11 +147,11 @@
|> Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
#> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
- |> setup_lifting_package gen_code quot_thm equiv_thm
+ |> setup_lifting_package gen_code quot_thm equiv_thm opt_par_thm
end
(* main function for constructing a quotient type *)
-fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
+fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), equiv_thm) lthy =
let
val part_equiv =
if partial
@@ -203,7 +203,7 @@
quot_thm = quotient_thm}
val lthy4 = lthy3
- |> init_quotient_infr gen_code quotient_thm equiv_thm
+ |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
|> (snd oo Local_Theory.note)
((equiv_thm_name,
if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -314,7 +314,7 @@
fun quotient_type_cmd spec lthy =
let
- fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
+ fun parse_spec (((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs), opt_par_xthm) lthy =
let
val rty = Syntax.read_typ lthy rty_str
val tmp_lthy1 = Variable.declare_typ rty lthy
@@ -323,8 +323,9 @@
|> Type.constraint (rty --> rty --> @{typ bool})
|> Syntax.check_term tmp_lthy1
val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
+ val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm
in
- (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
+ (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code, opt_par_thm)), tmp_lthy2)
end
val (spec', _) = parse_spec spec lthy
@@ -343,6 +344,7 @@
Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
(@{keyword "/"} |-- (partial -- Parse.term)) --
Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+ -- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse_Spec.xthm)
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
--- a/src/HOL/Tools/transfer.ML Fri Mar 08 11:28:20 2013 +0100
+++ b/src/HOL/Tools/transfer.ML Fri Mar 08 13:14:23 2013 +0100
@@ -9,6 +9,7 @@
val prep_conv: conv
val get_relator_eq: Proof.context -> thm list
val get_sym_relator_eq: Proof.context -> thm list
+ val get_transfer_raw: Proof.context -> thm list
val transfer_add: attribute
val transfer_del: attribute
val transfer_rule_of_term: Proof.context -> term -> thm