author | wenzelm |
Sun, 30 Sep 2018 12:50:28 +0200 | |
changeset 69091 | ce62fd14961a |
parent 69090 | 1b656a2ec0ad |
child 69092 | 854bd35cad49 |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Tools/Lifting/lifting_info.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
4 |
Context data for the lifting package. |
|
5 |
*) |
|
6 |
||
7 |
signature LIFTING_INFO = |
|
8 |
sig |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
9 |
type quot_map = {rel_quot_thm: thm} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
10 |
val lookup_quot_maps: Proof.context -> string -> quot_map option |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
11 |
val print_quot_maps: Proof.context -> unit |
69089 | 12 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
13 |
type pcr = {pcrel_def: thm, pcr_cr_eq: thm} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
14 |
type quotient = {quot_thm: thm, pcr_info: pcr option} |
53651 | 15 |
val pcr_eq: pcr * pcr -> bool |
16 |
val quotient_eq: quotient * quotient -> bool |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
17 |
val transform_quotient: morphism -> quotient -> quotient |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
18 |
val lookup_quotients: Proof.context -> string -> quotient option |
60235
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
19 |
val lookup_quot_thm_quotients: Proof.context -> thm -> quotient option |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
20 |
val update_quotients: string -> quotient -> Context.generic -> Context.generic |
53650 | 21 |
val delete_quotients: thm -> Context.generic -> Context.generic |
47308 | 22 |
val print_quotients: Proof.context -> unit |
23 |
||
53651 | 24 |
type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} |
25 |
val lookup_restore_data: Proof.context -> string -> restore_data option |
|
26 |
val init_restore_data: string -> quotient -> Context.generic -> Context.generic |
|
69089 | 27 |
val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic |
53651 | 28 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
29 |
val get_relator_eq_onp_rules: Proof.context -> thm list |
69089 | 30 |
|
47982
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
31 |
val get_reflexivity_rules: Proof.context -> thm list |
7aa35601ff65
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents:
47951
diff
changeset
|
32 |
val add_reflexivity_rule_attribute: attribute |
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
33 |
|
69089 | 34 |
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
35 |
pos_distr_rules: thm list, neg_distr_rules: thm list} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
36 |
val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
37 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
38 |
val add_no_code_type: string -> Context.generic -> Context.generic |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
39 |
val is_no_code_type: Proof.context -> string -> bool |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
40 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
41 |
val get_quot_maps : Proof.context -> quot_map Symtab.table |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
42 |
val get_quotients : Proof.context -> quotient Symtab.table |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
43 |
val get_relator_distr_data : Proof.context -> relator_distr_data Symtab.table |
53651 | 44 |
val get_restore_data : Proof.context -> restore_data Symtab.table |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
45 |
val get_no_code_types : Proof.context -> unit Symtab.table |
53651 | 46 |
end |
47308 | 47 |
|
48 |
structure Lifting_Info: LIFTING_INFO = |
|
49 |
struct |
|
50 |
||
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
51 |
open Lifting_Util |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
52 |
|
69089 | 53 |
|
54 |
(* context data *) |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
55 |
|
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
56 |
type quot_map = {rel_quot_thm: thm} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
57 |
type pcr = {pcrel_def: thm, pcr_cr_eq: thm} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
58 |
type quotient = {quot_thm: thm, pcr_info: pcr option} |
69089 | 59 |
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
60 |
pos_distr_rules: thm list, neg_distr_rules: thm list} |
53651 | 61 |
type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T} |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
62 |
|
53684 | 63 |
fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1}, |
69089 | 64 |
{pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = |
53684 | 65 |
Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2) |
66 |
||
67 |
fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1}, |
|
68 |
{quot_thm = quot_thm2, pcr_info = pcr_info2}) = |
|
69088 | 69 |
Thm.eq_thm (quot_thm1, quot_thm2) andalso eq_option pcr_eq (pcr_info1, pcr_info2) |
53684 | 70 |
|
53754 | 71 |
fun join_restore_data key (rd1:restore_data, rd2) = |
53684 | 72 |
if pointer_eq (rd1, rd2) then raise Symtab.SAME else |
73 |
if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else |
|
69089 | 74 |
{ quotient = #quotient rd1, |
53684 | 75 |
transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)} |
76 |
||
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
77 |
structure Data = Generic_Data |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
78 |
( |
69089 | 79 |
type T = |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
80 |
{ quot_maps : quot_map Symtab.table, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
81 |
quotients : quotient Symtab.table, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
82 |
reflexivity_rules : thm Item_Net.T, |
53651 | 83 |
relator_distr_data : relator_distr_data Symtab.table, |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
84 |
restore_data : restore_data Symtab.table, |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
85 |
no_code_types : unit Symtab.table |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
86 |
} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
87 |
val empty = |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
88 |
{ quot_maps = Symtab.empty, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
89 |
quotients = Symtab.empty, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
90 |
reflexivity_rules = Thm.full_rules, |
53651 | 91 |
relator_distr_data = Symtab.empty, |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
92 |
restore_data = Symtab.empty, |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
93 |
no_code_types = Symtab.empty |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
94 |
} |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
95 |
val extend = I |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
96 |
fun merge |
69089 | 97 |
( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
98 |
restore_data = rd1, no_code_types = nct1 }, |
53651 | 99 |
{ quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2, |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
100 |
restore_data = rd2, no_code_types = nct2 } ) = |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
101 |
{ quot_maps = Symtab.merge (K true) (qm1, qm2), |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
102 |
quotients = Symtab.merge (K true) (q1, q2), |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
103 |
reflexivity_rules = Item_Net.merge (rr1, rr2), |
53651 | 104 |
relator_distr_data = Symtab.merge (K true) (rdd1, rdd2), |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
105 |
restore_data = Symtab.join join_restore_data (rd1, rd2), |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
106 |
no_code_types = Symtab.merge (K true) (nct1, nct2) |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
107 |
} |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
108 |
) |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
109 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
110 |
fun map_data f1 f2 f3 f4 f5 f6 |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
111 |
{ quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } = |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
112 |
{ quot_maps = f1 quot_maps, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
113 |
quotients = f2 quotients, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
114 |
reflexivity_rules = f3 reflexivity_rules, |
53651 | 115 |
relator_distr_data = f4 relator_distr_data, |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
116 |
restore_data = f5 restore_data, |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
117 |
no_code_types = f6 no_code_types |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
118 |
} |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
119 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
120 |
fun map_quot_maps f = map_data f I I I I I |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
121 |
fun map_quotients f = map_data I f I I I I |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
122 |
fun map_reflexivity_rules f = map_data I I f I I I |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
123 |
fun map_relator_distr_data f = map_data I I I f I I |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
124 |
fun map_restore_data f = map_data I I I I f I |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
125 |
fun map_no_code_types f = map_data I I I I I f |
69089 | 126 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
127 |
val get_quot_maps' = #quot_maps o Data.get |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
128 |
val get_quotients' = #quotients o Data.get |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
129 |
val get_reflexivity_rules' = #reflexivity_rules o Data.get |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
130 |
val get_relator_distr_data' = #relator_distr_data o Data.get |
53651 | 131 |
val get_restore_data' = #restore_data o Data.get |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
132 |
val get_no_code_types' = #no_code_types o Data.get |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
133 |
|
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
134 |
fun get_quot_maps ctxt = get_quot_maps' (Context.Proof ctxt) |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
135 |
fun get_quotients ctxt = get_quotients' (Context.Proof ctxt) |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
136 |
fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt) |
53651 | 137 |
fun get_restore_data ctxt = get_restore_data' (Context.Proof ctxt) |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
138 |
fun get_no_code_types ctxt = get_no_code_types' (Context.Proof ctxt) |
47308 | 139 |
|
69089 | 140 |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
141 |
(* info about Quotient map theorems *) |
47308 | 142 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
143 |
val lookup_quot_maps = Symtab.lookup o get_quot_maps |
47308 | 144 |
|
47784 | 145 |
fun quot_map_thm_sanity_check rel_quot_thm ctxt = |
146 |
let |
|
69089 | 147 |
fun quot_term_absT ctxt quot_term = |
148 |
let |
|
47784 | 149 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
150 |
handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block |
|
151 |
[Pretty.str "The Quotient map theorem is not in the right form.", |
|
152 |
Pretty.brk 1, |
|
153 |
Pretty.str "The following term is not the Quotient predicate:", |
|
154 |
Pretty.brk 1, |
|
155 |
Syntax.pretty_term ctxt t])) |
|
156 |
in |
|
157 |
fastype_of abs |
|
158 |
end |
|
159 |
||
160 |
val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt |
|
59582 | 161 |
val rel_quot_thm_prop = Thm.prop_of rel_quot_thm_fixed |
47784 | 162 |
val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop |
163 |
val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; |
|
164 |
val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl |
|
165 |
val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] |
|
69089 | 166 |
val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) |
47784 | 167 |
rel_quot_thm_prems [] |
168 |
val extra_prem_tfrees = |
|
169 |
case subtract (op =) concl_tfrees prems_tfrees of |
|
170 |
[] => [] |
|
171 |
| extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:", |
|
69089 | 172 |
Pretty.brk 1] @ |
47784 | 173 |
((Pretty.commas o map (Pretty.str o quote)) extras) @ |
174 |
[Pretty.str "."])] |
|
69089 | 175 |
val errs = extra_prem_tfrees |
47784 | 176 |
in |
69089 | 177 |
if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] |
47784 | 178 |
@ (map Pretty.string_of errs))) |
179 |
end |
|
180 |
||
181 |
||
69089 | 182 |
fun add_quot_map rel_quot_thm ctxt = |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
183 |
let |
47784 | 184 |
val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt |
59582 | 185 |
val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
186 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
187 |
val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
188 |
val minfo = {rel_quot_thm = rel_quot_thm} |
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
189 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
190 |
Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt |
69089 | 191 |
end |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
192 |
|
58821 | 193 |
val _ = |
194 |
Theory.setup |
|
195 |
(Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map)) |
|
196 |
"declaration of the Quotient map theorem") |
|
47308 | 197 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
198 |
fun print_quot_maps ctxt = |
47308 | 199 |
let |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
200 |
fun prt_map (ty_name, {rel_quot_thm}) = |
47308 | 201 |
Pretty.block (separate (Pretty.brk 2) |
69089 | 202 |
[Pretty.str "type:", |
47308 | 203 |
Pretty.str ty_name, |
69089 | 204 |
Pretty.str "quot. theorem:", |
59582 | 205 |
Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)]) |
47308 | 206 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
207 |
map prt_map (Symtab.dest (get_quot_maps ctxt)) |
47308 | 208 |
|> Pretty.big_list "maps for type constructors:" |
209 |
|> Pretty.writeln |
|
210 |
end |
|
211 |
||
69089 | 212 |
|
47308 | 213 |
(* info about quotient types *) |
53651 | 214 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
215 |
fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
216 |
{pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
217 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
218 |
fun transform_quotient phi {quot_thm, pcr_info} = |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
219 |
{quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} |
47308 | 220 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
221 |
fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name |
47308 | 222 |
|
60235
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
223 |
fun lookup_quot_thm_quotients ctxt quot_thm = |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
224 |
let |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
225 |
val (_, qtyp) = quot_thm_rty_qty quot_thm |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
226 |
val qty_full_name = (fst o dest_Type) qtyp |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
227 |
fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm) |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
228 |
in |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
229 |
case lookup_quotients ctxt qty_full_name of |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
230 |
SOME quotient => if compare_data quotient then SOME quotient else NONE |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
231 |
| NONE => NONE |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
232 |
end |
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
233 |
|
69089 | 234 |
fun update_quotients type_name qinfo ctxt = |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
235 |
Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt |
47308 | 236 |
|
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
237 |
fun delete_quotients quot_thm ctxt = |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
238 |
let |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
239 |
val (_, qtyp) = quot_thm_rty_qty quot_thm |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
240 |
val qty_full_name = (fst o dest_Type) qtyp |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
241 |
in |
60235
3cab6f891c2f
reorder some steps in the construction to support mutual datatypes
kuncar
parents:
59936
diff
changeset
|
242 |
if is_some (lookup_quot_thm_quotients (Context.proof_of ctxt) quot_thm) |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
243 |
then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
244 |
else ctxt |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
245 |
end |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
246 |
|
47308 | 247 |
fun print_quotients ctxt = |
248 |
let |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
249 |
fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = |
47308 | 250 |
Pretty.block (separate (Pretty.brk 2) |
69089 | 251 |
[Pretty.str "type:", |
47308 | 252 |
Pretty.str qty_name, |
253 |
Pretty.str "quot. thm:", |
|
59582 | 254 |
Syntax.pretty_term ctxt (Thm.prop_of quot_thm), |
50227 | 255 |
Pretty.str "pcrel_def thm:", |
59582 | 256 |
option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcrel_def) pcr_info, |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
257 |
Pretty.str "pcr_cr_eq thm:", |
59582 | 258 |
option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o Thm.prop_of o #pcr_cr_eq) pcr_info]) |
47308 | 259 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
260 |
map prt_quot (Symtab.dest (get_quotients ctxt)) |
47308 | 261 |
|> Pretty.big_list "quotients:" |
262 |
|> Pretty.writeln |
|
263 |
end |
|
264 |
||
58821 | 265 |
val _ = |
266 |
Theory.setup |
|
267 |
(Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients)) |
|
268 |
"deletes the Quotient theorem") |
|
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
269 |
|
53651 | 270 |
(* data for restoring Transfer/Lifting context *) |
271 |
||
272 |
fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name |
|
273 |
||
69089 | 274 |
fun update_restore_data bundle_name restore_data ctxt = |
53651 | 275 |
Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt |
276 |
||
69089 | 277 |
fun init_restore_data bundle_name qinfo ctxt = |
53651 | 278 |
update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt |
279 |
||
280 |
fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt = |
|
281 |
case Symtab.lookup (get_restore_data' ctxt) bundle_name of |
|
69089 | 282 |
SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, |
53651 | 283 |
transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt |
284 |
| NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.") |
|
285 |
||
69089 | 286 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
287 |
(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *) |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
288 |
|
57961 | 289 |
fun get_relator_eq_onp_rules ctxt = |
290 |
map safe_mk_meta_eq (rev (Named_Theorems.get ctxt @{named_theorems relator_eq_onp})) |
|
47634
091bcd569441
hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents:
47308
diff
changeset
|
291 |
|
69089 | 292 |
|
51994 | 293 |
(* info about reflexivity rules *) |
294 |
||
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
295 |
fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) |
51994 | 296 |
|
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:
53754
diff
changeset
|
297 |
fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm)) |
51994 | 298 |
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule |
299 |
||
69089 | 300 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
301 |
(* info about relator distributivity theorems *) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
302 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
303 |
fun map_relator_distr_data' f1 f2 f3 f4 |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
304 |
{pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} = |
69089 | 305 |
{pos_mono_rule = f1 pos_mono_rule, |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
306 |
neg_mono_rule = f2 neg_mono_rule, |
69089 | 307 |
pos_distr_rules = f3 pos_distr_rules, |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
308 |
neg_distr_rules = f4 neg_distr_rules} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
309 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
310 |
fun map_pos_mono_rule f = map_relator_distr_data' f I I I |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
311 |
fun map_neg_mono_rule f = map_relator_distr_data' I f I I |
69089 | 312 |
fun map_pos_distr_rules f = map_relator_distr_data' I I f I |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
313 |
fun map_neg_distr_rules f = map_relator_distr_data' I I I f |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
314 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
315 |
fun introduce_polarities rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
316 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
317 |
val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT |
59582 | 318 |
val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (Thm.prems_of rule) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
319 |
val equal_prems = filter op= prems_pairs |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
320 |
val _ = |
69089 | 321 |
if null equal_prems then () |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
322 |
else error "The rule contains reflexive assumptions." |
69089 | 323 |
val concl_pairs = rule |
59582 | 324 |
|> Thm.concl_of |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
325 |
|> HOLogic.dest_Trueprop |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
326 |
|> dest_less_eq |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
327 |
|> apply2 (snd o strip_comb) |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
328 |
|> op ~~ |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
329 |
|> filter_out op = |
69089 | 330 |
|
331 |
val _ = if has_duplicates op= concl_pairs |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
332 |
then error "The rule contains duplicated variables in the conlusion." else () |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
333 |
|
69089 | 334 |
fun rewrite_prem prem_pair = |
51427
08bb00239652
proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm
parents:
51426
diff
changeset
|
335 |
if member op= concl_pairs prem_pair |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
336 |
then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})) |
51427
08bb00239652
proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm
parents:
51426
diff
changeset
|
337 |
else if member op= concl_pairs (swap prem_pair) |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
338 |
then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def})) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
339 |
else error "The rule contains a non-relevant assumption." |
69089 | 340 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
341 |
fun rewrite_prems [] = Conv.all_conv |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
342 |
| rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs) |
69089 | 343 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
344 |
val rewrite_prems_conv = rewrite_prems prems_pairs |
69089 | 345 |
val rewrite_concl_conv = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
346 |
Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
347 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
348 |
(Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
349 |
end |
69089 | 350 |
handle |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
351 |
TERM _ => error "The rule has a wrong format." |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
352 |
| CTERM _ => error "The rule has a wrong format." |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
353 |
|
69089 | 354 |
fun negate_mono_rule mono_rule = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
355 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
356 |
val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}]) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
357 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
358 |
Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
359 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
360 |
|
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:
53754
diff
changeset
|
361 |
fun add_reflexivity_rules mono_rule ctxt = |
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:
53754
diff
changeset
|
362 |
let |
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:
53754
diff
changeset
|
363 |
fun find_eq_rule thm ctxt = |
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:
53754
diff
changeset
|
364 |
let |
59582 | 365 |
val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o Thm.concl_of) thm; |
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:
53754
diff
changeset
|
366 |
val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs; |
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:
53754
diff
changeset
|
367 |
in |
69089 | 368 |
find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, |
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:
53754
diff
changeset
|
369 |
(fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules |
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:
53754
diff
changeset
|
370 |
end |
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:
53754
diff
changeset
|
371 |
|
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:
53754
diff
changeset
|
372 |
val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt); |
69089 | 373 |
val eq_rule = if is_some eq_rule then the eq_rule else error |
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:
53754
diff
changeset
|
374 |
"No corresponding rule that the relator preserves equality was found." |
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:
53754
diff
changeset
|
375 |
in |
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:
53754
diff
changeset
|
376 |
ctxt |
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:
53754
diff
changeset
|
377 |
|> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) |
69089 | 378 |
|> add_reflexivity_rule |
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:
53754
diff
changeset
|
379 |
(Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule])) |
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:
53754
diff
changeset
|
380 |
end |
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:
53754
diff
changeset
|
381 |
|
69089 | 382 |
fun add_mono_rule mono_rule ctxt = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
383 |
let |
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:
53754
diff
changeset
|
384 |
val pol_mono_rule = introduce_polarities mono_rule |
69089 | 385 |
val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o |
59582 | 386 |
dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) pol_mono_rule |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
387 |
in |
69091
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
388 |
if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
389 |
then |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
390 |
(if Context_Position.is_visible_generic ctxt then |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
391 |
warning ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
392 |
else (); ctxt) |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
393 |
else |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
394 |
let |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
395 |
val neg_mono_rule = negate_mono_rule pol_mono_rule |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
396 |
val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
397 |
pos_distr_rules = [], neg_distr_rules = []} |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
398 |
in |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
399 |
ctxt |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
400 |
|> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data))) |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
401 |
|> add_reflexivity_rules mono_rule |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
402 |
end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
403 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
404 |
|
69089 | 405 |
local |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
406 |
fun add_distr_rule update_entry distr_rule ctxt = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
407 |
let |
69089 | 408 |
val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o |
59582 | 409 |
dest_Const o head_of o HOLogic.dest_Trueprop o Thm.concl_of) distr_rule |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
410 |
in |
69089 | 411 |
if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then |
412 |
Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
413 |
ctxt |
69090 | 414 |
else error "The monotonicity rule is not defined." |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
415 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
416 |
|
69090 | 417 |
fun rewrite_concl_conv thm ctm = |
418 |
Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm |
|
419 |
handle CTERM _ => error "The rule has a wrong format." |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
420 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
421 |
in |
69089 | 422 |
fun add_pos_distr_rule distr_rule ctxt = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
423 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
424 |
val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule |
69089 | 425 |
fun update_entry distr_rule data = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
426 |
map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
427 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
428 |
add_distr_rule update_entry distr_rule ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
429 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
430 |
handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
431 |
|
69089 | 432 |
|
433 |
fun add_neg_distr_rule distr_rule ctxt = |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
434 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
435 |
val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule |
69089 | 436 |
fun update_entry distr_rule data = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
437 |
map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
438 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
439 |
add_distr_rule update_entry distr_rule ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
440 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
441 |
handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed." |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
442 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
443 |
|
69089 | 444 |
local |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
445 |
val eq_refl2 = sym RS @{thm eq_refl} |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
446 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
447 |
fun add_eq_distr_rule distr_rule ctxt = |
69089 | 448 |
let |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
449 |
val pos_distr_rule = @{thm eq_refl} OF [distr_rule] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
450 |
val neg_distr_rule = eq_refl2 OF [distr_rule] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
451 |
in |
69089 | 452 |
ctxt |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
453 |
|> add_pos_distr_rule pos_distr_rule |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
454 |
|> add_neg_distr_rule neg_distr_rule |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
455 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
456 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
457 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
458 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
459 |
fun sanity_check rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
460 |
let |
59582 | 461 |
val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule) |
462 |
val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of rule); |
|
56257 | 463 |
val (lhs, rhs) = |
464 |
(case concl of |
|
465 |
Const (@{const_name less_eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs => |
|
466 |
(lhs, rhs) |
|
467 |
| Const (@{const_name less_eq}, _) $ rhs $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) => |
|
468 |
(lhs, rhs) |
|
469 |
| Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs => |
|
470 |
(lhs, rhs) |
|
471 |
| _ => error "The rule has a wrong format.") |
|
69089 | 472 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
473 |
val lhs_vars = Term.add_vars lhs [] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
474 |
val rhs_vars = Term.add_vars rhs [] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
475 |
val assms_vars = fold Term.add_vars assms []; |
56257 | 476 |
val _ = |
477 |
if has_duplicates op= lhs_vars |
|
478 |
then error "Left-hand side has variable duplicates" else () |
|
479 |
val _ = |
|
69089 | 480 |
if subset op= (rhs_vars, lhs_vars) then () |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
481 |
else error "Extra variables in the right-hand side of the rule" |
56257 | 482 |
val _ = |
69089 | 483 |
if subset op= (assms_vars, lhs_vars) then () |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
484 |
else error "Extra variables in the assumptions of the rule" |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
485 |
val rhs_args = (snd o strip_comb) rhs; |
56257 | 486 |
fun check_comp t = |
487 |
(case t of |
|
488 |
Const (@{const_name relcompp}, _) $ Var _ $ Var _ => () |
|
489 |
| _ => error "There is an argument on the rhs that is not a composition.") |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
490 |
val _ = map check_comp rhs_args |
56257 | 491 |
in () end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
492 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
493 |
|
69089 | 494 |
fun add_distr_rule distr_rule ctxt = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
495 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
496 |
val _ = sanity_check distr_rule |
59582 | 497 |
val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of distr_rule) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
498 |
in |
56257 | 499 |
(case concl of |
500 |
Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ => |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
501 |
add_pos_distr_rule distr_rule ctxt |
56257 | 502 |
| Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) => |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
503 |
add_neg_distr_rule distr_rule ctxt |
56257 | 504 |
| Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ => |
505 |
add_eq_distr_rule distr_rule ctxt) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
506 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
507 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
508 |
|
69089 | 509 |
fun get_distr_rules_raw ctxt = Symtab.fold |
510 |
(fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
511 |
(get_relator_distr_data' ctxt) [] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
512 |
|
69089 | 513 |
fun get_mono_rules_raw ctxt = Symtab.fold |
514 |
(fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
515 |
(get_relator_distr_data' ctxt) [] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
516 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
517 |
val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
518 |
|
58821 | 519 |
val _ = |
520 |
Theory.setup |
|
521 |
(Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule)) |
|
69090 | 522 |
"declaration of relator's monotonicity" |
58821 | 523 |
#> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule)) |
524 |
"declaration of relator's distributivity over OO" |
|
525 |
#> Global_Theory.add_thms_dynamic |
|
526 |
(@{binding relator_distr_raw}, get_distr_rules_raw) |
|
527 |
#> Global_Theory.add_thms_dynamic |
|
528 |
(@{binding relator_mono_raw}, get_mono_rules_raw)) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
529 |
|
69089 | 530 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
531 |
(* no_code types *) |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
532 |
|
69089 | 533 |
fun add_no_code_type type_name ctxt = |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
534 |
Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt; |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
535 |
|
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
536 |
fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
537 |
|
69089 | 538 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
539 |
(* setup fixed eq_onp rules *) |
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55563
diff
changeset
|
540 |
|
57961 | 541 |
val _ = Context.>> |
542 |
(fold (Named_Theorems.add_thm @{named_theorems relator_eq_onp} o |
|
543 |
Transfer.prep_transfer_domain_thm @{context}) |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
544 |
@{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp}) |
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
|
545 |
|
69089 | 546 |
|
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
|
547 |
(* setup fixed reflexivity rules *) |
beb3b6851665
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents:
56257
diff
changeset
|
548 |
|
69089 | 549 |
val _ = Context.>> (fold add_reflexivity_rule |
67399 | 550 |
@{thms order_refl[of "(=)"] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq |
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
|
551 |
bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO}) |
55731
66df76dd2640
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents:
55563
diff
changeset
|
552 |
|
69089 | 553 |
|
47308 | 554 |
(* outer syntax commands *) |
555 |
||
556 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset
|
557 |
Outer_Syntax.command @{command_keyword print_quot_maps} "print quotient map functions" |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
558 |
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) |
47308 | 559 |
|
560 |
val _ = |
|
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59582
diff
changeset
|
561 |
Outer_Syntax.command @{command_keyword print_quotients} "print quotients" |
47308 | 562 |
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) |
563 |
||
53651 | 564 |
end |