author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 69349 | 7cef9e386ffe |
child 70320 | 59258a3192bf |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Tools/Lifting/lifting_setup.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
47352 | 4 |
Setting up the lifting infrastructure. |
47308 | 5 |
*) |
6 |
||
7 |
signature LIFTING_SETUP = |
|
8 |
sig |
|
9 |
exception SETUP_LIFTING_INFR of string |
|
10 |
||
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
11 |
type config = { notes: bool }; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
12 |
val default_config: config; |
47308 | 13 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
14 |
val setup_by_quotient: config -> thm -> thm option -> thm option -> local_theory -> |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
15 |
binding * local_theory |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
16 |
|
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
17 |
val setup_by_typedef_thm: config -> thm -> local_theory -> binding * local_theory |
53651 | 18 |
|
19 |
val lifting_restore: Lifting_Info.quotient -> Context.generic -> Context.generic |
|
60226
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
20 |
|
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
21 |
val lifting_forget: string -> local_theory -> local_theory |
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
22 |
val update_transfer_rules: string -> local_theory -> local_theory |
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
23 |
val pointer_of_bundle_binding: Proof.context -> binding -> string |
53651 | 24 |
end |
47308 | 25 |
|
47334 | 26 |
structure Lifting_Setup: LIFTING_SETUP = |
47308 | 27 |
struct |
28 |
||
47698 | 29 |
open Lifting_Util |
47308 | 30 |
|
47698 | 31 |
infix 0 MRSL |
47308 | 32 |
|
33 |
exception SETUP_LIFTING_INFR of string |
|
34 |
||
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
35 |
(* Config *) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
36 |
|
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
37 |
type config = { notes: bool }; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
38 |
val default_config = { notes = true }; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
39 |
|
60239 | 40 |
fun define_crel (config: config) rep_fun lthy = |
47308 | 41 |
let |
47361
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
42 |
val (qty, rty) = (dest_funT o fastype_of) rep_fun |
87c0eaf04bad
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
kuncar
parents:
47352
diff
changeset
|
43 |
val rep_fun_graph = (HOLogic.eq_const rty) $ Bound 1 $ (rep_fun $ Bound 0) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
44 |
val def_term = Abs ("x", rty, Abs ("y", qty, rep_fun_graph)) |
50175 | 45 |
val qty_name = (Binding.name o Long_Name.base_name o fst o dest_Type) qty |
50227 | 46 |
val crel_name = Binding.prefix_name "cr_" qty_name |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
47 |
val (fixed_def_term, lthy) = yield_singleton (Variable.importT_terms) def_term lthy |
63352 | 48 |
val ((_, (_ , def_thm)), lthy) = |
49 |
if #notes config then |
|
50 |
Local_Theory.define |
|
51 |
((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
52 |
else |
63352 | 53 |
Local_Theory.define |
54 |
((Binding.concealed crel_name, NoSyn), (Binding.empty_atts, fixed_def_term)) lthy |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
55 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
56 |
(def_thm, lthy) |
47308 | 57 |
end |
58 |
||
50227 | 59 |
fun print_define_pcrel_warning msg = |
60 |
let |
|
61 |
val warning_msg = cat_lines |
|
62 |
["Generation of a parametrized correspondence relation failed.", |
|
63 |
(Pretty.string_of (Pretty.block |
|
64 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))] |
|
65 |
in |
|
66 |
warning warning_msg |
|
67 |
end |
|
68 |
||
60239 | 69 |
fun define_pcrel (config: config) crel lthy = |
50227 | 70 |
let |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
71 |
val (fixed_crel, lthy) = yield_singleton Variable.importT_terms crel lthy |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
72 |
val [rty', qty] = (binder_types o fastype_of) fixed_crel |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
73 |
val (param_rel, args) = Lifting_Term.generate_parametrized_relator lthy rty' |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
74 |
val rty_raw = (domain_type o range_type o fastype_of) param_rel |
50227 | 75 |
val thy = Proof_Context.theory_of lthy |
76 |
val tyenv_match = Sign.typ_match thy (rty_raw, rty') Vartab.empty |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
77 |
val param_rel_subst = Envir.subst_term (tyenv_match,Vartab.empty) param_rel |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
78 |
val args_subst = map (Envir.subst_term (tyenv_match,Vartab.empty)) args |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
79 |
val lthy = Variable.declare_names fixed_crel lthy |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
80 |
val (instT, lthy) = Variable.importT_inst (param_rel_subst :: args_subst) lthy |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
81 |
val args_fixed = (map (Term_Subst.instantiate (instT, []))) args_subst |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
82 |
val param_rel_fixed = Term_Subst.instantiate (instT, []) param_rel_subst |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
83 |
val rty = (domain_type o fastype_of) param_rel_fixed |
69593 | 84 |
val relcomp_op = Const (\<^const_name>\<open>relcompp\<close>, |
50227 | 85 |
(rty --> rty' --> HOLogic.boolT) --> |
86 |
(rty' --> qty --> HOLogic.boolT) --> |
|
87 |
rty --> qty --> HOLogic.boolT) |
|
88 |
val qty_name = (fst o dest_Type) qty |
|
89 |
val pcrel_name = Binding.prefix_name "pcr_" ((Binding.name o Long_Name.base_name) qty_name) |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
90 |
val relator_type = foldr1 (op -->) ((map type_of args_fixed) @ [rty, qty, HOLogic.boolT]) |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
91 |
val lhs = Library.foldl (op $) ((Free (Binding.name_of pcrel_name, relator_type)), args_fixed) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
92 |
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel |
50227 | 93 |
val definition_term = Logic.mk_equals (lhs, rhs) |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
94 |
fun note_def lthy = |
63180 | 95 |
Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] [] |
63352 | 96 |
(Binding.empty_atts, definition_term) lthy |>> (snd #> snd); |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
97 |
fun raw_def lthy = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
98 |
let |
63395 | 99 |
val ((_, rhs), prove) = |
100 |
Local_Defs.derived_def lthy (K []) {conditional = true} definition_term; |
|
63352 | 101 |
val ((_, (_, raw_th)), lthy) = |
102 |
Local_Theory.define |
|
103 |
((Binding.concealed pcrel_name, NoSyn), (Binding.empty_atts, rhs)) lthy; |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
104 |
val th = prove lthy raw_th; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
105 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
106 |
(th, lthy) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
107 |
end |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
108 |
val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy |
50227 | 109 |
in |
110 |
(SOME def_thm, lthy) |
|
111 |
end |
|
112 |
handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy)) |
|
113 |
||
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
114 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
115 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
116 |
val eq_OO_meta = mk_meta_eq @{thm eq_OO} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
117 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
118 |
fun print_generate_pcr_cr_eq_error ctxt term = |
56257 | 119 |
let |
69593 | 120 |
val goal = Const (\<^const_name>\<open>HOL.eq\<close>, dummyT) $ term $ Const (\<^const_name>\<open>HOL.eq\<close>, dummyT) |
56257 | 121 |
val error_msg = cat_lines |
122 |
["Generation of a pcr_cr_eq failed.", |
|
123 |
(Pretty.string_of (Pretty.block |
|
124 |
[Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])), |
|
125 |
"Most probably a relator_eq rule for one of the involved types is missing."] |
|
126 |
in |
|
127 |
error error_msg |
|
128 |
end |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
129 |
in |
60239 | 130 |
fun define_pcr_cr_eq (config: config) lthy pcr_rel_def = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
131 |
let |
59582 | 132 |
val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def |
60239 | 133 |
val qty_name = |
134 |
(Binding.name o Long_Name.base_name o fst o dest_Type o |
|
135 |
List.last o binder_types o fastype_of) lhs |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
136 |
val args = (snd o strip_comb) lhs |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
137 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
138 |
fun make_inst var ctxt = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
139 |
let |
60784 | 140 |
val typ = snd (relation_types (#2 (dest_Var var))) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
141 |
val sort = Type.sort_of_atyp typ |
59630 | 142 |
val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt |
60784 | 143 |
val inst = (#1 (dest_Var var), Thm.cterm_of ctxt' (HOLogic.eq_const (TFree fresh_var))) |
144 |
in (inst, ctxt') end |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
145 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
146 |
val orig_lthy = lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
147 |
val (args_inst, lthy) = fold_map make_inst args lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
148 |
val pcr_cr_eq = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
149 |
pcr_rel_def |
60784 | 150 |
|> infer_instantiate lthy args_inst |
52883
0a7c97c76f46
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents:
51994
diff
changeset
|
151 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv |
0a7c97c76f46
expand equalities in the transfer relation in transfer_prover if the relation doesn't follow the functional structure
kuncar
parents:
51994
diff
changeset
|
152 |
(Transfer.bottom_rewr_conv (Transfer.get_relator_eq lthy)))) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
153 |
in |
59582 | 154 |
case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of |
69593 | 155 |
Const (\<^const_name>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ => |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
156 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
157 |
val thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
158 |
pcr_cr_eq |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
159 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta)) |
67710
cc2db3239932
added HOLogic.mk_obj_eq convenience and eliminated some clones;
wenzelm
parents:
66251
diff
changeset
|
160 |
|> HOLogic.mk_obj_eq |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
161 |
|> singleton (Variable.export lthy orig_lthy) |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
162 |
val lthy = (#notes config ? (Local_Theory.note |
63003 | 163 |
((Binding.qualify_name true qty_name "pcr_cr_eq", []), [thm]) #> snd)) lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
164 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
165 |
(thm, lthy) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
166 |
end |
69593 | 167 |
| Const (\<^const_name>\<open>relcompp\<close>, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
168 |
| _ => error "generate_pcr_cr_eq: implementation error" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
169 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
170 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
171 |
|
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
172 |
fun define_code_constr quot_thm lthy = |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
173 |
let |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47943
diff
changeset
|
174 |
val abs = quot_thm_abs quot_thm |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
175 |
in |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
176 |
if is_Const abs then |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
177 |
let |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
178 |
val (fixed_abs, lthy') = yield_singleton Variable.importT_terms abs lthy |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
179 |
in |
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
63395
diff
changeset
|
180 |
Local_Theory.background_theory |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
63395
diff
changeset
|
181 |
(Code.declare_datatype_global [dest_Const fixed_abs]) lthy' |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
182 |
end |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
183 |
else |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
184 |
lthy |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
185 |
end |
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
186 |
|
66251
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
63395
diff
changeset
|
187 |
fun define_abs_type quot_thm = |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
63395
diff
changeset
|
188 |
Lifting_Def.can_generate_code_cert quot_thm ? |
cd935b7cb3fb
proper concept of code declaration wrt. atomicity and Isar declarations
haftmann
parents:
63395
diff
changeset
|
189 |
Code.declare_abstype (quot_thm RS @{thm Quotient_abs_rep}); |
47308 | 190 |
|
53651 | 191 |
local |
192 |
exception QUOT_ERROR of Pretty.T list |
|
193 |
in |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
194 |
fun quot_thm_sanity_check ctxt quot_thm = |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
195 |
let |
53651 | 196 |
val _ = |
59582 | 197 |
if (Thm.nprems_of quot_thm > 0) then |
53651 | 198 |
raise QUOT_ERROR [Pretty.block |
199 |
[Pretty.str "The Quotient theorem has extra assumptions:", |
|
200 |
Pretty.brk 1, |
|
61268 | 201 |
Thm.pretty_thm ctxt quot_thm]] |
53651 | 202 |
else () |
59582 | 203 |
val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient |
53651 | 204 |
handle TERM _ => raise QUOT_ERROR |
205 |
[Pretty.block |
|
206 |
[Pretty.str "The Quotient theorem is not of the right form:", |
|
207 |
Pretty.brk 1, |
|
61268 | 208 |
Thm.pretty_thm ctxt quot_thm]] |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
209 |
val ((_, [quot_thm_fixed]), ctxt') = Variable.importT [quot_thm] ctxt |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47943
diff
changeset
|
210 |
val (rty, qty) = quot_thm_rty_qty quot_thm_fixed |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
211 |
val rty_tfreesT = Term.add_tfree_namesT rty [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
212 |
val qty_tfreesT = Term.add_tfree_namesT qty [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
213 |
val extra_rty_tfrees = |
47545 | 214 |
case subtract (op =) qty_tfreesT rty_tfreesT of |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
215 |
[] => [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
216 |
| extras => [Pretty.block ([Pretty.str "Extra variables in the raw type:", |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
217 |
Pretty.brk 1] @ |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
218 |
((Pretty.commas o map (Pretty.str o quote)) extras) @ |
47545 | 219 |
[Pretty.str "."])] |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
220 |
val not_type_constr = |
47545 | 221 |
case qty of |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
222 |
Type _ => [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
223 |
| _ => [Pretty.block [Pretty.str "The quotient type ", |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
224 |
Pretty.quote (Syntax.pretty_typ ctxt' qty), |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
225 |
Pretty.brk 1, |
47545 | 226 |
Pretty.str "is not a type constructor."]] |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
227 |
val errs = extra_rty_tfrees @ not_type_constr |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
228 |
in |
53651 | 229 |
if null errs then () else raise QUOT_ERROR errs |
230 |
end |
|
231 |
handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] |
|
232 |
@ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
233 |
end |
|
234 |
||
235 |
fun lifting_bundle qty_full_name qinfo lthy = |
|
236 |
let |
|
63003 | 237 |
val binding = |
238 |
Binding.qualify_name true (qty_full_name |> Long_Name.base_name |> Binding.name) "lifting" |
|
53651 | 239 |
val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding |
240 |
val bundle_name = Name_Space.full_name (Name_Space.naming_of |
|
241 |
(Context.Theory (Proof_Context.theory_of lthy))) morphed_binding |
|
242 |
fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo |
|
243 |
||
244 |
val thy = Proof_Context.theory_of lthy |
|
245 |
val dummy_thm = Thm.transfer thy Drule.dummy_thm |
|
246 |
val restore_lifting_att = |
|
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
247 |
([dummy_thm], |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
248 |
[map (Token.make_string o rpair Position.none) |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
249 |
["Lifting.lifting_restore_internal", bundle_name]]) |
53651 | 250 |
in |
251 |
lthy |
|
252 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
|
253 |
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) |
|
254 |
|> Bundle.bundle ((binding, [restore_lifting_att])) [] |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
255 |
|> pair binding |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
256 |
end |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
257 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
258 |
fun setup_lifting_infr config quot_thm opt_reflp_thm lthy = |
47308 | 259 |
let |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
260 |
val _ = quot_thm_sanity_check lthy quot_thm |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
261 |
val (_, qty) = quot_thm_rty_qty quot_thm |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
262 |
val (pcrel_def, lthy) = define_pcrel config (quot_thm_crel quot_thm) lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
263 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
264 |
val pcrel_def = Option.map (Morphism.thm (Local_Theory.target_morphism lthy)) pcrel_def |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
265 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
266 |
val (pcr_cr_eq, lthy) = case pcrel_def of |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
267 |
SOME pcrel_def => apfst SOME (define_pcr_cr_eq config lthy pcrel_def) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
268 |
| NONE => (NONE, lthy) |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
269 |
val pcr_info = case pcrel_def of |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
270 |
SOME pcrel_def => SOME { pcrel_def = pcrel_def, pcr_cr_eq = the pcr_cr_eq } |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
271 |
| NONE => NONE |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
272 |
val quotients = { quot_thm = quot_thm, pcr_info = pcr_info } |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
273 |
val qty_full_name = (fst o dest_Type) qty |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
274 |
fun quot_info phi = Lifting_Info.transform_quotient phi quotients |
51994 | 275 |
val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
276 |
val lthy = case opt_reflp_thm of |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
277 |
SOME reflp_thm => lthy |
51994 | 278 |
|> (snd oo Local_Theory.note) ((Binding.empty, [reflexivity_rule_attr]), |
55563
a64d49f49ca3
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents:
55487
diff
changeset
|
279 |
[reflp_thm RS @{thm reflp_ge_eq}]) |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
280 |
|> define_code_constr quot_thm |
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
281 |
| NONE => lthy |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
282 |
|> define_abs_type quot_thm |
47308 | 283 |
in |
50227 | 284 |
lthy |
47308 | 285 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
286 |
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
|
53651 | 287 |
|> lifting_bundle qty_full_name quotients |
47308 | 288 |
end |
289 |
||
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
290 |
local |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
291 |
fun importT_inst_exclude exclude ts ctxt = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
292 |
let |
53651 | 293 |
val tvars = rev (subtract op= exclude (fold Term.add_tvars ts [])) |
294 |
val (tfrees, ctxt') = Variable.invent_types (map #2 tvars) ctxt |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
295 |
in (tvars ~~ map TFree tfrees, ctxt') end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
296 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
297 |
fun import_inst_exclude exclude ts ctxt = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
298 |
let |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
299 |
val excludeT = fold (Term.add_tvarsT o snd) exclude [] |
53651 | 300 |
val (instT, ctxt') = importT_inst_exclude excludeT ts ctxt |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
301 |
val vars = map (apsnd (Term_Subst.instantiateT instT)) |
53651 | 302 |
(rev (subtract op= exclude (fold Term.add_vars ts []))) |
303 |
val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt' |
|
304 |
val inst = vars ~~ map Free (xs ~~ map #2 vars) |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
305 |
in ((instT, inst), ctxt'') end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
306 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
307 |
fun import_terms_exclude exclude ts ctxt = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
308 |
let val (inst, ctxt') = import_inst_exclude exclude ts ctxt |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
309 |
in (map (Term_Subst.instantiate inst) ts, ctxt') end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
310 |
in |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
311 |
fun reduce_goal not_fix goal tac ctxt = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
312 |
let |
59630 | 313 |
val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt |
314 |
val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal) |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
315 |
in |
59630 | 316 |
(singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE tac init_goal)) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
317 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
318 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
319 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
320 |
local |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
321 |
val OO_rules = @{thms left_total_OO left_unique_OO right_total_OO right_unique_OO bi_total_OO |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
322 |
bi_unique_OO} |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
323 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
324 |
fun parametrize_class_constraint ctxt pcr_def constraint = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
325 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
326 |
fun generate_transfer_rule pcr_def constraint goal ctxt = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
327 |
let |
59630 | 328 |
val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt |
329 |
val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal) |
|
330 |
val rules = Transfer.get_transfer_raw ctxt' |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
331 |
val rules = constraint :: OO_rules @ rules |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
332 |
val tac = |
63170 | 333 |
K (Local_Defs.unfold0_tac ctxt' [pcr_def]) THEN' REPEAT_ALL_NEW (resolve_tac ctxt' rules) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
334 |
in |
59630 | 335 |
(singleton (Variable.export ctxt' ctxt) o Goal.conclude) (the (SINGLE (tac 1) init_goal)) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
336 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
337 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
338 |
fun make_goal pcr_def constr = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
339 |
let |
59582 | 340 |
val pred_name = |
341 |
(fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr |
|
342 |
val arg = (fst o Logic.dest_equals o Thm.prop_of) pcr_def |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
343 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
344 |
HOLogic.mk_Trueprop ((Const (pred_name, (fastype_of arg) --> HOLogic.boolT)) $ arg) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
345 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
346 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
347 |
val check_assms = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
348 |
let |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
349 |
val right_names = ["right_total", "right_unique", "left_total", "left_unique", "bi_total", |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
350 |
"bi_unique"] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
351 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
352 |
fun is_right_name name = member op= right_names (Long_Name.base_name name) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
353 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
354 |
fun is_trivial_assm (Const (name, _) $ Var (_, _)) = is_right_name name |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
355 |
| is_trivial_assm (Const (name, _) $ Free (_, _)) = is_right_name name |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
356 |
| is_trivial_assm _ = false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
357 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
358 |
fn thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
359 |
let |
59582 | 360 |
val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm) |
361 |
val thm_name = |
|
362 |
(Long_Name.base_name o fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
363 |
val non_trivial_assms = filter_out is_trivial_assm prems |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
364 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
365 |
if null non_trivial_assms then () |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
366 |
else |
61876 | 367 |
Pretty.block ([Pretty.str "Non-trivial assumptions in ", |
368 |
Pretty.str thm_name, |
|
369 |
Pretty.str " transfer rule found:", |
|
370 |
Pretty.brk 1] @ |
|
371 |
Pretty.commas (map (Syntax.pretty_term ctxt) non_trivial_assms)) |
|
372 |
|> Pretty.string_of |
|
373 |
|> warning |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
374 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
375 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
376 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
377 |
val goal = make_goal pcr_def constraint |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
378 |
val thm = generate_transfer_rule pcr_def constraint goal ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
379 |
val _ = check_assms thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
380 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
381 |
thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
382 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
383 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
384 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
385 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
386 |
val id_unfold = (Conv.rewr_conv (mk_meta_eq @{thm id_def})) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
387 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
388 |
fun generate_parametric_id lthy rty id_transfer_rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
389 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
390 |
(* it doesn't raise an exception because it would have already raised it in define_pcrel *) |
59630 | 391 |
val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty |
392 |
val parametrized_relator = |
|
393 |
singleton (Variable.export_terms ctxt' lthy) (quot_thm_crel quot_thm) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
394 |
val id_transfer = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
395 |
@{thm id_transfer} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
396 |
|> Thm.incr_indexes (Term.maxidx_of_term parametrized_relator + 1) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
397 |
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold)) |
60784 | 398 |
val var = hd (Term.add_vars (Thm.prop_of id_transfer) []) |
399 |
val inst = [(#1 var, Thm.cterm_of lthy parametrized_relator)] |
|
400 |
val id_par_thm = infer_instantiate lthy inst id_transfer |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
401 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
402 |
Lifting_Def.generate_parametric_transfer_rule lthy id_transfer_rule id_par_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
403 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
404 |
handle Lifting_Term.MERGE_TRANSFER_REL msg => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
405 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
406 |
val error_msg = cat_lines |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
407 |
["Generation of a parametric transfer rule for the abs. or the rep. function failed.", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
408 |
"A non-parametric version will be used.", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
409 |
(Pretty.string_of (Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
410 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
411 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
412 |
(warning error_msg; id_transfer_rule) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
413 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
414 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
415 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
416 |
local |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
417 |
fun rewrite_first_Domainp_arg rewr_thm thm = Conv.fconv_rule (Conv.concl_conv ~1 (HOLogic.Trueprop_conv |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
418 |
(Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv rewr_thm))))) thm |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
419 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
420 |
fun fold_Domainp_pcrel pcrel_def thm = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
421 |
let |
59582 | 422 |
val ct = |
423 |
thm |> Thm.cprop_of |> Drule.strip_imp_concl |
|
424 |
|> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg |
|
59586 | 425 |
val pcrel_def = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) pcrel_def |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
426 |
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm |
53651 | 427 |
handle Pattern.MATCH => raise CTERM ("fold_Domainp_pcrel", [ct, Thm.rhs_of pcrel_def]) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
428 |
in |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
429 |
rewrite_first_Domainp_arg (Thm.symmetric pcrel_def) thm |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
430 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
431 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
432 |
fun reduce_Domainp ctxt rules thm = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
433 |
let |
59582 | 434 |
val goal = thm |> Thm.prems_of |> hd |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
435 |
val var = goal |> HOLogic.dest_Trueprop |> dest_comb |> snd |> dest_Var |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
436 |
val reduced_assm = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
437 |
reduce_goal [var] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
438 |
in |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
439 |
reduced_assm RS thm |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
440 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
441 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
442 |
fun parametrize_domain dom_thm (pcr_info : Lifting_Info.pcr) ctxt = |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
443 |
let |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
444 |
fun reduce_first_assm ctxt rules thm = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
445 |
let |
59582 | 446 |
val goal = thm |> Thm.prems_of |> hd |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
447 |
val reduced_assm = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
448 |
reduce_goal [] goal (TRY (REPEAT_ALL_NEW (resolve_tac ctxt rules) 1)) ctxt |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
449 |
in |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
450 |
reduced_assm RS thm |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
451 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
452 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
453 |
val pcr_cr_met_eq = #pcr_cr_eq pcr_info RS @{thm eq_reflection} |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
454 |
val pcr_Domainp_eq = rewrite_first_Domainp_arg (Thm.symmetric pcr_cr_met_eq) dom_thm |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
455 |
val pcrel_def = #pcrel_def pcr_info |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
456 |
val pcr_Domainp_par_left_total = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
457 |
(dom_thm RS @{thm pcr_Domainp_par_left_total}) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
458 |
|> fold_Domainp_pcrel pcrel_def |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
459 |
|> reduce_first_assm ctxt (Lifting_Info.get_reflexivity_rules ctxt) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
460 |
val pcr_Domainp_par = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
461 |
(dom_thm RS @{thm pcr_Domainp_par}) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
462 |
|> fold_Domainp_pcrel pcrel_def |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
463 |
|> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
464 |
val pcr_Domainp = |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
465 |
(dom_thm RS @{thm pcr_Domainp}) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
466 |
|> fold_Domainp_pcrel pcrel_def |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
467 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
468 |
[("domain", [pcr_Domainp], @{attributes [transfer_domain_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
469 |
("domain_par", [pcr_Domainp_par], @{attributes [transfer_domain_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
470 |
("domain_par_left_total", [pcr_Domainp_par_left_total], @{attributes [transfer_domain_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
471 |
("domain_eq", [pcr_Domainp_eq], @{attributes [transfer_domain_rule]})] |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
472 |
in |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
473 |
thms |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
474 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
475 |
|
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
476 |
fun parametrize_total_domain left_total pcrel_def ctxt = |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
477 |
let |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
478 |
val thm = |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
479 |
(left_total RS @{thm pcr_Domainp_total}) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
480 |
|> fold_Domainp_pcrel pcrel_def |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
481 |
|> reduce_Domainp ctxt (Transfer.get_relator_domain ctxt) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
482 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
483 |
[("domain", [thm], @{attributes [transfer_domain_rule]})] |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
484 |
end |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
485 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
486 |
end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
487 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
488 |
fun get_pcrel_info ctxt qty_full_name = |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
489 |
#pcr_info (the (Lifting_Info.lookup_quotients ctxt qty_full_name)) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
490 |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
491 |
fun get_Domainp_thm quot_thm = |
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
492 |
the (get_first (try(curry op RS quot_thm)) [@{thm eq_onp_to_Domainp}, @{thm Quotient_to_Domainp}]) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
493 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
494 |
fun notes names thms = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
495 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
496 |
val notes = |
63352 | 497 |
if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms |
498 |
else map_filter (fn (_, thms, attrs) => if null attrs then NONE |
|
499 |
else SOME (Binding.empty_atts, [(thms, attrs)])) thms |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
500 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
501 |
Local_Theory.notes notes #> snd |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
502 |
end |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
503 |
|
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
504 |
fun map_thms map_name map_thm thms = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
505 |
map (fn (name, thms, attr) => (map_name name, map map_thm thms, attr)) thms |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
506 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
507 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
508 |
Sets up the Lifting package by a quotient theorem. |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
509 |
|
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
510 |
quot_thm - a quotient theorem (Quotient R Abs Rep T) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
511 |
opt_reflp_thm - a theorem saying that a relation from quot_thm is reflexive |
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
512 |
(in the form "reflp R") |
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
513 |
opt_par_thm - a parametricity theorem for R |
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
514 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
515 |
|
60239 | 516 |
fun setup_by_quotient (config: config) quot_thm opt_reflp_thm opt_par_thm lthy = |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
517 |
let |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
518 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
519 |
val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy) quot_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
520 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
521 |
val (rty, qty) = quot_thm_rty_qty quot_thm |
47575 | 522 |
val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty)))) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
523 |
val qty_full_name = (fst o dest_Type) qty |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
524 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name |
63003 | 525 |
val qualify = Binding.qualify_name true qty_name |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
526 |
val notes1 = case opt_reflp_thm of |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
527 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
528 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
529 |
val thms = |
63003 | 530 |
[("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), |
531 |
("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [])] |
|
532 |
in map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms end |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
533 |
| NONE => |
63003 | 534 |
let val thms = [("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] |
535 |
in map_thms qualify (fn thm => quot_thm RS thm) thms end |
|
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
536 |
val dom_thm = get_Domainp_thm quot_thm |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
537 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
538 |
fun setup_transfer_rules_nonpar notes = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
539 |
let |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
540 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
541 |
case opt_reflp_thm of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
542 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
543 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
544 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
545 |
[("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
546 |
("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
547 |
("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
548 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
549 |
map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
550 |
end |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
551 |
| NONE => map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
552 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
553 |
val notes2 = map_thms qualify (fn thm => quot_thm RS thm) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
554 |
[("rel_eq_transfer", @{thms Quotient_rel_eq_transfer}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
555 |
("right_unique", @{thms Quotient_right_unique}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
556 |
("right_total", @{thms Quotient_right_total}, @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
557 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
558 |
notes2 @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
559 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
560 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
561 |
fun generate_parametric_rel_eq lthy transfer_rule opt_param_thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
562 |
option_fold transfer_rule (Lifting_Def.generate_parametric_transfer_rule lthy transfer_rule) opt_param_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
563 |
handle Lifting_Term.MERGE_TRANSFER_REL msg => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
564 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
565 |
val error_msg = cat_lines |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
566 |
["Generation of a parametric transfer rule for the quotient relation failed.", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
567 |
(Pretty.string_of (Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
568 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
569 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
570 |
error error_msg |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
571 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
572 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
573 |
fun setup_transfer_rules_par lthy notes = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
574 |
let |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
575 |
val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
576 |
val pcrel_def = #pcrel_def pcrel_info |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
577 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
578 |
case opt_reflp_thm of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
579 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
580 |
let |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
581 |
val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
582 |
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
583 |
val domain_thms = parametrize_total_domain left_total pcrel_def lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
584 |
val id_abs_transfer = generate_parametric_id lthy rty |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
585 |
(Lifting_Term.parametrize_transfer_rule lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
586 |
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
587 |
val left_total = parametrize_class_constraint lthy pcrel_def left_total |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
588 |
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
589 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
590 |
[("id_abs_transfer", [id_abs_transfer], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
591 |
("left_total", [left_total], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
592 |
("bi_total", [bi_total], @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
593 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
594 |
map_thms qualify I thms @ map_thms qualify I domain_thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
595 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
596 |
| NONE => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
597 |
let |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
598 |
val thms = parametrize_domain dom_thm pcrel_info lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
599 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
600 |
map_thms qualify I thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
601 |
end |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
602 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
603 |
val rel_eq_transfer = generate_parametric_rel_eq lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
604 |
(Lifting_Term.parametrize_transfer_rule lthy (quot_thm RS @{thm Quotient_rel_eq_transfer})) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
605 |
opt_par_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
606 |
val right_unique = parametrize_class_constraint lthy pcrel_def |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
607 |
(quot_thm RS @{thm Quotient_right_unique}) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
608 |
val right_total = parametrize_class_constraint lthy pcrel_def |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
609 |
(quot_thm RS @{thm Quotient_right_total}) |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
610 |
val notes2 = map_thms qualify I |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
611 |
[("rel_eq_transfer", [rel_eq_transfer], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
612 |
("right_unique", [right_unique], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
613 |
("right_total", [right_total], @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
614 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
615 |
notes2 @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
616 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
617 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
618 |
fun setup_rules lthy = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
619 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
620 |
val thms = if is_some (get_pcrel_info lthy qty_full_name) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
621 |
then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
622 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
623 |
notes (#notes config) thms lthy |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
624 |
end |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
625 |
in |
50227 | 626 |
lthy |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
627 |
|> setup_lifting_infr config quot_thm opt_reflp_thm |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
628 |
||> setup_rules |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
629 |
end |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
630 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
631 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
632 |
Sets up the Lifting package by a typedef theorem. |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
633 |
|
47937
70375fa2679d
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
kuncar
parents:
47936
diff
changeset
|
634 |
gen_code - flag if an abstract type given by typedef_thm should be registred |
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
635 |
as an abstract type in the code generator |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
636 |
typedef_thm - a typedef theorem (type_definition Rep Abs S) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
637 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
638 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
639 |
fun setup_by_typedef_thm config typedef_thm lthy = |
47308 | 640 |
let |
59582 | 641 |
val (_ $ rep_fun $ _ $ typedef_set) = (HOLogic.dest_Trueprop o Thm.prop_of) typedef_thm |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
642 |
val (T_def, lthy) = define_crel config rep_fun lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
643 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
644 |
val T_def = Morphism.thm (Local_Theory.target_morphism lthy) T_def |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
645 |
(**) |
47545 | 646 |
val quot_thm = case typedef_set of |
69593 | 647 |
Const (\<^const_name>\<open>top\<close>, _) => |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
648 |
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} |
69593 | 649 |
| Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, _) => |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
650 |
[typedef_thm, T_def] MRSL @{thm open_typedef_to_Quotient} |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
651 |
| _ => |
47545 | 652 |
[typedef_thm, T_def] MRSL @{thm typedef_to_Quotient} |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
653 |
val (rty, qty) = quot_thm_rty_qty quot_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
654 |
val qty_full_name = (fst o dest_Type) qty |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
655 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name |
63003 | 656 |
val qualify = Binding.qualify_name true qty_name |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
657 |
val opt_reflp_thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
658 |
case typedef_set of |
69593 | 659 |
Const (\<^const_name>\<open>top\<close>, _) => |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
660 |
SOME ((typedef_thm RS @{thm UNIV_typedef_to_equivp}) RS @{thm equivp_reflp2}) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
661 |
| _ => NONE |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
662 |
val dom_thm = get_Domainp_thm quot_thm |
47308 | 663 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
664 |
fun setup_transfer_rules_nonpar notes = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
665 |
let |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
666 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
667 |
case opt_reflp_thm of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
668 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
669 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
670 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
671 |
[("id_abs_transfer",@{thms Quotient_id_abs_transfer}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
672 |
("left_total", @{thms Quotient_left_total}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
673 |
("bi_total", @{thms Quotient_bi_total}, @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
674 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
675 |
map_thms qualify (fn thm => [quot_thm, reflp_thm] MRSL thm) thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
676 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
677 |
| NONE => |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
678 |
map_thms qualify I [("domain", [dom_thm], @{attributes [transfer_domain_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
679 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
680 |
[("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
681 |
("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
682 |
("right_unique", @{thms typedef_right_unique}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
683 |
("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
684 |
("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]})] |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
685 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
686 |
map_thms qualify (fn thm => [typedef_thm, T_def] MRSL thm) thms @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
687 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
688 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
689 |
fun setup_transfer_rules_par lthy notes = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
690 |
let |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
691 |
val pcrel_info = (the (get_pcrel_info lthy qty_full_name)) |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
692 |
val pcrel_def = #pcrel_def pcrel_info |
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
693 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
694 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
695 |
case opt_reflp_thm of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
696 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
697 |
let |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
698 |
val left_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_left_total}) |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
699 |
val bi_total = ([quot_thm, reflp_thm] MRSL @{thm Quotient_bi_total}) |
56518
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
700 |
val domain_thms = parametrize_total_domain left_total pcrel_def lthy |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
701 |
val left_total = parametrize_class_constraint lthy pcrel_def left_total |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
702 |
val bi_total = parametrize_class_constraint lthy pcrel_def bi_total |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
703 |
val id_abs_transfer = generate_parametric_id lthy rty |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
704 |
(Lifting_Term.parametrize_transfer_rule lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
705 |
([quot_thm, reflp_thm] MRSL @{thm Quotient_id_abs_transfer})) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
706 |
val thms = |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
707 |
[("left_total", [left_total], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
708 |
("bi_total", [bi_total], @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
709 |
("id_abs_transfer",[id_abs_transfer], @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
710 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
711 |
map_thms qualify I thms @ map_thms qualify I domain_thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
712 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
713 |
| NONE => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
714 |
let |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
715 |
val thms = parametrize_domain dom_thm pcrel_info lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
716 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
717 |
map_thms qualify I thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
718 |
end |
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
719 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
720 |
val notes2 = map_thms qualify (fn thm => generate_parametric_id lthy rty |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
721 |
(Lifting_Term.parametrize_transfer_rule lthy ([typedef_thm, T_def] MRSL thm))) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
722 |
[("rep_transfer", @{thms typedef_rep_transfer}, @{attributes [transfer_rule]})]; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
723 |
val notes3 = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
724 |
map_thms qualify |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
725 |
(fn thm => parametrize_class_constraint lthy pcrel_def ([typedef_thm, T_def] MRSL thm)) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
726 |
[("left_unique", @{thms typedef_left_unique}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
727 |
("right_unique", @{thms typedef_right_unique},@{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
728 |
("bi_unique", @{thms typedef_bi_unique}, @{attributes [transfer_rule]}), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
729 |
("right_total", @{thms typedef_right_total}, @{attributes [transfer_rule]})] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
730 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
731 |
notes3 @ notes2 @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
732 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
733 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
734 |
val notes1 = [(Binding.prefix_name "Quotient_" qty_name, [quot_thm], [])] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
735 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
736 |
fun setup_rules lthy = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
737 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
738 |
val thms = if is_some (get_pcrel_info lthy qty_full_name) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
739 |
then setup_transfer_rules_par lthy notes1 else setup_transfer_rules_nonpar notes1 |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
740 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
741 |
notes (#notes config) thms lthy |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
742 |
end |
47308 | 743 |
in |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
744 |
lthy |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
745 |
|> setup_lifting_infr config quot_thm opt_reflp_thm |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
746 |
||> setup_rules |
47308 | 747 |
end |
748 |
||
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
749 |
fun setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm lthy = |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
750 |
let |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
751 |
val input_thm = singleton (Attrib.eval_thms lthy) xthm |
59582 | 752 |
val input_term = (HOLogic.dest_Trueprop o Thm.prop_of) input_thm |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
753 |
handle TERM _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
754 |
|
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
755 |
fun sanity_check_reflp_thm reflp_thm = |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
756 |
let |
59582 | 757 |
val reflp_tm = (HOLogic.dest_Trueprop o Thm.prop_of) reflp_thm |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
758 |
handle TERM _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
759 |
in |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
760 |
case reflp_tm of |
69593 | 761 |
Const (\<^const_name>\<open>reflp\<close>, _) $ _ => () |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
762 |
| _ => error "Invalid form of the reflexivity theorem. Use \"reflp R\"." |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
763 |
end |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
764 |
|
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
765 |
fun check_qty qty = if not (is_Type qty) |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
766 |
then error "The abstract type must be a type constructor." |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
767 |
else () |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
768 |
|
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
769 |
fun setup_quotient () = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
770 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
771 |
val opt_reflp_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_reflp_xthm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
772 |
val _ = if is_some opt_reflp_thm then sanity_check_reflp_thm (the opt_reflp_thm) else () |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
773 |
val opt_par_thm = Option.map (singleton (Attrib.eval_thms lthy)) opt_par_xthm |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
774 |
val _ = check_qty (snd (quot_thm_rty_qty input_thm)) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
775 |
in |
60231
0daab758e087
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
kuncar
parents:
60226
diff
changeset
|
776 |
setup_by_quotient default_config input_thm opt_reflp_thm opt_par_thm lthy |> snd |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
777 |
end |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
778 |
|
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
779 |
fun setup_typedef () = |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
780 |
let |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
781 |
val qty = (range_type o fastype_of o hd o get_args 2) input_term |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
782 |
val _ = check_qty qty |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
783 |
in |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
784 |
case opt_reflp_xthm of |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
785 |
SOME _ => error "The reflexivity theorem cannot be specified if the type_definition theorem is used." |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
786 |
| NONE => ( |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
787 |
case opt_par_xthm of |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
788 |
SOME _ => error "The parametricity theorem cannot be specified if the type_definition theorem is used." |
60231
0daab758e087
don't use the human-readable version of the rsp thm as a goal in the ML interface (there is no formal definition of its statement); make tactics more robust wrt. predicates in predicators; tuned
kuncar
parents:
60226
diff
changeset
|
789 |
| NONE => setup_by_typedef_thm default_config input_thm lthy |> snd |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
790 |
) |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
791 |
end |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
792 |
in |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
793 |
case input_term of |
69593 | 794 |
(Const (\<^const_name>\<open>Quotient\<close>, _) $ _ $ _ $ _ $ _) => setup_quotient () |
795 |
| (Const (\<^const_name>\<open>type_definition\<close>, _) $ _ $ _ $ _) => setup_typedef () |
|
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
796 |
| _ => error "Unsupported type of a theorem. Only Quotient or type_definition are supported." |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
797 |
end |
47308 | 798 |
|
799 |
val _ = |
|
69593 | 800 |
Outer_Syntax.local_theory \<^command_keyword>\<open>setup_lifting\<close> |
50214 | 801 |
"setup lifting infrastructure" |
62969 | 802 |
(Parse.thm -- Scan.option Parse.thm |
69593 | 803 |
-- Scan.option (\<^keyword>\<open>parametric\<close> |-- Parse.!!! Parse.thm) >> |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
804 |
(fn ((xthm, opt_reflp_xthm), opt_par_xthm) => |
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
805 |
setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm)) |
53651 | 806 |
|
807 |
(* restoring lifting infrastructure *) |
|
808 |
||
809 |
local |
|
810 |
exception PCR_ERROR of Pretty.T list |
|
811 |
in |
|
812 |
||
813 |
fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) = |
|
814 |
let |
|
815 |
val quot_thm = (#quot_thm qinfo) |
|
816 |
val _ = quot_thm_sanity_check ctxt quot_thm |
|
817 |
val pcr_info_err = |
|
818 |
(case #pcr_info qinfo of |
|
819 |
SOME pcr => |
|
820 |
let |
|
821 |
val pcrel_def = #pcrel_def pcr |
|
822 |
val pcr_cr_eq = #pcr_cr_eq pcr |
|
59582 | 823 |
val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def) |
53651 | 824 |
handle TERM _ => raise PCR_ERROR [Pretty.block |
825 |
[Pretty.str "The pcr definiton theorem is not a plain meta equation:", |
|
826 |
Pretty.brk 1, |
|
61268 | 827 |
Thm.pretty_thm ctxt pcrel_def]] |
53651 | 828 |
val pcr_const_def = head_of def_lhs |
59582 | 829 |
val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq)) |
53651 | 830 |
handle TERM _ => raise PCR_ERROR [Pretty.block |
831 |
[Pretty.str "The pcr_cr equation theorem is not a plain equation:", |
|
832 |
Pretty.brk 1, |
|
61268 | 833 |
Thm.pretty_thm ctxt pcr_cr_eq]] |
53651 | 834 |
val (pcr_const_eq, eqs) = strip_comb eq_lhs |
69593 | 835 |
fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true |
53651 | 836 |
| is_eq _ = false |
837 |
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2) |
|
838 |
| eq_Const _ _ = false |
|
839 |
val all_eqs = if not (forall is_eq eqs) then |
|
840 |
[Pretty.block |
|
841 |
[Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:", |
|
842 |
Pretty.brk 1, |
|
61268 | 843 |
Thm.pretty_thm ctxt pcr_cr_eq]] |
53651 | 844 |
else [] |
845 |
val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then |
|
846 |
[Pretty.block |
|
847 |
[Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:", |
|
848 |
Pretty.brk 1, |
|
849 |
Syntax.pretty_term ctxt pcr_const_def, |
|
850 |
Pretty.brk 1, |
|
851 |
Pretty.str "vs.", |
|
852 |
Pretty.brk 1, |
|
853 |
Syntax.pretty_term ctxt pcr_const_eq]] |
|
854 |
else [] |
|
855 |
val crel = quot_thm_crel quot_thm |
|
856 |
val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then |
|
857 |
[Pretty.block |
|
858 |
[Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:", |
|
859 |
Pretty.brk 1, |
|
860 |
Syntax.pretty_term ctxt crel, |
|
861 |
Pretty.brk 1, |
|
862 |
Pretty.str "vs.", |
|
863 |
Pretty.brk 1, |
|
864 |
Syntax.pretty_term ctxt eq_rhs]] |
|
865 |
else [] |
|
866 |
in |
|
867 |
all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal |
|
868 |
end |
|
869 |
| NONE => []) |
|
870 |
val errs = pcr_info_err |
|
871 |
in |
|
872 |
if null errs then () else raise PCR_ERROR errs |
|
873 |
end |
|
874 |
handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] |
|
875 |
@ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
876 |
end |
|
877 |
||
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
878 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
879 |
Registers the data in qinfo in the Lifting infrastructure. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
880 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
881 |
|
53651 | 882 |
fun lifting_restore qinfo ctxt = |
883 |
let |
|
884 |
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo |
|
885 |
val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) |
|
886 |
val qty_full_name = (fst o dest_Type) qty |
|
887 |
val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name |
|
888 |
in |
|
889 |
if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo))) |
|
890 |
then error (Pretty.string_of |
|
891 |
(Pretty.block |
|
892 |
[Pretty.str "Lifting is already setup for the type", |
|
893 |
Pretty.brk 1, |
|
894 |
Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)])) |
|
895 |
else Lifting_Info.update_quotients qty_full_name qinfo ctxt |
|
896 |
end |
|
897 |
||
898 |
val parse_opt_pcr = |
|
899 |
Scan.optional (Attrib.thm -- Attrib.thm >> |
|
900 |
(fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE |
|
901 |
||
902 |
val lifting_restore_attribute_setup = |
|
69593 | 903 |
Attrib.setup \<^binding>\<open>lifting_restore\<close> |
53651 | 904 |
((Attrib.thm -- parse_opt_pcr) >> |
905 |
(fn (quot_thm, opt_pcr) => |
|
906 |
let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr} |
|
907 |
in Thm.declaration_attribute (K (lifting_restore qinfo)) end)) |
|
908 |
"restoring lifting infrastructure" |
|
909 |
||
910 |
val _ = Theory.setup lifting_restore_attribute_setup |
|
911 |
||
912 |
fun lifting_restore_internal bundle_name ctxt = |
|
913 |
let |
|
914 |
val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name |
|
915 |
in |
|
916 |
case restore_info of |
|
917 |
SOME restore_info => |
|
918 |
ctxt |
|
919 |
|> lifting_restore (#quotient restore_info) |
|
920 |
|> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info)) |
|
921 |
| NONE => ctxt |
|
922 |
end |
|
923 |
||
924 |
val lifting_restore_internal_attribute_setup = |
|
69593 | 925 |
Attrib.setup \<^binding>\<open>lifting_restore_internal\<close> |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
926 |
(Scan.lift Parse.string >> |
59084
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
927 |
(fn name => Thm.declaration_attribute (K (lifting_restore_internal name)))) |
53651 | 928 |
"restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users" |
929 |
||
930 |
val _ = Theory.setup lifting_restore_internal_attribute_setup |
|
931 |
||
932 |
(* lifting_forget *) |
|
933 |
||
69593 | 934 |
val monotonicity_names = [\<^const_name>\<open>right_unique\<close>, \<^const_name>\<open>left_unique\<close>, \<^const_name>\<open>right_total\<close>, |
935 |
\<^const_name>\<open>left_total\<close>, \<^const_name>\<open>bi_unique\<close>, \<^const_name>\<open>bi_total\<close>] |
|
53651 | 936 |
|
69593 | 937 |
fun fold_transfer_rel f (Const (\<^const_name>\<open>Transfer.Rel\<close>, _) $ rel $ _ $ _) = f rel |
938 |
| fold_transfer_rel f (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ |
|
939 |
(Const (\<^const_name>\<open>Domainp\<close>, _) $ rel) $ _) = f rel |
|
53651 | 940 |
| fold_transfer_rel f (Const (name, _) $ rel) = |
69593 | 941 |
if member op= monotonicity_names name then f rel else f \<^term>\<open>undefined\<close> |
942 |
| fold_transfer_rel f _ = f \<^term>\<open>undefined\<close> |
|
53651 | 943 |
|
944 |
fun filter_transfer_rules_by_rel transfer_rel transfer_rules = |
|
945 |
let |
|
946 |
val transfer_rel_name = transfer_rel |> dest_Const |> fst; |
|
947 |
fun has_transfer_rel thm = |
|
948 |
let |
|
59582 | 949 |
val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |
53651 | 950 |
in |
951 |
member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name |
|
952 |
end |
|
953 |
handle TERM _ => false |
|
954 |
in |
|
955 |
filter has_transfer_rel transfer_rules |
|
956 |
end |
|
957 |
||
958 |
type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T} |
|
959 |
||
53754 | 960 |
fun get_transfer_rel (qinfo : Lifting_Info.quotient) = |
53651 | 961 |
let |
59582 | 962 |
fun get_pcrel pcr_def = pcr_def |> Thm.concl_of |> Logic.dest_equals |> fst |> head_of |
53651 | 963 |
in |
964 |
if is_some (#pcr_info qinfo) |
|
965 |
then get_pcrel (#pcrel_def (the (#pcr_info qinfo))) |
|
966 |
else quot_thm_crel (#quot_thm qinfo) |
|
967 |
end |
|
968 |
||
969 |
fun pointer_of_bundle_name bundle_name ctxt = |
|
970 |
let |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
55563
diff
changeset
|
971 |
val bundle = Bundle.get_bundle_cmd ctxt bundle_name |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
972 |
fun err () = error "The provided bundle is not a lifting bundle" |
53651 | 973 |
in |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
974 |
(case bundle of |
53651 | 975 |
[(_, [arg_src])] => |
56035
745f568837f1
proper Args.syntax for slightly odd bundle trickery;
wenzelm
parents:
56029
diff
changeset
|
976 |
let |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
977 |
val (name, _) = Token.syntax (Scan.lift Parse.string) arg_src ctxt |
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
978 |
handle ERROR _ => err () |
56035
745f568837f1
proper Args.syntax for slightly odd bundle trickery;
wenzelm
parents:
56029
diff
changeset
|
979 |
in name end |
61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61268
diff
changeset
|
980 |
| _ => err ()) |
53651 | 981 |
end |
982 |
||
60226
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
983 |
fun pointer_of_bundle_binding ctxt binding = Name_Space.full_name (Name_Space.naming_of |
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
984 |
(Context.Theory (Proof_Context.theory_of ctxt))) binding |
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
985 |
|
53651 | 986 |
fun lifting_forget pointer lthy = |
987 |
let |
|
988 |
fun get_transfer_rules_to_delete qinfo ctxt = |
|
989 |
let |
|
53754 | 990 |
val transfer_rel = get_transfer_rel qinfo |
53651 | 991 |
in |
992 |
filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt) |
|
993 |
end |
|
994 |
in |
|
995 |
case Lifting_Info.lookup_restore_data lthy pointer of |
|
996 |
SOME restore_info => |
|
997 |
let |
|
998 |
val qinfo = #quotient restore_info |
|
999 |
val quot_thm = #quot_thm qinfo |
|
1000 |
val transfer_rules = get_transfer_rules_to_delete qinfo lthy |
|
1001 |
in |
|
1002 |
Local_Theory.declaration {syntax = false, pervasive = true} |
|
1003 |
(K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm)) |
|
1004 |
lthy |
|
1005 |
end |
|
1006 |
| NONE => error "The lifting bundle refers to non-existent restore data." |
|
1007 |
end |
|
1008 |
||
1009 |
||
1010 |
fun lifting_forget_cmd bundle_name lthy = |
|
1011 |
lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy |
|
1012 |
||
1013 |
||
1014 |
val _ = |
|
69593 | 1015 |
Outer_Syntax.local_theory \<^command_keyword>\<open>lifting_forget\<close> |
53651 | 1016 |
"unsetup Lifting and Transfer for the given lifting bundle" |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
67710
diff
changeset
|
1017 |
(Parse.name_position >> lifting_forget_cmd) |
53651 | 1018 |
|
1019 |
(* lifting_update *) |
|
1020 |
||
1021 |
fun update_transfer_rules pointer lthy = |
|
1022 |
let |
|
53754 | 1023 |
fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy = |
53651 | 1024 |
let |
1025 |
val transfer_rel = get_transfer_rel qinfo |
|
1026 |
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy) |
|
1027 |
in |
|
1028 |
fn phi => fold_rev |
|
1029 |
(Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules |
|
1030 |
end |
|
1031 |
in |
|
1032 |
case Lifting_Info.lookup_restore_data lthy pointer of |
|
1033 |
SOME refresh_data => |
|
1034 |
Local_Theory.declaration {syntax = false, pervasive = true} |
|
1035 |
(fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer |
|
1036 |
(new_transfer_rules refresh_data lthy phi)) lthy |
|
1037 |
| NONE => error "The lifting bundle refers to non-existent restore data." |
|
1038 |
end |
|
1039 |
||
1040 |
fun lifting_update_cmd bundle_name lthy = |
|
1041 |
update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy |
|
1042 |
||
1043 |
val _ = |
|
69593 | 1044 |
Outer_Syntax.local_theory \<^command_keyword>\<open>lifting_update\<close> |
53651 | 1045 |
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer" |
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
67710
diff
changeset
|
1046 |
(Parse.name_position >> lifting_update_cmd) |
53651 | 1047 |
|
1048 |
end |