author | wenzelm |
Wed, 10 May 2023 21:41:58 +0200 | |
changeset 78024 | 261b527f1b03 |
parent 77723 | b761c91c2447 |
child 78027 | 4bb7eb16b867 |
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 |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
45 |
val get_no_code_types : Proof.context -> Symset.T |
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, |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
85 |
no_code_types : Symset.T |
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, |
74152 | 90 |
reflexivity_rules = Thm.item_net, |
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, |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
93 |
no_code_types = Symset.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 |
fun merge |
69089 | 96 |
( { 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
|
97 |
restore_data = rd1, no_code_types = nct1 }, |
53651 | 98 |
{ 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
|
99 |
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
|
100 |
{ 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
|
101 |
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
|
102 |
reflexivity_rules = Item_Net.merge (rr1, rr2), |
53651 | 103 |
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
|
104 |
restore_data = Symtab.join join_restore_data (rd1, rd2), |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
105 |
no_code_types = Symset.merge (nct1, nct2) |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
106 |
} |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
107 |
) |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
108 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
109 |
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
|
110 |
{ 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
|
111 |
{ quot_maps = f1 quot_maps, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
112 |
quotients = f2 quotients, |
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
113 |
reflexivity_rules = f3 reflexivity_rules, |
53651 | 114 |
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
|
115 |
restore_data = f5 restore_data, |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
116 |
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
|
117 |
} |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
118 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
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
|
124 |
fun map_no_code_types f = map_data I I I I I f |
69089 | 125 |
|
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
126 |
val get_quot_maps' = #quot_maps o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
127 |
val get_quotients' = #quotients o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
128 |
val get_reflexivity_rules' = #reflexivity_rules o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
129 |
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
|
130 |
val get_restore_data' = #restore_data o Data.get |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
131 |
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
|
132 |
|
70320
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
133 |
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
|
134 |
val get_quotients = get_quotients' o Context.Proof |
59258a3192bf
misc tuning and clarification, notably wrt. flow of context;
wenzelm
parents:
69593
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
val get_no_code_types = get_no_code_types' o Context.Proof |
47308 | 138 |
|
69089 | 139 |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
140 |
(* info about Quotient map theorems *) |
47308 | 141 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
142 |
val lookup_quot_maps = Symtab.lookup o get_quot_maps |
47308 | 143 |
|
47784 | 144 |
fun quot_map_thm_sanity_check rel_quot_thm ctxt = |
145 |
let |
|
69089 | 146 |
fun quot_term_absT ctxt quot_term = |
147 |
let |
|
78024 | 148 |
val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop quot_term) |
47784 | 149 |
handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block |
150 |
[Pretty.str "The Quotient map theorem is not in the right form.", |
|
151 |
Pretty.brk 1, |
|
152 |
Pretty.str "The following term is not the Quotient predicate:", |
|
153 |
Pretty.brk 1, |
|
154 |
Syntax.pretty_term ctxt t])) |
|
155 |
in |
|
156 |
fastype_of abs |
|
157 |
end |
|
158 |
||
159 |
val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt |
|
59582 | 160 |
val rel_quot_thm_prop = Thm.prop_of rel_quot_thm_fixed |
47784 | 161 |
val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop |
162 |
val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop; |
|
163 |
val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl |
|
164 |
val concl_tfrees = Term.add_tfree_namesT (concl_absT) [] |
|
69089 | 165 |
val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) |
47784 | 166 |
rel_quot_thm_prems [] |
167 |
val extra_prem_tfrees = |
|
168 |
case subtract (op =) concl_tfrees prems_tfrees of |
|
169 |
[] => [] |
|
78024 | 170 |
| extras => |
171 |
[Pretty.block ([Pretty.str "Extra type variables in the premises:", |
|
172 |
Pretty.brk 1] @ |
|
173 |
Pretty.commas (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 |
78024 | 185 |
val rel_quot_thm_concl = Logic.strip_imp_concl (Thm.prop_of rel_quot_thm) |
186 |
val (_, abs, _, _) = dest_Quotient (HOLogic.dest_Trueprop rel_quot_thm_concl) |
|
187 |
val relatorT_name = fst (dest_Type (fst (dest_funT (fastype_of abs)))) |
|
70473 | 188 |
val minfo = {rel_quot_thm = Thm.trim_context rel_quot_thm} |
78024 | 189 |
in (Data.map o map_quot_maps) (Symtab.update (relatorT_name, minfo)) context end |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
190 |
|
58821 | 191 |
val _ = |
192 |
Theory.setup |
|
69593 | 193 |
(Attrib.setup \<^binding>\<open>quot_map\<close> (Scan.succeed (Thm.declaration_attribute add_quot_map)) |
58821 | 194 |
"declaration of the Quotient map theorem") |
47308 | 195 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
196 |
fun print_quot_maps ctxt = |
47308 | 197 |
let |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47634
diff
changeset
|
198 |
fun prt_map (ty_name, {rel_quot_thm}) = |
47308 | 199 |
Pretty.block (separate (Pretty.brk 2) |
69089 | 200 |
[Pretty.str "type:", |
47308 | 201 |
Pretty.str ty_name, |
69089 | 202 |
Pretty.str "quot. theorem:", |
59582 | 203 |
Syntax.pretty_term ctxt (Thm.prop_of rel_quot_thm)]) |
47308 | 204 |
in |
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
205 |
map prt_map (Symtab.dest (get_quot_maps ctxt)) |
47308 | 206 |
|> Pretty.big_list "maps for type constructors:" |
207 |
|> Pretty.writeln |
|
208 |
end |
|
209 |
||
69089 | 210 |
|
47308 | 211 |
(* info about quotient types *) |
53651 | 212 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
213 |
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
|
214 |
{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
|
215 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
216 |
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
|
217 |
{quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info} |
47308 | 218 |
|
70473 | 219 |
fun lookup_quotients ctxt type_name = |
220 |
Symtab.lookup (get_quotients ctxt) type_name |
|
221 |
|> Option.map (transform_quotient (Morphism.transfer_morphism' ctxt)) |
|
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 |
78024 | 226 |
val qty_full_name = fst (dest_Type qtyp) |
60235
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 = |
70473 | 235 |
let val qinfo' = transform_quotient Morphism.trim_context_morphism qinfo |
78024 | 236 |
in (Data.map o map_quotients) (Symtab.update (type_name, qinfo')) context end |
47308 | 237 |
|
69092 | 238 |
fun delete_quotients quot_thm context = |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
239 |
let |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
240 |
val (_, qtyp) = quot_thm_rty_qty quot_thm |
78024 | 241 |
val qty_full_name = fst (dest_Type qtyp) |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
242 |
in |
69092 | 243 |
if is_some (lookup_quot_thm_quotients (Context.proof_of context) quot_thm) |
78024 | 244 |
then (Data.map o map_quotients) (Symtab.delete qty_full_name) context |
69092 | 245 |
else context |
47951
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
246 |
end |
8c8a03765de7
quot_del attribute, it allows us to deregister quotient types
kuncar
parents:
47936
diff
changeset
|
247 |
|
47308 | 248 |
fun print_quotients ctxt = |
249 |
let |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
250 |
fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) = |
47308 | 251 |
Pretty.block (separate (Pretty.brk 2) |
70322 | 252 |
([Pretty.str "type:", Pretty.str qty_name, |
253 |
Pretty.str "quot thm:", Thm.pretty_thm ctxt quot_thm] @ |
|
254 |
(case pcr_info of |
|
255 |
NONE => [] |
|
256 |
| SOME {pcrel_def, pcr_cr_eq, ...} => |
|
257 |
[Pretty.str "pcrel_def thm:", Thm.pretty_thm ctxt pcrel_def, |
|
258 |
Pretty.str "pcr_cr_eq thm:", Thm.pretty_thm ctxt pcr_cr_eq]))) |
|
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 |
|
69593 | 267 |
(Attrib.setup \<^binding>\<open>quot_del\<close> (Scan.succeed (Thm.declaration_attribute delete_quotients)) |
58821 | 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 |
||
69092 | 274 |
fun update_restore_data bundle_name restore_data context = |
78024 | 275 |
(Data.map o map_restore_data) (Symtab.update (bundle_name, restore_data)) context |
53651 | 276 |
|
69092 | 277 |
fun init_restore_data bundle_name qinfo context = |
74152 | 278 |
update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.item_net } context |
53651 | 279 |
|
69092 | 280 |
fun add_transfer_rules_in_restore_data bundle_name transfer_rules context = |
281 |
(case Symtab.lookup (get_restore_data' context) bundle_name of |
|
282 |
SOME restore_data => |
|
283 |
update_restore_data bundle_name { quotient = #quotient restore_data, |
|
284 |
transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } context |
|
285 |
| NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")) |
|
53651 | 286 |
|
69089 | 287 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
288 |
(* 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
|
289 |
|
57961 | 290 |
fun get_relator_eq_onp_rules ctxt = |
69593 | 291 |
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
|
292 |
|
69089 | 293 |
|
51994 | 294 |
(* info about reflexivity rules *) |
295 |
||
70473 | 296 |
fun get_reflexivity_rules ctxt = |
297 |
Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt)) |
|
298 |
|> map (Thm.transfer' ctxt) |
|
51994 | 299 |
|
70473 | 300 |
fun add_reflexivity_rule thm = |
78024 | 301 |
(Data.map o map_reflexivity_rules) (Item_Net.update (Thm.trim_context thm)) |
70473 | 302 |
|
51994 | 303 |
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule |
304 |
||
69089 | 305 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
306 |
(* 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
|
307 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
308 |
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
|
309 |
{pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} = |
69089 | 310 |
{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
|
311 |
neg_mono_rule = f2 neg_mono_rule, |
69089 | 312 |
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
|
313 |
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
|
314 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
315 |
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
|
316 |
fun map_neg_mono_rule f = map_relator_distr_data' I f I I |
69089 | 317 |
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
|
318 |
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
|
319 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
320 |
fun introduce_polarities rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
321 |
let |
69593 | 322 |
val dest_less_eq = HOLogic.dest_bin \<^const_name>\<open>less_eq\<close> dummyT |
59582 | 323 |
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
|
324 |
val equal_prems = filter op= prems_pairs |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
325 |
val _ = |
69089 | 326 |
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
|
327 |
else error "The rule contains reflexive assumptions." |
69089 | 328 |
val concl_pairs = rule |
59582 | 329 |
|> Thm.concl_of |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
330 |
|> HOLogic.dest_Trueprop |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
331 |
|> dest_less_eq |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
332 |
|> apply2 (snd o strip_comb) |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
333 |
|> op ~~ |
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58893
diff
changeset
|
334 |
|> filter_out op = |
69089 | 335 |
|
336 |
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
|
337 |
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
|
338 |
|
69089 | 339 |
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
|
340 |
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
|
341 |
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
|
342 |
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
|
343 |
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
|
344 |
else error "The rule contains a non-relevant assumption." |
69089 | 345 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
346 |
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
|
347 |
| rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs) |
69089 | 348 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
349 |
val rewrite_prems_conv = rewrite_prems prems_pairs |
69089 | 350 |
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
|
351 |
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
|
352 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
353 |
(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
|
354 |
end |
69089 | 355 |
handle |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
356 |
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
|
357 |
| 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
|
358 |
|
69089 | 359 |
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
|
360 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
361 |
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
|
362 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
363 |
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
|
364 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
365 |
|
69092 | 366 |
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
|
367 |
let |
70473 | 368 |
val ctxt = Context.proof_of context |
369 |
val thy = Context.theory_of context |
|
370 |
||
371 |
fun find_eq_rule 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
|
372 |
let |
78024 | 373 |
val concl_rhs = hd (get_args 1 (HOLogic.dest_Trueprop (Thm.concl_of thm))) |
70473 | 374 |
val rules = Transfer.retrieve_relator_eq 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
|
375 |
in |
70473 | 376 |
find_first (fn th => Pattern.matches thy (concl_rhs, |
78024 | 377 |
fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of th))))) rules |
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
|
378 |
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
|
379 |
|
70473 | 380 |
val eq_rule = find_eq_rule mono_rule; |
69089 | 381 |
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
|
382 |
"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
|
383 |
in |
69092 | 384 |
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
|
385 |
|> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule])) |
69089 | 386 |
|> 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
|
387 |
(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
|
388 |
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
|
389 |
|
69092 | 390 |
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
|
391 |
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
|
392 |
val pol_mono_rule = introduce_polarities mono_rule |
78024 | 393 |
val mono_ruleT_name = |
394 |
fst (dest_Type (fst (relation_types (fst (relation_types |
|
395 |
(snd (dest_Const (head_of (HOLogic.dest_Trueprop (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
|
396 |
in |
69092 | 397 |
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
|
398 |
then |
69092 | 399 |
(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
|
400 |
warning ("Monotonicity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.") |
69092 | 401 |
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
|
402 |
else |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
403 |
let |
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
in |
69092 | 408 |
context |
78024 | 409 |
|> (Data.map o map_relator_distr_data) (Symtab.update (mono_ruleT_name, relator_distr_data)) |
69091
ce62fd14961a
permissive declaration attribute "relator_mono", e.g. relevant for Binomial-Heaps.BinomialHeap with -o export_theory;
wenzelm
parents:
69090
diff
changeset
|
410 |
|> 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
|
411 |
end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
412 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
413 |
|
69089 | 414 |
local |
69092 | 415 |
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
|
416 |
let |
78024 | 417 |
val distr_ruleT_name = |
418 |
fst (dest_Type (fst (relation_types (fst (relation_types |
|
419 |
(snd (dest_Const (head_of (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
|
420 |
in |
69092 | 421 |
if Symtab.defined (get_relator_distr_data' context) distr_ruleT_name then |
78024 | 422 |
(Data.map o map_relator_distr_data) |
423 |
(Symtab.map_entry distr_ruleT_name (update_entry distr_rule)) context |
|
69090 | 424 |
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
|
425 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
426 |
|
69090 | 427 |
fun rewrite_concl_conv thm ctm = |
428 |
Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm |
|
429 |
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
|
430 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
431 |
in |
69092 | 432 |
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
|
433 |
let |
78024 | 434 |
val distr_rule' = Conv.fconv_rule (rewrite_concl_conv @{thm POS_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_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
|
437 |
in |
78024 | 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 |
|
69092 | 442 |
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
|
443 |
let |
78024 | 444 |
val distr_rule' = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule |
69089 | 445 |
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
|
446 |
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
|
447 |
in |
78024 | 448 |
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
|
449 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
450 |
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
|
451 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
452 |
|
69089 | 453 |
local |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
454 |
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
|
455 |
in |
69092 | 456 |
fun add_eq_distr_rule distr_rule context = |
69089 | 457 |
let |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
458 |
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
|
459 |
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
|
460 |
in |
69092 | 461 |
context |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
462 |
|> 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
|
463 |
|> 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
|
464 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
465 |
end; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
466 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
467 |
local |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
468 |
fun sanity_check rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
469 |
let |
59582 | 470 |
val assms = map (perhaps (try HOLogic.dest_Trueprop)) (Thm.prems_of rule) |
78024 | 471 |
val concl = perhaps (try HOLogic.dest_Trueprop) (Thm.concl_of rule); |
56257 | 472 |
val (lhs, rhs) = |
473 |
(case concl of |
|
69593 | 474 |
Const (\<^const_name>\<open>less_eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => |
56257 | 475 |
(lhs, rhs) |
69593 | 476 |
| Const (\<^const_name>\<open>less_eq\<close>, _) $ rhs $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => |
56257 | 477 |
(lhs, rhs) |
69593 | 478 |
| Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (lhs as Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ rhs => |
56257 | 479 |
(lhs, rhs) |
480 |
| _ => error "The rule has a wrong format.") |
|
69089 | 481 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
482 |
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
|
483 |
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
|
484 |
val assms_vars = fold Term.add_vars assms []; |
56257 | 485 |
val _ = |
486 |
if has_duplicates op= lhs_vars |
|
487 |
then error "Left-hand side has variable duplicates" else () |
|
488 |
val _ = |
|
69089 | 489 |
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
|
490 |
else error "Extra variables in the right-hand side of the rule" |
56257 | 491 |
val _ = |
69089 | 492 |
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
|
493 |
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
|
494 |
val rhs_args = (snd o strip_comb) rhs; |
56257 | 495 |
fun check_comp t = |
496 |
(case t of |
|
69593 | 497 |
Const (\<^const_name>\<open>relcompp\<close>, _) $ Var _ $ Var _ => () |
56257 | 498 |
| _ => 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
|
499 |
val _ = map check_comp rhs_args |
56257 | 500 |
in () end |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
501 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
502 |
|
69092 | 503 |
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
|
504 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
505 |
val _ = sanity_check distr_rule |
78024 | 506 |
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
|
507 |
in |
56257 | 508 |
(case concl of |
69593 | 509 |
Const (\<^const_name>\<open>less_eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => |
69092 | 510 |
add_pos_distr_rule distr_rule context |
69593 | 511 |
| Const (\<^const_name>\<open>less_eq\<close>, _) $ _ $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) => |
69092 | 512 |
add_neg_distr_rule distr_rule context |
69593 | 513 |
| Const (\<^const_name>\<open>HOL.eq\<close>, _) $ (Const (\<^const_name>\<open>relcompp\<close>,_) $ _ $ _) $ _ => |
69092 | 514 |
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
|
515 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
516 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
517 |
|
70473 | 518 |
fun get_distr_rules_raw context = |
519 |
Symtab.fold (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => |
|
520 |
pos_distr_rules @ neg_distr_rules @ rules) |
|
69092 | 521 |
(get_relator_distr_data' context) [] |
70473 | 522 |
|> map (Thm.transfer'' context) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
523 |
|
70473 | 524 |
fun get_mono_rules_raw context = |
525 |
Symtab.fold (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => |
|
526 |
[pos_mono_rule, neg_mono_rule] @ rules) |
|
69092 | 527 |
(get_relator_distr_data' context) [] |
70473 | 528 |
|> map (Thm.transfer'' context) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50227
diff
changeset
|
529 |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51994
diff
changeset
|
530 |
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
|
531 |
|
58821 | 532 |
val _ = |
533 |
Theory.setup |
|
69593 | 534 |
(Attrib.setup \<^binding>\<open>relator_mono\<close> (Scan.succeed (Thm.declaration_attribute add_mono_rule)) |
69090 | 535 |
"declaration of relator's monotonicity" |
69593 | 536 |
#> Attrib.setup \<^binding>\<open>relator_distr\<close> (Scan.succeed (Thm.declaration_attribute add_distr_rule)) |
58821 | 537 |
"declaration of relator's distributivity over OO" |
538 |
#> Global_Theory.add_thms_dynamic |
|
69593 | 539 |
(\<^binding>\<open>relator_distr_raw\<close>, get_distr_rules_raw) |
58821 | 540 |
#> Global_Theory.add_thms_dynamic |
69593 | 541 |
(\<^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
|
542 |
|
69089 | 543 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
544 |
(* no_code types *) |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
545 |
|
69092 | 546 |
fun add_no_code_type type_name context = |
77723
b761c91c2447
performance tuning: prefer functor Set() over Table();
wenzelm
parents:
74561
diff
changeset
|
547 |
Data.map (map_no_code_types (Symset.insert type_name)) context; |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
548 |
|
78024 | 549 |
val is_no_code_type = Symset.member o get_no_code_types; |
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
56519
diff
changeset
|
550 |
|
69089 | 551 |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
552 |
(* 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
|
553 |
|
57961 | 554 |
val _ = Context.>> |
69593 | 555 |
(fold (Named_Theorems.add_thm \<^named_theorems>\<open>relator_eq_onp\<close> o |
556 |
Transfer.prep_transfer_domain_thm \<^context>) |
|
56519
c1048f5bbb45
more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents:
56518
diff
changeset
|
557 |
@{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
|
558 |
|
69089 | 559 |
|
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
|
560 |
(* 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
|
561 |
|
69089 | 562 |
val _ = Context.>> (fold add_reflexivity_rule |
67399 | 563 |
@{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
|
564 |
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
|
565 |
|
69089 | 566 |
|
47308 | 567 |
(* outer syntax commands *) |
568 |
||
569 |
val _ = |
|
69593 | 570 |
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
|
571 |
(Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of))) |
47308 | 572 |
|
573 |
val _ = |
|
69593 | 574 |
Outer_Syntax.command \<^command_keyword>\<open>print_quotients\<close> "print quotients" |
47308 | 575 |
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of))) |
576 |
||
53651 | 577 |
end |