author | wenzelm |
Sun, 03 May 2015 14:35:48 +0200 | |
changeset 60239 | 755e11e2e15d |
parent 60231 | 0daab758e087 |
child 60784 | 4f590c08fd5d |
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 |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
48 |
val ((_, (_ , def_thm)), lthy) = if #notes config then |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
49 |
Local_Theory.define ((crel_name, NoSyn), ((Thm.def_binding crel_name, []), fixed_def_term)) lthy |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
50 |
else |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
51 |
Local_Theory.define ((Binding.concealed crel_name, NoSyn), ((Binding.empty, []), fixed_def_term)) lthy |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
52 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
53 |
(def_thm, lthy) |
47308 | 54 |
end |
55 |
||
50227 | 56 |
fun print_define_pcrel_warning msg = |
57 |
let |
|
58 |
val warning_msg = cat_lines |
|
59 |
["Generation of a parametrized correspondence relation failed.", |
|
60 |
(Pretty.string_of (Pretty.block |
|
61 |
[Pretty.str "Reason:", Pretty.brk 2, msg]))] |
|
62 |
in |
|
63 |
warning warning_msg |
|
64 |
end |
|
65 |
||
60239 | 66 |
fun define_pcrel (config: config) crel lthy = |
50227 | 67 |
let |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50231
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
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
|
71 |
val rty_raw = (domain_type o range_type o fastype_of) param_rel |
50227 | 72 |
val thy = Proof_Context.theory_of lthy |
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
val rty = (domain_type o fastype_of) param_rel_fixed |
50227 | 81 |
val relcomp_op = Const (@{const_name "relcompp"}, |
82 |
(rty --> rty' --> HOLogic.boolT) --> |
|
83 |
(rty' --> qty --> HOLogic.boolT) --> |
|
84 |
rty --> qty --> HOLogic.boolT) |
|
85 |
val qty_name = (fst o dest_Type) qty |
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel |
50227 | 90 |
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
|
91 |
fun note_def lthy = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
92 |
Specification.definition ((SOME (pcrel_name, SOME relator_type, NoSyn)), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
93 |
((Binding.empty, []), definition_term)) lthy |>> (snd #> snd); |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
94 |
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
|
95 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
96 |
val ((_, rhs), prove) = Local_Defs.derived_def lthy true definition_term; |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
97 |
val ((_, (_, raw_th)), lthy) = lthy |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
98 |
|> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs)); |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
99 |
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
|
100 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
101 |
(th, lthy) |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
102 |
end |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
103 |
val (def_thm, lthy) = if #notes config then note_def lthy else raw_def lthy |
50227 | 104 |
in |
105 |
(SOME def_thm, lthy) |
|
106 |
end |
|
107 |
handle Lifting_Term.PARAM_QUOT_THM (_, msg) => (print_define_pcrel_warning msg; (NONE, lthy)) |
|
108 |
||
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
109 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
110 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
111 |
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
|
112 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
113 |
fun print_generate_pcr_cr_eq_error ctxt term = |
56257 | 114 |
let |
115 |
val goal = Const (@{const_name HOL.eq}, dummyT) $ term $ Const (@{const_name HOL.eq}, dummyT) |
|
116 |
val error_msg = cat_lines |
|
117 |
["Generation of a pcr_cr_eq failed.", |
|
118 |
(Pretty.string_of (Pretty.block |
|
119 |
[Pretty.str "Reason: Cannot prove this: ", Pretty.brk 2, Syntax.pretty_term ctxt goal])), |
|
120 |
"Most probably a relator_eq rule for one of the involved types is missing."] |
|
121 |
in |
|
122 |
error error_msg |
|
123 |
end |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
124 |
in |
60239 | 125 |
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
|
126 |
let |
59582 | 127 |
val lhs = (Thm.term_of o Thm.lhs_of) pcr_rel_def |
60239 | 128 |
val qty_name = |
129 |
(Binding.name o Long_Name.base_name o fst o dest_Type o |
|
130 |
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
|
131 |
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
|
132 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
133 |
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
|
134 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
135 |
val typ = (snd o relation_types o snd o dest_Var) var |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
136 |
val sort = Type.sort_of_atyp typ |
59630 | 137 |
val (fresh_var, ctxt') = yield_singleton Variable.invent_types sort ctxt |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
138 |
in |
59630 | 139 |
(apply2 (Thm.cterm_of ctxt') (var, HOLogic.eq_const (TFree fresh_var)), ctxt') |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
140 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
141 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
142 |
val orig_lthy = lthy |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
143 |
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
|
144 |
val pcr_cr_eq = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
145 |
pcr_rel_def |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
146 |
|> Drule.cterm_instantiate 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
|
147 |
|> 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
|
148 |
(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
|
149 |
in |
59582 | 150 |
case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of |
56257 | 151 |
Const (@{const_name "relcompp"}, _) $ Const (@{const_name HOL.eq}, _) $ _ => |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
152 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
153 |
val thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
154 |
pcr_cr_eq |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
155 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.rewr_conv eq_OO_meta)) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
156 |
|> mk_HOL_eq |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
157 |
|> 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
|
158 |
val lthy = (#notes config ? (Local_Theory.note |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
159 |
((Binding.qualified true "pcr_cr_eq" qty_name, []), [thm]) #> snd)) lthy |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
160 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
161 |
(thm, lthy) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
162 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
163 |
| Const (@{const_name "relcompp"}, _) $ t $ _ => print_generate_pcr_cr_eq_error lthy t |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
164 |
| _ => 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
|
165 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
166 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
167 |
|
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
168 |
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
|
169 |
let |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47943
diff
changeset
|
170 |
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
|
171 |
in |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
172 |
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
|
173 |
let |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
174 |
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
|
175 |
in |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
176 |
Local_Theory.background_theory (Code.add_datatype [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
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
|
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
182 |
fun define_abs_type quot_thm lthy = |
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
183 |
if Lifting_Def.can_generate_code_cert quot_thm then |
47308 | 184 |
let |
185 |
val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep} |
|
186 |
val add_abstype_attribute = |
|
59458 | 187 |
Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype_default thm) I) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
188 |
val add_abstype_attrib = Attrib.internal (K add_abstype_attribute) |
47308 | 189 |
in |
190 |
lthy |
|
191 |
|> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm]) |
|
192 |
end |
|
193 |
else |
|
194 |
lthy |
|
195 |
||
53651 | 196 |
local |
197 |
exception QUOT_ERROR of Pretty.T list |
|
198 |
in |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
199 |
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
|
200 |
let |
53651 | 201 |
val _ = |
59582 | 202 |
if (Thm.nprems_of quot_thm > 0) then |
53651 | 203 |
raise QUOT_ERROR [Pretty.block |
204 |
[Pretty.str "The Quotient theorem has extra assumptions:", |
|
205 |
Pretty.brk 1, |
|
206 |
Display.pretty_thm ctxt quot_thm]] |
|
207 |
else () |
|
59582 | 208 |
val _ = quot_thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_Quotient |
53651 | 209 |
handle TERM _ => raise QUOT_ERROR |
210 |
[Pretty.block |
|
211 |
[Pretty.str "The Quotient theorem is not of the right form:", |
|
212 |
Pretty.brk 1, |
|
213 |
Display.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
|
214 |
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
|
215 |
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
|
216 |
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
|
217 |
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
|
218 |
val extra_rty_tfrees = |
47545 | 219 |
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
|
220 |
[] => [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
221 |
| 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
|
222 |
Pretty.brk 1] @ |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
223 |
((Pretty.commas o map (Pretty.str o quote)) extras) @ |
47545 | 224 |
[Pretty.str "."])] |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
225 |
val not_type_constr = |
47545 | 226 |
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
|
227 |
Type _ => [] |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
228 |
| _ => [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
|
229 |
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
|
230 |
Pretty.brk 1, |
47545 | 231 |
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
|
232 |
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
|
233 |
in |
53651 | 234 |
if null errs then () else raise QUOT_ERROR errs |
235 |
end |
|
236 |
handle QUOT_ERROR errs => error (cat_lines (["Sanity check of the quotient theorem failed:"] |
|
237 |
@ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
238 |
end |
|
239 |
||
240 |
fun lifting_bundle qty_full_name qinfo lthy = |
|
241 |
let |
|
242 |
fun qualify suffix defname = Binding.qualified true suffix defname |
|
243 |
val binding = qty_full_name |> Long_Name.base_name |> Binding.name |> qualify "lifting" |
|
244 |
val morphed_binding = Morphism.binding (Local_Theory.target_morphism lthy) binding |
|
245 |
val bundle_name = Name_Space.full_name (Name_Space.naming_of |
|
246 |
(Context.Theory (Proof_Context.theory_of lthy))) morphed_binding |
|
247 |
fun phi_qinfo phi = Lifting_Info.transform_quotient phi qinfo |
|
248 |
||
249 |
val thy = Proof_Context.theory_of lthy |
|
250 |
val dummy_thm = Thm.transfer thy Drule.dummy_thm |
|
59084
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
251 |
val pointer = |
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
252 |
Token.explode (Thy_Header.get_keywords thy) Position.none (cartouche bundle_name) |
53651 | 253 |
val restore_lifting_att = |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
57918
diff
changeset
|
254 |
([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer]) |
53651 | 255 |
in |
256 |
lthy |
|
257 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
|
258 |
(fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi)) |
|
259 |
|> 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
|
260 |
|> pair binding |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
261 |
end |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
262 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
263 |
fun setup_lifting_infr config quot_thm opt_reflp_thm lthy = |
47308 | 264 |
let |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47361
diff
changeset
|
265 |
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
|
266 |
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
|
267 |
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
|
268 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
269 |
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
|
270 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
271 |
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
|
272 |
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
|
273 |
| NONE => (NONE, lthy) |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
274 |
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
|
275 |
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
|
276 |
| NONE => NONE |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
277 |
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
|
278 |
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
|
279 |
fun quot_info phi = Lifting_Info.transform_quotient phi quotients |
51994 | 280 |
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
|
281 |
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
|
282 |
SOME reflp_thm => lthy |
51994 | 283 |
|> (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
|
284 |
[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
|
285 |
|> 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
|
286 |
| NONE => lthy |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
287 |
|> define_abs_type quot_thm |
47308 | 288 |
in |
50227 | 289 |
lthy |
47308 | 290 |
|> Local_Theory.declaration {syntax = false, pervasive = true} |
291 |
(fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi)) |
|
53651 | 292 |
|> lifting_bundle qty_full_name quotients |
47308 | 293 |
end |
294 |
||
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 |
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
|
296 |
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
|
297 |
let |
53651 | 298 |
val tvars = rev (subtract op= exclude (fold Term.add_tvars ts [])) |
299 |
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
|
300 |
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
|
301 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
302 |
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
|
303 |
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
|
304 |
val excludeT = fold (Term.add_tvarsT o snd) exclude [] |
53651 | 305 |
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
|
306 |
val vars = map (apsnd (Term_Subst.instantiateT instT)) |
53651 | 307 |
(rev (subtract op= exclude (fold Term.add_vars ts []))) |
308 |
val (xs, ctxt'') = Variable.variant_fixes (map (#1 o #1) vars) ctxt' |
|
309 |
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
|
310 |
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
|
311 |
|
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 |
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
|
313 |
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
|
314 |
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
|
315 |
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
|
316 |
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
|
317 |
let |
59630 | 318 |
val (fixed_goal, ctxt') = yield_singleton (import_terms_exclude not_fix) goal ctxt |
319 |
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
|
320 |
in |
59630 | 321 |
(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
|
322 |
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
|
323 |
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
|
324 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
325 |
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
|
326 |
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
|
327 |
bi_unique_OO} |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
328 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
329 |
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
|
330 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
331 |
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
|
332 |
let |
59630 | 333 |
val (fixed_goal, ctxt') = yield_singleton (Variable.import_terms true) goal ctxt |
334 |
val init_goal = Goal.init (Thm.cterm_of ctxt' fixed_goal) |
|
335 |
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
|
336 |
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
|
337 |
val tac = |
59630 | 338 |
K (Local_Defs.unfold_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
|
339 |
in |
59630 | 340 |
(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
|
341 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
342 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
343 |
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
|
344 |
let |
59582 | 345 |
val pred_name = |
346 |
(fst o dest_Const o strip_args 1 o HOLogic.dest_Trueprop o Thm.prop_of) constr |
|
347 |
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
|
348 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
349 |
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
|
350 |
end |
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 |
val check_assms = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
353 |
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
|
354 |
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
|
355 |
"bi_unique"] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
356 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
357 |
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
|
358 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
359 |
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
|
360 |
| 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
|
361 |
| is_trivial_assm _ = false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
362 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
363 |
fn thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
364 |
let |
59582 | 365 |
val prems = map HOLogic.dest_Trueprop (Thm.prems_of thm) |
366 |
val thm_name = |
|
367 |
(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
|
368 |
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
|
369 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
370 |
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
|
371 |
else |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
372 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
373 |
val pretty_msg = Pretty.block ([Pretty.str "Non-trivial assumptions in ", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
374 |
Pretty.str thm_name, |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
375 |
Pretty.str " transfer rule found:", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
376 |
Pretty.brk 1] @ |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
377 |
((Pretty.commas o map (Syntax.pretty_term ctxt)) non_trivial_assms) @ |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
378 |
[Pretty.str "."]) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
379 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
380 |
warning (Pretty.str_of pretty_msg) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
381 |
end |
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 |
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
|
386 |
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
|
387 |
val _ = check_assms thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
388 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
389 |
thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
390 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
391 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
392 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
393 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
394 |
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
|
395 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
396 |
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
|
397 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
398 |
(* it doesn't raise an exception because it would have already raised it in define_pcrel *) |
59630 | 399 |
val (quot_thm, _, ctxt') = Lifting_Term.prove_param_quot_thm lthy rty |
400 |
val parametrized_relator = |
|
401 |
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
|
402 |
val id_transfer = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
403 |
@{thm id_transfer} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
404 |
|> 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
|
405 |
|> Conv.fconv_rule(HOLogic.Trueprop_conv (Conv.arg_conv id_unfold then_conv Conv.arg1_conv id_unfold)) |
59582 | 406 |
val var = Var (hd (Term.add_vars (Thm.prop_of id_transfer) [])) |
59630 | 407 |
val inst = [(Thm.cterm_of lthy var, Thm.cterm_of lthy parametrized_relator)] |
53651 | 408 |
val id_par_thm = Drule.cterm_instantiate inst id_transfer |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
409 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
410 |
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
|
411 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
412 |
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
|
413 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
414 |
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
|
415 |
["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
|
416 |
"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
|
417 |
(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
|
418 |
[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
|
419 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
420 |
(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
|
421 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
422 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
423 |
|
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
|
424 |
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
|
425 |
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
|
426 |
(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
|
427 |
|
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 |
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
|
429 |
let |
59582 | 430 |
val ct = |
431 |
thm |> Thm.cprop_of |> Drule.strip_imp_concl |
|
432 |
|> Thm.dest_arg |> Thm.dest_arg1 |> Thm.dest_arg |
|
59586 | 433 |
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
|
434 |
val thm = Thm.instantiate (Thm.match (ct, Thm.rhs_of pcrel_def)) thm |
53651 | 435 |
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
|
436 |
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
|
437 |
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
|
438 |
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
|
439 |
|
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 |
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
|
441 |
let |
59582 | 442 |
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
|
443 |
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
|
444 |
val reduced_assm = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
445 |
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
|
446 |
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
|
447 |
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
|
448 |
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
|
449 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
450 |
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
|
451 |
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
|
452 |
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
|
453 |
let |
59582 | 454 |
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
|
455 |
val reduced_assm = |
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59487
diff
changeset
|
456 |
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
|
457 |
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
|
458 |
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
|
459 |
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
|
460 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
52883
diff
changeset
|
461 |
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
|
462 |
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
|
463 |
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
|
464 |
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
|
465 |
(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
|
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 |
|> 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
|
468 |
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
|
469 |
(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
|
470 |
|> 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
|
471 |
|> 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
|
472 |
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
|
473 |
(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
|
474 |
|> 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
|
475 |
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
|
476 |
[("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
|
477 |
("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
|
478 |
("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
|
479 |
("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
|
480 |
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
|
481 |
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
|
482 |
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
|
483 |
|
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
|
484 |
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
|
485 |
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
|
486 |
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
|
487 |
(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
|
488 |
|> 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
|
489 |
|> 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
|
490 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
491 |
[("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
|
492 |
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
|
493 |
|
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51374
diff
changeset
|
494 |
end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
495 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
496 |
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
|
497 |
#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
|
498 |
|
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
|
499 |
fun get_Domainp_thm quot_thm = |
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
500 |
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
|
501 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
502 |
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
|
503 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
504 |
val notes = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
505 |
if names then map (fn (name, thms, attrs) => ((name, []), [(thms, attrs)])) thms |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
506 |
else map_filter (fn (_, thms, attrs) => if null attrs then NONE |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
507 |
else SOME ((Binding.empty, []), [(thms, attrs)])) thms |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
508 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
509 |
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
|
510 |
end |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
511 |
|
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
512 |
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
|
513 |
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
|
514 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
515 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
516 |
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
|
517 |
|
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
518 |
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
|
519 |
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
|
520 |
(in the form "reflp R") |
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
521 |
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
|
522 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
523 |
|
60239 | 524 |
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
|
525 |
let |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
526 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
527 |
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
|
528 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
529 |
val (rty, qty) = quot_thm_rty_qty quot_thm |
47575 | 530 |
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
|
531 |
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
|
532 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name |
47545 | 533 |
fun qualify suffix = Binding.qualified true suffix 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
|
534 |
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
|
535 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
536 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
537 |
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
|
538 |
[("abs_induct", @{thms Quotient_total_abs_induct}, [induct_attr]), |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
539 |
("abs_eq_iff", @{thms Quotient_total_abs_eq_iff}, [] )] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
540 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
541 |
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
|
542 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
543 |
| NONE => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
544 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
545 |
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
|
546 |
[("abs_induct", @{thms Quotient_abs_induct}, [induct_attr])] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
547 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
548 |
map_thms qualify (fn thm => quot_thm RS thm) thms |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
549 |
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
|
550 |
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
|
551 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
552 |
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
|
553 |
let |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
554 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
555 |
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
|
556 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
557 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
558 |
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
|
559 |
[("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
|
560 |
("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
|
561 |
("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
|
562 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
563 |
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
|
564 |
end |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
565 |
| 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
|
566 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
567 |
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
|
568 |
[("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
|
569 |
("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
|
570 |
("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
|
571 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
572 |
notes2 @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
573 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
574 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
575 |
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
|
576 |
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
|
577 |
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
|
578 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
579 |
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
|
580 |
["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
|
581 |
(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
|
582 |
[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
|
583 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
584 |
error error_msg |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
585 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
586 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
587 |
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
|
588 |
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
|
589 |
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
|
590 |
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
|
591 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
592 |
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
|
593 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
594 |
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
|
595 |
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
|
596 |
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
|
597 |
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
|
598 |
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
|
599 |
(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
|
600 |
([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
|
601 |
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
|
602 |
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
|
603 |
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
|
604 |
[("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
|
605 |
("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
|
606 |
("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
|
607 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
608 |
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
|
609 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
610 |
| NONE => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
611 |
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
|
612 |
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
|
613 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
614 |
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
|
615 |
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
|
616 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
617 |
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
|
618 |
(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
|
619 |
opt_par_thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
620 |
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
|
621 |
(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
|
622 |
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
|
623 |
(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
|
624 |
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
|
625 |
[("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
|
626 |
("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
|
627 |
("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
|
628 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
629 |
notes2 @ notes1 @ notes |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
630 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
631 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
632 |
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
|
633 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
634 |
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
|
635 |
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
|
636 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
637 |
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
|
638 |
end |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
639 |
in |
50227 | 640 |
lthy |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
641 |
|> 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
|
642 |
||> setup_rules |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
643 |
end |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
644 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
645 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
646 |
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
|
647 |
|
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
|
648 |
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
|
649 |
as an abstract type in the code generator |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
650 |
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
|
651 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47779
diff
changeset
|
652 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
653 |
fun setup_by_typedef_thm config typedef_thm lthy = |
47308 | 654 |
let |
59582 | 655 |
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
|
656 |
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
|
657 |
(**) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
658 |
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
|
659 |
(**) |
47545 | 660 |
val quot_thm = case typedef_set of |
56257 | 661 |
Const (@{const_name top}, _) => |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
662 |
[typedef_thm, T_def] MRSL @{thm UNIV_typedef_to_Quotient} |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
663 |
| Const (@{const_name "Collect"}, _) $ Abs (_, _, _) => |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
664 |
[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
|
665 |
| _ => |
47545 | 666 |
[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
|
667 |
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
|
668 |
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
|
669 |
val qty_name = (Binding.name o Long_Name.base_name) qty_full_name |
47545 | 670 |
fun qualify suffix = Binding.qualified true suffix qty_name |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
671 |
val opt_reflp_thm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
672 |
case typedef_set of |
56257 | 673 |
Const (@{const_name top}, _) => |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
674 |
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
|
675 |
| _ => 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
|
676 |
val dom_thm = get_Domainp_thm quot_thm |
47308 | 677 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
678 |
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
|
679 |
let |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
680 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
681 |
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
|
682 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
683 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
684 |
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
|
685 |
[("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
|
686 |
("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
|
687 |
("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
|
688 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
689 |
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
|
690 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
691 |
| NONE => |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
692 |
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
|
693 |
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
|
694 |
[("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
|
695 |
("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
|
696 |
("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
|
697 |
("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
|
698 |
("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
|
699 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
700 |
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
|
701 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
702 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
703 |
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
|
704 |
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
|
705 |
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
|
706 |
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
|
707 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
708 |
val notes1 = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
709 |
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
|
710 |
SOME reflp_thm => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
711 |
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
|
712 |
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
|
713 |
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
|
714 |
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
|
715 |
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
|
716 |
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
|
717 |
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
|
718 |
(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
|
719 |
([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
|
720 |
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
|
721 |
[("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
|
722 |
("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
|
723 |
("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
|
724 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
725 |
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
|
726 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
727 |
| NONE => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
728 |
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
|
729 |
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
|
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 |
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
|
732 |
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
|
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 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
|
735 |
(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
|
736 |
[("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
|
737 |
val notes3 = |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
738 |
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
|
739 |
(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
|
740 |
[("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
|
741 |
("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
|
742 |
("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
|
743 |
("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
|
744 |
in |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
745 |
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
|
746 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
747 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
748 |
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
|
749 |
|
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
750 |
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
|
751 |
let |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
752 |
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
|
753 |
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
|
754 |
in |
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
755 |
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
|
756 |
end |
47308 | 757 |
in |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
758 |
lthy |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
759 |
|> 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
|
760 |
||> setup_rules |
47308 | 761 |
end |
762 |
||
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
763 |
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
|
764 |
let |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
765 |
val input_thm = singleton (Attrib.eval_thms lthy) xthm |
59582 | 766 |
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
|
767 |
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
|
768 |
|
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
769 |
fun sanity_check_reflp_thm reflp_thm = |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
770 |
let |
59582 | 771 |
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
|
772 |
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
|
773 |
in |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
774 |
case reflp_tm of |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
775 |
Const (@{const_name reflp}, _) $ _ => () |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
776 |
| _ => 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
|
777 |
end |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
778 |
|
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
779 |
fun check_qty qty = if not (is_Type qty) |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
780 |
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
|
781 |
else () |
60225
eb4e322734bf
note theorems by Local_Theory.notes (it is faster); make note of the generated theorems optional
kuncar
parents:
59936
diff
changeset
|
782 |
|
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
783 |
fun setup_quotient () = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
784 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
785 |
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
|
786 |
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
|
787 |
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
|
788 |
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
|
789 |
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
|
790 |
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
|
791 |
end |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
792 |
|
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
793 |
fun setup_typedef () = |
55487
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
794 |
let |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
795 |
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
|
796 |
val _ = check_qty qty |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
797 |
in |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
798 |
case opt_reflp_xthm of |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
799 |
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
|
800 |
| NONE => ( |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
801 |
case opt_par_xthm of |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
802 |
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
|
803 |
| 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
|
804 |
) |
6380313b8ed5
abstract type must be a type constructor; check it
kuncar
parents:
54335
diff
changeset
|
805 |
end |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
806 |
in |
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
807 |
case input_term of |
47566
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
808 |
(Const (@{const_name Quotient}, _) $ _ $ _ $ _ $ _) => setup_quotient () |
c201a1fe0a81
setup_lifting: no_code switch and supoport for quotient theorems
kuncar
parents:
47545
diff
changeset
|
809 |
| (Const (@{const_name type_definition}, _) $ _ $ _ $ _) => setup_typedef () |
47521
69f95ac85c3d
tuned the setup of lifting; generate transfer rules for typedef and Quotient thms
kuncar
parents:
47379
diff
changeset
|
810 |
| _ => 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
|
811 |
end |
47308 | 812 |
|
813 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59630
diff
changeset
|
814 |
Outer_Syntax.local_theory @{command_keyword setup_lifting} |
50214 | 815 |
"setup lifting infrastructure" |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
816 |
(Parse.xthm -- Scan.option Parse.xthm |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
817 |
-- Scan.option (@{keyword "parametric"} |-- Parse.!!! Parse.xthm) >> |
59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
59458
diff
changeset
|
818 |
(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
|
819 |
setup_lifting_cmd xthm opt_reflp_xthm opt_par_xthm)) |
53651 | 820 |
|
821 |
(* restoring lifting infrastructure *) |
|
822 |
||
823 |
local |
|
824 |
exception PCR_ERROR of Pretty.T list |
|
825 |
in |
|
826 |
||
827 |
fun lifting_restore_sanity_check ctxt (qinfo:Lifting_Info.quotient) = |
|
828 |
let |
|
829 |
val quot_thm = (#quot_thm qinfo) |
|
830 |
val _ = quot_thm_sanity_check ctxt quot_thm |
|
831 |
val pcr_info_err = |
|
832 |
(case #pcr_info qinfo of |
|
833 |
SOME pcr => |
|
834 |
let |
|
835 |
val pcrel_def = #pcrel_def pcr |
|
836 |
val pcr_cr_eq = #pcr_cr_eq pcr |
|
59582 | 837 |
val (def_lhs, _) = Logic.dest_equals (Thm.prop_of pcrel_def) |
53651 | 838 |
handle TERM _ => raise PCR_ERROR [Pretty.block |
839 |
[Pretty.str "The pcr definiton theorem is not a plain meta equation:", |
|
840 |
Pretty.brk 1, |
|
841 |
Display.pretty_thm ctxt pcrel_def]] |
|
842 |
val pcr_const_def = head_of def_lhs |
|
59582 | 843 |
val (eq_lhs, eq_rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of pcr_cr_eq)) |
53651 | 844 |
handle TERM _ => raise PCR_ERROR [Pretty.block |
845 |
[Pretty.str "The pcr_cr equation theorem is not a plain equation:", |
|
846 |
Pretty.brk 1, |
|
847 |
Display.pretty_thm ctxt pcr_cr_eq]] |
|
848 |
val (pcr_const_eq, eqs) = strip_comb eq_lhs |
|
56257 | 849 |
fun is_eq (Const (@{const_name HOL.eq}, _)) = true |
53651 | 850 |
| is_eq _ = false |
851 |
fun eq_Const (Const (name1, _)) (Const (name2, _)) = (name1 = name2) |
|
852 |
| eq_Const _ _ = false |
|
853 |
val all_eqs = if not (forall is_eq eqs) then |
|
854 |
[Pretty.block |
|
855 |
[Pretty.str "Arguments of the lhs of the pcr_cr equation theorem are not only equalities:", |
|
856 |
Pretty.brk 1, |
|
857 |
Display.pretty_thm ctxt pcr_cr_eq]] |
|
858 |
else [] |
|
859 |
val pcr_consts_not_equal = if not (eq_Const pcr_const_def pcr_const_eq) then |
|
860 |
[Pretty.block |
|
861 |
[Pretty.str "Parametrized correspondence relation constants in pcr_def and pcr_cr_eq are not equal:", |
|
862 |
Pretty.brk 1, |
|
863 |
Syntax.pretty_term ctxt pcr_const_def, |
|
864 |
Pretty.brk 1, |
|
865 |
Pretty.str "vs.", |
|
866 |
Pretty.brk 1, |
|
867 |
Syntax.pretty_term ctxt pcr_const_eq]] |
|
868 |
else [] |
|
869 |
val crel = quot_thm_crel quot_thm |
|
870 |
val cr_consts_not_equal = if not (eq_Const crel eq_rhs) then |
|
871 |
[Pretty.block |
|
872 |
[Pretty.str "Correspondence relation constants in the Quotient theorem and pcr_cr_eq are not equal:", |
|
873 |
Pretty.brk 1, |
|
874 |
Syntax.pretty_term ctxt crel, |
|
875 |
Pretty.brk 1, |
|
876 |
Pretty.str "vs.", |
|
877 |
Pretty.brk 1, |
|
878 |
Syntax.pretty_term ctxt eq_rhs]] |
|
879 |
else [] |
|
880 |
in |
|
881 |
all_eqs @ pcr_consts_not_equal @ cr_consts_not_equal |
|
882 |
end |
|
883 |
| NONE => []) |
|
884 |
val errs = pcr_info_err |
|
885 |
in |
|
886 |
if null errs then () else raise PCR_ERROR errs |
|
887 |
end |
|
888 |
handle PCR_ERROR errs => error (cat_lines (["Sanity check failed:"] |
|
889 |
@ (map (Pretty.string_of o Pretty.item o single) errs))) |
|
890 |
end |
|
891 |
||
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
892 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
893 |
Registers the data in qinfo in the Lifting infrastructure. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
894 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
54333
diff
changeset
|
895 |
|
53651 | 896 |
fun lifting_restore qinfo ctxt = |
897 |
let |
|
898 |
val _ = lifting_restore_sanity_check (Context.proof_of ctxt) qinfo |
|
899 |
val (_, qty) = quot_thm_rty_qty (#quot_thm qinfo) |
|
900 |
val qty_full_name = (fst o dest_Type) qty |
|
901 |
val stored_qinfo = Lifting_Info.lookup_quotients (Context.proof_of ctxt) qty_full_name |
|
902 |
in |
|
903 |
if is_some (stored_qinfo) andalso not (Lifting_Info.quotient_eq (qinfo, (the stored_qinfo))) |
|
904 |
then error (Pretty.string_of |
|
905 |
(Pretty.block |
|
906 |
[Pretty.str "Lifting is already setup for the type", |
|
907 |
Pretty.brk 1, |
|
908 |
Pretty.quote (Syntax.pretty_typ (Context.proof_of ctxt) qty)])) |
|
909 |
else Lifting_Info.update_quotients qty_full_name qinfo ctxt |
|
910 |
end |
|
911 |
||
912 |
val parse_opt_pcr = |
|
913 |
Scan.optional (Attrib.thm -- Attrib.thm >> |
|
914 |
(fn (pcrel_def, pcr_cr_eq) => SOME {pcrel_def = pcrel_def, pcr_cr_eq = pcr_cr_eq})) NONE |
|
915 |
||
916 |
val lifting_restore_attribute_setup = |
|
917 |
Attrib.setup @{binding lifting_restore} |
|
918 |
((Attrib.thm -- parse_opt_pcr) >> |
|
919 |
(fn (quot_thm, opt_pcr) => |
|
920 |
let val qinfo = { quot_thm = quot_thm, pcr_info = opt_pcr} |
|
921 |
in Thm.declaration_attribute (K (lifting_restore qinfo)) end)) |
|
922 |
"restoring lifting infrastructure" |
|
923 |
||
924 |
val _ = Theory.setup lifting_restore_attribute_setup |
|
925 |
||
926 |
fun lifting_restore_internal bundle_name ctxt = |
|
927 |
let |
|
928 |
val restore_info = Lifting_Info.lookup_restore_data (Context.proof_of ctxt) bundle_name |
|
929 |
in |
|
930 |
case restore_info of |
|
931 |
SOME restore_info => |
|
932 |
ctxt |
|
933 |
|> lifting_restore (#quotient restore_info) |
|
934 |
|> fold_rev Transfer.transfer_raw_add (Item_Net.content (#transfer_rules restore_info)) |
|
935 |
| NONE => ctxt |
|
936 |
end |
|
937 |
||
938 |
val lifting_restore_internal_attribute_setup = |
|
939 |
Attrib.setup @{binding lifting_restore_internal} |
|
59084
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
940 |
(Scan.lift Parse.cartouche >> |
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
941 |
(fn name => Thm.declaration_attribute (K (lifting_restore_internal name)))) |
53651 | 942 |
"restoring lifting infrastructure; internal attribute; not meant to be used directly by regular users" |
943 |
||
944 |
val _ = Theory.setup lifting_restore_internal_attribute_setup |
|
945 |
||
946 |
(* lifting_forget *) |
|
947 |
||
948 |
val monotonicity_names = [@{const_name right_unique}, @{const_name left_unique}, @{const_name right_total}, |
|
949 |
@{const_name left_total}, @{const_name bi_unique}, @{const_name bi_total}] |
|
950 |
||
951 |
fun fold_transfer_rel f (Const (@{const_name "Transfer.Rel"}, _) $ rel $ _ $ _) = f rel |
|
952 |
| fold_transfer_rel f (Const (@{const_name "HOL.eq"}, _) $ |
|
953 |
(Const (@{const_name Domainp}, _) $ rel) $ _) = f rel |
|
954 |
| fold_transfer_rel f (Const (name, _) $ rel) = |
|
955 |
if member op= monotonicity_names name then f rel else f @{term undefined} |
|
956 |
| fold_transfer_rel f _ = f @{term undefined} |
|
957 |
||
958 |
fun filter_transfer_rules_by_rel transfer_rel transfer_rules = |
|
959 |
let |
|
960 |
val transfer_rel_name = transfer_rel |> dest_Const |> fst; |
|
961 |
fun has_transfer_rel thm = |
|
962 |
let |
|
59582 | 963 |
val concl = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |
53651 | 964 |
in |
965 |
member op= (fold_transfer_rel (fn tm => Term.add_const_names tm []) concl) transfer_rel_name |
|
966 |
end |
|
967 |
handle TERM _ => false |
|
968 |
in |
|
969 |
filter has_transfer_rel transfer_rules |
|
970 |
end |
|
971 |
||
972 |
type restore_data = {quotient : Lifting_Info.quotient, transfer_rules: thm Item_Net.T} |
|
973 |
||
53754 | 974 |
fun get_transfer_rel (qinfo : Lifting_Info.quotient) = |
53651 | 975 |
let |
59582 | 976 |
fun get_pcrel pcr_def = pcr_def |> Thm.concl_of |> Logic.dest_equals |> fst |> head_of |
53651 | 977 |
in |
978 |
if is_some (#pcr_info qinfo) |
|
979 |
then get_pcrel (#pcrel_def (the (#pcr_info qinfo))) |
|
980 |
else quot_thm_crel (#quot_thm qinfo) |
|
981 |
end |
|
982 |
||
983 |
fun pointer_of_bundle_name bundle_name ctxt = |
|
984 |
let |
|
56026
893fe12639bc
tuned signature -- prefer Name_Space.get with its builtin error;
wenzelm
parents:
55563
diff
changeset
|
985 |
val bundle = Bundle.get_bundle_cmd ctxt bundle_name |
53651 | 986 |
in |
987 |
case bundle of |
|
988 |
[(_, [arg_src])] => |
|
56035
745f568837f1
proper Args.syntax for slightly odd bundle trickery;
wenzelm
parents:
56029
diff
changeset
|
989 |
let |
59084
f982f3072d79
more robust bundle_name: avoid assumptions about identifier, keywords etc.;
wenzelm
parents:
59083
diff
changeset
|
990 |
val (name, _) = Token.syntax (Scan.lift Parse.cartouche) arg_src ctxt |
56035
745f568837f1
proper Args.syntax for slightly odd bundle trickery;
wenzelm
parents:
56029
diff
changeset
|
991 |
handle ERROR _ => error "The provided bundle is not a lifting bundle." |
745f568837f1
proper Args.syntax for slightly odd bundle trickery;
wenzelm
parents:
56029
diff
changeset
|
992 |
in name end |
53651 | 993 |
| _ => error "The provided bundle is not a lifting bundle." |
994 |
end |
|
995 |
||
60226
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
996 |
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
|
997 |
(Context.Theory (Proof_Context.theory_of ctxt))) binding |
ec23f2a97ba4
publish lifting_forget and lifting_udpate interface
kuncar
parents:
60225
diff
changeset
|
998 |
|
53651 | 999 |
fun lifting_forget pointer lthy = |
1000 |
let |
|
1001 |
fun get_transfer_rules_to_delete qinfo ctxt = |
|
1002 |
let |
|
53754 | 1003 |
val transfer_rel = get_transfer_rel qinfo |
53651 | 1004 |
in |
1005 |
filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw ctxt) |
|
1006 |
end |
|
1007 |
in |
|
1008 |
case Lifting_Info.lookup_restore_data lthy pointer of |
|
1009 |
SOME restore_info => |
|
1010 |
let |
|
1011 |
val qinfo = #quotient restore_info |
|
1012 |
val quot_thm = #quot_thm qinfo |
|
1013 |
val transfer_rules = get_transfer_rules_to_delete qinfo lthy |
|
1014 |
in |
|
1015 |
Local_Theory.declaration {syntax = false, pervasive = true} |
|
1016 |
(K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm)) |
|
1017 |
lthy |
|
1018 |
end |
|
1019 |
| NONE => error "The lifting bundle refers to non-existent restore data." |
|
1020 |
end |
|
1021 |
||
1022 |
||
1023 |
fun lifting_forget_cmd bundle_name lthy = |
|
1024 |
lifting_forget (pointer_of_bundle_name bundle_name lthy) lthy |
|
1025 |
||
1026 |
||
1027 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59630
diff
changeset
|
1028 |
Outer_Syntax.local_theory @{command_keyword lifting_forget} |
53651 | 1029 |
"unsetup Lifting and Transfer for the given lifting bundle" |
1030 |
(Parse.position Parse.xname >> (lifting_forget_cmd)) |
|
1031 |
||
1032 |
(* lifting_update *) |
|
1033 |
||
1034 |
fun update_transfer_rules pointer lthy = |
|
1035 |
let |
|
53754 | 1036 |
fun new_transfer_rules ({ quotient = qinfo, ... }:Lifting_Info.restore_data) lthy = |
53651 | 1037 |
let |
1038 |
val transfer_rel = get_transfer_rel qinfo |
|
1039 |
val transfer_rules = filter_transfer_rules_by_rel transfer_rel (Transfer.get_transfer_raw lthy) |
|
1040 |
in |
|
1041 |
fn phi => fold_rev |
|
1042 |
(Item_Net.update o Morphism.thm phi) transfer_rules Thm.full_rules |
|
1043 |
end |
|
1044 |
in |
|
1045 |
case Lifting_Info.lookup_restore_data lthy pointer of |
|
1046 |
SOME refresh_data => |
|
1047 |
Local_Theory.declaration {syntax = false, pervasive = true} |
|
1048 |
(fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer |
|
1049 |
(new_transfer_rules refresh_data lthy phi)) lthy |
|
1050 |
| NONE => error "The lifting bundle refers to non-existent restore data." |
|
1051 |
end |
|
1052 |
||
1053 |
fun lifting_update_cmd bundle_name lthy = |
|
1054 |
update_transfer_rules (pointer_of_bundle_name bundle_name lthy) lthy |
|
1055 |
||
1056 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59630
diff
changeset
|
1057 |
Outer_Syntax.local_theory @{command_keyword lifting_update} |
53651 | 1058 |
"add newly introduced transfer rules to a bundle storing the state of Lifting and Transfer" |
1059 |
(Parse.position Parse.xname >> lifting_update_cmd) |
|
1060 |
||
1061 |
end |