author | wenzelm |
Tue, 04 Jun 2019 17:04:18 +0200 | |
changeset 70322 | 65b880d4efbb |
parent 70320 | 59258a3192bf |
child 70473 | 9179e7a98196 |
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 |
|
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
127 |
val get_quot_maps' = #quot_maps o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
128 |
val get_quotients' = #quotients o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
129 |
val get_reflexivity_rules' = #reflexivity_rules o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
130 |
val get_relator_distr_data' = #relator_distr_data o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
131 |
val get_restore_data' = #restore_data o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
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 |
|
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
134 |
val get_quot_maps = get_quot_maps' o Context.Proof |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
135 |
val get_quotients = get_quotients' o Context.Proof |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
136 |
val get_relator_distr_data = get_relator_distr_data' o Context.Proof |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
137 |
val get_restore_data = get_restore_data' o Context.Proof |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
138 |
val get_no_code_types = get_no_code_types' o Context.Proof |
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 |
||
69092 | 182 |
fun add_quot_map rel_quot_thm context = |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
183 |
let |
69092 | 184 |
val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) context |
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 |
69092 | 190 |
Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) context |
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 |
|
69593 | 195 |
(Attrib.setup \<^binding>\<open>quot_map\<close> (Scan.succeed (Thm.declaration_attribute add_quot_map)) |
58821 | 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 |
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
231 |
| NONE => NONE |
60235
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 |
|
69092 | 234 |
fun update_quotients type_name qinfo context = |
235 |
Data.map (map_quotients (Symtab.update (type_name, qinfo))) context |
|
47308 | 236 |
|
69092 | 237 |
fun delete_quotients quot_thm context = |
47951
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 |
69092 | 242 |
if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm) |
243 |
then Data.map (map_quotients (Symtab.delete qty_full_name)) context |
|
244 |
else context |
|
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) |
70322 | 251 |
([Pretty.str "type:", Pretty.str qty_name, |
252 |
Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @ |
|
253 |
(case pcr_info of |
|
254 |
NONE => [] |
|
255 |
| SOME {pcrel_def, pcr_cr_eq, ...} => |
|
256 |
[Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def, |
|
257 |
Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq]))) |
|
47308 | 258 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
259 |
map prt_quot (Symtab.dest (get_quotients ctxt)) |
47308 | 260 |
|> Pretty.big_list "quotients:" |
261 |
|> Pretty.writeln |
|
262 |
end |
|
263 |
||
58821 | 264 |
val _ = |
265 |
Theory.setup |
|
69593 | 266 |
(Attrib.setup \<^binding>\<open>quot_del\<close> (Scan.succeed (Thm.declaration_attribute delete_quotients)) |
58821 | 267 |
"deletes the Quotient theorem") |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
268 |
|
53651 | 269 |
(* data for restoring Transfer/Lifting context *) |
270 |
||
271 |
fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name |
|
272 |
||
69092 | 273 |
fun update_restore_data bundle_name restore_data context = |
274 |
Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) context |
|
53651 | 275 |
|
69092 | 276 |
fun init_restore_data bundle_name qinfo context = |
277 |
update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } context |
|
53651 | 278 |
|
69092 | 279 |
fun add_transfer_rules_in_restore_data bundle_name transfer_rules context = |
280 |
(case Symtab.lookup (get_restore_data' context) bundle_name of |
|
281 |
SOME restore_data => |
|
282 |
update_restore_data bundle_name { quotient = #quotient restore_data, |
|
283 |
transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } context |
|
284 |
| NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")) |
|
53651 | 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 = |
69593 | 290 |
map safe_mk_meta_eq (rev (Named_Theorems.get ctxt \<^named_theorems>\<open>relator_eq_onp\<close>)) |
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 |
||
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
295 |
val get_reflexivity_rules = Item_Net.content o get_reflexivity_rules' o Context.Proof |
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 |
69593 | 317 |
val dest_less_eq = HOLogic.dest_bin \<^const_name>\<open>less_eq\<close> 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 |
|
69092 | 361 |
fun add_reflexivity_rules mono_rule context = |
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
|
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 |
|
69092 | 372 |
val eq_rule = find_eq_rule mono_rule (Context.proof_of context); |
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 |
69092 | 376 |
context |
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
|
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 |
|
69092 | 382 |
fun add_mono_rule mono_rule context = |
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 |
69092 | 388 |
if Symtab.defined (get_relator_distr_data' context) mono_ruleT_name |
69091
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
389 |
then |
69092 | 390 |
(if Context_Position.is_visible_generic context then |
69091
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.") |
69092 | 392 |
else (); context) |
69091
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 |
69092 | 399 |
context |
69091
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 |
69092 | 406 |
fun add_distr_rule update_entry distr_rule context = |
51374
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 |
69092 | 411 |
if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then |
69089 | 412 |
Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) |
69092 | 413 |
context |
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 |
69092 | 422 |
fun add_pos_distr_rule distr_rule context = |
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 |
69092 | 428 |
add_distr_rule update_entry distr_rule context |
51374
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 |
|
69092 | 432 |
fun add_neg_distr_rule distr_rule context = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
433 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
434 |
val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule |
69089 | 435 |
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
|
436 |
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
|
437 |
in |
69092 | 438 |
add_distr_rule update_entry distr_rule context |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
439 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
440 |
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
|
441 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
442 |
|
69089 | 443 |
local |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
444 |
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
|
445 |
in |
69092 | 446 |
fun add_eq_distr_rule distr_rule context = |
69089 | 447 |
let |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
448 |
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
|
449 |
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
|
450 |
in |
69092 | 451 |
context |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
452 |
|> 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
|
453 |
|> 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
|
454 |
end |
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 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
457 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
458 |
fun sanity_check rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
459 |
let |
59582 | 460 |
val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule) |
461 |
val concl = (perhaps (try HOLogic.dest_Trueprop)) (Thm.concl_of rule); |
|
56257 | 462 |
val (lhs, rhs) = |
463 |
(case concl of |
|
69593 | 464 |
Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => |
56257 | 465 |
(lhs, rhs) |
69593 | 466 |
| Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => |
56257 | 467 |
(lhs, rhs) |
69593 | 468 |
| Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => |
56257 | 469 |
(lhs, rhs) |
470 |
| _ => error "The rule has a wrong format.") |
|
69089 | 471 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
472 |
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
|
473 |
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
|
474 |
val assms_vars = fold Term.add_vars assms []; |
56257 | 475 |
val _ = |
476 |
if has_duplicates op= lhs_vars |
|
477 |
then error "Left-hand side has variable duplicates" else () |
|
478 |
val _ = |
|
69089 | 479 |
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
|
480 |
else error "Extra variables in the right-hand side of the rule" |
56257 | 481 |
val _ = |
69089 | 482 |
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
|
483 |
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
|
484 |
val rhs_args = (snd o strip_comb) rhs; |
56257 | 485 |
fun check_comp t = |
486 |
(case t of |
|
69593 | 487 |
Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => () |
56257 | 488 |
| _ => 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
|
489 |
val _ = map check_comp rhs_args |
56257 | 490 |
in () end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
491 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
492 |
|
69092 | 493 |
fun add_distr_rule distr_rule context = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
494 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
495 |
val _ = sanity_check distr_rule |
59582 | 496 |
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
|
497 |
in |
56257 | 498 |
(case concl of |
69593 | 499 |
Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => |
69092 | 500 |
add_pos_distr_rule distr_rule context |
69593 | 501 |
| Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => |
69092 | 502 |
add_neg_distr_rule distr_rule context |
69593 | 503 |
| Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => |
69092 | 504 |
add_eq_distr_rule distr_rule context) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
505 |
end |
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 |
|
69092 | 508 |
fun get_distr_rules_raw context = Symtab.fold |
69089 | 509 |
(fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) |
69092 | 510 |
(get_relator_distr_data' context) [] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
511 |
|
69092 | 512 |
fun get_mono_rules_raw context = Symtab.fold |
69089 | 513 |
(fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) |
69092 | 514 |
(get_relator_distr_data' context) [] |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
515 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
516 |
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
|
517 |
|
58821 | 518 |
val _ = |
519 |
Theory.setup |
|
69593 | 520 |
(Attrib.setup \<^binding>\<open>relator_mono\<close> (Scan.succeed (Thm.declaration_attribute add_mono_rule)) |
69090 | 521 |
"declaration of relator's monotonicity" |
69593 | 522 |
#> Attrib.setup \<^binding>\<open>relator_distr\<close> (Scan.succeed (Thm.declaration_attribute add_distr_rule)) |
58821 | 523 |
"declaration of relator's distributivity over OO" |
524 |
#> Global_Theory.add_thms_dynamic |
|
69593 | 525 |
(\<^binding>\<open>relator_distr_raw\<close>, get_distr_rules_raw) |
58821 | 526 |
#> Global_Theory.add_thms_dynamic |
69593 | 527 |
(\<^binding>\<open>relator_mono_raw\<close>, 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
|
528 |
|
69089 | 529 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
530 |
(* no_code types *) |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
531 |
|
69092 | 532 |
fun add_no_code_type type_name context = |
533 |
Data.map (map_no_code_types (Symtab.update (type_name, ()))) context; |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
534 |
|
69092 | 535 |
fun is_no_code_type context type_name = (Symtab.defined o get_no_code_types) context type_name |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
536 |
|
69089 | 537 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
538 |
(* 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
|
539 |
|
57961 | 540 |
val _ = Context.>> |
69593 | 541 |
(fold (Named_Theorems.add_thm \<^named_theorems>\<open>relator_eq_onp\<close> o |
542 |
Transfer.prep_transfer_domain_thm \<^context>) |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
543 |
@{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
|
544 |
|
69089 | 545 |
|
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
|
546 |
(* 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
|
547 |
|
69089 | 548 |
val _ = Context.>> (fold add_reflexivity_rule |
67399 | 549 |
@{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
|
550 |
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
|
551 |
|
69089 | 552 |
|
47308 | 553 |
(* outer syntax commands *) |
554 |
||
555 |
val _ = |
|
69593 | 556 |
Outer_Syntax.command \<^command_keyword>\<open>print_quot_maps\<close> "print quotient map functions" |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
557 |
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) |
47308 | 558 |
|
559 |
val _ = |
|
69593 | 560 |
Outer_Syntax.command \<^command_keyword>\<open>print_quotients\<close> "print quotients" |
47308 | 561 |
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) |
562 |
||
53651 | 563 |
end |