author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 60801 | 7664e0916eec |
child 70320 | 59258a3192bf |
permissions | -rw-r--r-- |
47308 | 1 |
(* Title: HOL/Tools/Lifting/lifting_term.ML |
2 |
Author: Ondrej Kuncar |
|
3 |
||
4 |
Proves Quotient theorem. |
|
5 |
*) |
|
6 |
||
7 |
signature LIFTING_TERM = |
|
8 |
sig |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
9 |
exception QUOT_THM of typ * typ * Pretty.T |
50227 | 10 |
exception PARAM_QUOT_THM of typ * Pretty.T |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
11 |
exception MERGE_TRANSFER_REL of Pretty.T |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
12 |
exception CHECK_RTY of typ * typ |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
13 |
|
60217 | 14 |
type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, |
15 |
comp_lift: typ -> thm * 'a -> thm * 'a } |
|
16 |
||
60222 | 17 |
type quotients = Lifting_Info.quotient Symtab.table |
18 |
||
60217 | 19 |
val force_qty_type: Proof.context -> typ -> thm -> thm |
20 |
||
60222 | 21 |
val prove_schematic_quot_thm: 'a fold_quot_thm -> quotients -> Proof.context -> |
22 |
typ * typ -> 'a -> thm * 'a |
|
60217 | 23 |
|
57663
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
55731
diff
changeset
|
24 |
val instantiate_rtys: Proof.context -> typ * typ -> typ * typ |
b590fcd03a4a
store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents:
55731
diff
changeset
|
25 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
26 |
val prove_quot_thm: Proof.context -> typ * typ -> thm |
47308 | 27 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
28 |
val abs_fun: Proof.context -> typ * typ -> term |
47308 | 29 |
|
30 |
val equiv_relation: Proof.context -> typ * typ -> term |
|
50227 | 31 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
32 |
val prove_param_quot_thm: Proof.context -> typ -> thm * (typ * thm) list * Proof.context |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
33 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
34 |
val generate_parametrized_relator: Proof.context -> typ -> term * term list |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
35 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
36 |
val merge_transfer_relations: Proof.context -> cterm -> thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
37 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
38 |
val parametrize_transfer_rule: Proof.context -> thm -> thm |
47308 | 39 |
end |
40 |
||
41 |
structure Lifting_Term: LIFTING_TERM = |
|
42 |
struct |
|
47698 | 43 |
open Lifting_Util |
44 |
||
45 |
infix 0 MRSL |
|
46 |
||
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
47 |
exception QUOT_THM_INTERNAL of Pretty.T |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
48 |
exception QUOT_THM of typ * typ * Pretty.T |
50227 | 49 |
exception PARAM_QUOT_THM of typ * Pretty.T |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
50 |
exception MERGE_TRANSFER_REL of Pretty.T |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
51 |
exception CHECK_RTY of typ * typ |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
52 |
|
60222 | 53 |
type quotients = Lifting_Info.quotient Symtab.table |
54 |
||
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
55 |
fun match ctxt err ty_pat ty = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
56 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
57 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
58 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
59 |
Sign.typ_match thy (ty_pat, ty) Vartab.empty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
60 |
handle Type.TYPE_MATCH => err ctxt ty_pat ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
61 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
62 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
63 |
fun equiv_match_err ctxt ty_pat ty = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
64 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
65 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
66 |
val ty_str = Syntax.string_of_typ ctxt ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
67 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
68 |
raise QUOT_THM_INTERNAL (Pretty.block |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
69 |
[Pretty.str ("The quotient type " ^ quote ty_str), |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
70 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
71 |
Pretty.str ("and the quotient type pattern " ^ quote ty_pat_str), |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
72 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
73 |
Pretty.str "don't match."]) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
74 |
end |
47308 | 75 |
|
60239 | 76 |
fun get_quot_data (quotients: quotients) s = |
60222 | 77 |
case Symtab.lookup quotients s of |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
78 |
SOME qdata => qdata |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
79 |
| NONE => raise QUOT_THM_INTERNAL (Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
80 |
[Pretty.str ("No quotient type " ^ quote s), |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
81 |
Pretty.brk 1, |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
82 |
Pretty.str "found."]) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
83 |
|
60222 | 84 |
fun get_quot_thm quotients ctxt s = |
47308 | 85 |
let |
86 |
val thy = Proof_Context.theory_of ctxt |
|
87 |
in |
|
60222 | 88 |
Thm.transfer thy (#quot_thm (get_quot_data quotients s)) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
89 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
90 |
|
60222 | 91 |
fun has_pcrel_info quotients s = is_some (#pcr_info (get_quot_data quotients s)) |
55455
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
92 |
|
60222 | 93 |
fun get_pcrel_info quotients s = |
94 |
case #pcr_info (get_quot_data quotients s) of |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51374
diff
changeset
|
95 |
SOME pcr_info => pcr_info |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
96 |
| NONE => raise QUOT_THM_INTERNAL (Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
97 |
[Pretty.str ("No parametrized correspondce relation for " ^ quote s), |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
98 |
Pretty.brk 1, |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
99 |
Pretty.str "found."]) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
100 |
|
60222 | 101 |
fun get_pcrel_def quotients ctxt s = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
102 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
103 |
val thy = Proof_Context.theory_of ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
104 |
in |
60222 | 105 |
Thm.transfer thy (#pcrel_def (get_pcrel_info quotients s)) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
106 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
107 |
|
60222 | 108 |
fun get_pcr_cr_eq quotients ctxt s = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
109 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
110 |
val thy = Proof_Context.theory_of ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
111 |
in |
60222 | 112 |
Thm.transfer thy (#pcr_cr_eq (get_pcrel_info quotients s)) |
47308 | 113 |
end |
114 |
||
115 |
fun get_rel_quot_thm ctxt s = |
|
116 |
let |
|
117 |
val thy = Proof_Context.theory_of ctxt |
|
118 |
in |
|
53219
ca237b9e4542
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents:
51374
diff
changeset
|
119 |
(case Lifting_Info.lookup_quot_maps ctxt s of |
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47698
diff
changeset
|
120 |
SOME map_data => Thm.transfer thy (#rel_quot_thm map_data) |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
121 |
| NONE => raise QUOT_THM_INTERNAL (Pretty.block |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
122 |
[Pretty.str ("No relator for the type " ^ quote s), |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
123 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
124 |
Pretty.str "found."])) |
47308 | 125 |
end |
126 |
||
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
127 |
fun get_rel_distr_rules ctxt s tm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
128 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
129 |
val thy = Proof_Context.theory_of ctxt |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
130 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
131 |
(case Lifting_Info.lookup_relator_distr_data ctxt s of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
132 |
SOME rel_distr_thm => ( |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
133 |
case tm of |
69593 | 134 |
Const (\<^const_name>\<open>POS\<close>, _) => map (Thm.transfer thy) (#pos_distr_rules rel_distr_thm) |
135 |
| Const (\<^const_name>\<open>NEG\<close>, _) => map (Thm.transfer thy) (#neg_distr_rules rel_distr_thm) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
136 |
) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
137 |
| NONE => raise QUOT_THM_INTERNAL (Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
138 |
[Pretty.str ("No relator distr. data for the type " ^ quote s), |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
139 |
Pretty.brk 1, |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
140 |
Pretty.str "found."])) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
141 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
142 |
|
59848 | 143 |
fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient}) |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
144 |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
145 |
fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
146 |
case try (get_rel_quot_thm ctxt) type_name of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
147 |
NONE => rty_Tvars ~~ qty_Tvars |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
148 |
| SOME rel_quot_thm => |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
149 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
150 |
fun quot_term_absT quot_term = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
151 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
152 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
153 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
154 |
fastype_of abs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
155 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
156 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
157 |
fun equiv_univ_err ctxt ty_pat ty = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
158 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
159 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
160 |
val ty_str = Syntax.string_of_typ ctxt ty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
161 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
162 |
raise QUOT_THM_INTERNAL (Pretty.block |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
163 |
[Pretty.str ("The type " ^ quote ty_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
164 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
165 |
Pretty.str ("and the relator type pattern " ^ quote ty_pat_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
166 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
167 |
Pretty.str "don't unify."]) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
168 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
169 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
170 |
fun raw_match (TVar (v, S), T) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
171 |
(case Vartab.defined subs v of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
172 |
false => Vartab.update_new (v, (S, T)) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
173 |
| true => subs) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
174 |
| raw_match (Type (_, Ts), Type (_, Us)) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
175 |
raw_matches (Ts, Us) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
176 |
| raw_match _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
177 |
and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
178 |
| raw_matches _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
179 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
180 |
val rty = Type (type_name, rty_Tvars) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
181 |
val qty = Type (type_name, qty_Tvars) |
59582 | 182 |
val rel_quot_thm_concl = (Logic.strip_imp_concl o Thm.prop_of) rel_quot_thm |
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
183 |
val schematic_rel_absT = quot_term_absT rel_quot_thm_concl; |
54946
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
184 |
val thy = Proof_Context.theory_of ctxt |
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
185 |
val absT = rty --> qty |
54946
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
186 |
val schematic_absT = |
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
187 |
absT |
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
188 |
|> Logic.type_map (singleton (Variable.polymorphic ctxt)) |
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
189 |
|> Logic.incr_tvar (maxidx_of_typ schematic_rel_absT + 1) |
1c000fa0fdf5
ensure that schematic type variables are fresh in rty
kuncar
parents:
54945
diff
changeset
|
190 |
(* because absT can already contain schematic variables from rty patterns *) |
47853 | 191 |
val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT] |
192 |
val _ = Sign.typ_unify thy (schematic_rel_absT, schematic_absT) (Vartab.empty,maxidx) |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
193 |
handle Type.TUNIFY => equiv_univ_err ctxt schematic_rel_absT schematic_absT |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
194 |
val subs = raw_match (schematic_rel_absT, absT) Vartab.empty |
59582 | 195 |
val rel_quot_thm_prems = (Logic.strip_imp_prems o Thm.prop_of) rel_quot_thm |
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
196 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
197 |
map (dest_funT o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
198 |
Envir.subst_type subs o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
199 |
quot_term_absT) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
200 |
rel_quot_thm_prems |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
201 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
202 |
|
60222 | 203 |
fun gen_rty_is_TVar quotients ctxt qty = qty |> Tname |> get_quot_thm quotients ctxt |> |
204 |
quot_thm_rty_qty |> fst |> is_TVar |
|
55454 | 205 |
|
60222 | 206 |
fun gen_instantiate_rtys quotients ctxt (rty, (qty as Type (qty_name, _))) = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
207 |
let |
60222 | 208 |
val quot_thm = get_quot_thm quotients ctxt qty_name |
55454 | 209 |
val (rty_pat, qty_pat) = quot_thm_rty_qty quot_thm |
210 |
||
54945
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
211 |
fun inst_rty (Type (s, tys), Type (s', tys')) = |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
212 |
if s = s' then Type (s', map inst_rty (tys ~~ tys')) |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
213 |
else raise QUOT_THM_INTERNAL (Pretty.block |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
214 |
[Pretty.str "The type", |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
215 |
Pretty.brk 1, |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
216 |
Syntax.pretty_typ ctxt rty, |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
217 |
Pretty.brk 1, |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
218 |
Pretty.str ("is not a raw type for the quotient type " ^ quote qty_name ^ ";"), |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
219 |
Pretty.brk 1, |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
220 |
Pretty.str "the correct raw type must be an instance of", |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
221 |
Pretty.brk 1, |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
222 |
Syntax.pretty_typ ctxt rty_pat]) |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
223 |
| inst_rty (t as Type (_, _), TFree _) = t |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
224 |
| inst_rty ((TVar _), rty) = rty |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
225 |
| inst_rty ((TFree _), rty) = rty |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
226 |
| inst_rty (_, _) = error "check_raw_types: we should not be here" |
dcd4dcf26395
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
kuncar
parents:
54335
diff
changeset
|
227 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
228 |
val qtyenv = match ctxt equiv_match_err qty_pat qty |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
229 |
in |
55454 | 230 |
(inst_rty (rty_pat, rty), Envir.subst_type qtyenv rty_pat) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
231 |
end |
60222 | 232 |
| gen_instantiate_rtys _ _ _ = error "gen_instantiate_rtys: not Type" |
233 |
||
234 |
fun instantiate_rtys ctxt (rty, qty) = |
|
235 |
gen_instantiate_rtys (Lifting_Info.get_quotients ctxt) ctxt (rty, qty) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
236 |
|
60217 | 237 |
type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, |
238 |
comp_lift: typ -> thm * 'a -> thm * 'a } |
|
239 |
||
60239 | 240 |
fun prove_schematic_quot_thm (actions: 'a fold_quot_thm) quotients ctxt (rty, qty) fold_val = |
55454 | 241 |
let |
242 |
fun lifting_step (rty, qty) = |
|
243 |
let |
|
60222 | 244 |
val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty) |
245 |
val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) |
|
55454 | 246 |
else (Targs rty', Targs rtyq) |
60217 | 247 |
val (args, fold_val) = |
60222 | 248 |
fold_map (prove_schematic_quot_thm actions quotients ctxt) (rty's ~~ rtyqs) fold_val |
55454 | 249 |
in |
250 |
if forall is_id_quot args |
|
251 |
then |
|
60217 | 252 |
let |
60222 | 253 |
val quot_thm = get_quot_thm quotients ctxt (Tname qty) |
60217 | 254 |
in |
255 |
#lift actions qty (quot_thm, fold_val) |
|
256 |
end |
|
55454 | 257 |
else |
258 |
let |
|
60222 | 259 |
val quot_thm = get_quot_thm quotients ctxt (Tname qty) |
260 |
val rel_quot_thm = if gen_rty_is_TVar quotients ctxt qty then the_single args else |
|
55454 | 261 |
args MRSL (get_rel_quot_thm ctxt (Tname rty)) |
60217 | 262 |
val comp_quot_thm = [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} |
55454 | 263 |
in |
60217 | 264 |
#comp_lift actions qty (comp_quot_thm, fold_val) |
55454 | 265 |
end |
266 |
end |
|
267 |
in |
|
268 |
(case (rty, qty) of |
|
269 |
(Type (s, tys), Type (s', tys')) => |
|
270 |
if s = s' |
|
271 |
then |
|
272 |
let |
|
60217 | 273 |
val (args, fold_val) = |
60222 | 274 |
fold_map (prove_schematic_quot_thm actions quotients ctxt) |
275 |
(zip_Tvars ctxt s tys tys') fold_val |
|
55454 | 276 |
in |
277 |
if forall is_id_quot args |
|
278 |
then |
|
60217 | 279 |
(@{thm identity_quotient}, fold_val) |
55454 | 280 |
else |
60217 | 281 |
let |
282 |
val quot_thm = args MRSL (get_rel_quot_thm ctxt s) |
|
283 |
in |
|
284 |
#constr actions qty (quot_thm, fold_val) |
|
285 |
end |
|
55454 | 286 |
end |
287 |
else |
|
288 |
lifting_step (rty, qty) |
|
289 |
| (_, Type (s', tys')) => |
|
60222 | 290 |
(case try (get_quot_thm quotients ctxt) s' of |
55454 | 291 |
SOME quot_thm => |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
292 |
let |
55454 | 293 |
val rty_pat = (fst o quot_thm_rty_qty) quot_thm |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
294 |
in |
55454 | 295 |
lifting_step (rty_pat, qty) |
296 |
end |
|
297 |
| NONE => |
|
298 |
let |
|
299 |
val rty_pat = Type (s', map (fn _ => TFree ("a",[])) tys') |
|
300 |
in |
|
60222 | 301 |
prove_schematic_quot_thm actions quotients ctxt (rty_pat, qty) fold_val |
55454 | 302 |
end) |
60217 | 303 |
| _ => (@{thm identity_quotient}, fold_val) |
304 |
) |
|
55454 | 305 |
end |
306 |
handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg) |
|
47308 | 307 |
|
59630 | 308 |
fun force_qty_type ctxt qty quot_thm = |
47308 | 309 |
let |
59630 | 310 |
val thy = Proof_Context.theory_of ctxt |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
311 |
val (_, qty_schematic) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
312 |
val match_env = Sign.typ_match thy (qty_schematic, qty) Vartab.empty |
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60239
diff
changeset
|
313 |
fun prep_ty (x, (S, ty)) = ((x, S), Thm.ctyp_of ctxt ty) |
59630 | 314 |
val ty_inst = Vartab.fold (cons o prep_ty) match_env [] |
47308 | 315 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
316 |
Thm.instantiate (ty_inst, []) quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
317 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
318 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
319 |
fun check_rty_type ctxt rty quot_thm = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
320 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
321 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
322 |
val (rty_forced, _) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
323 |
val rty_schematic = Logic.type_map (singleton (Variable.polymorphic ctxt)) rty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
324 |
val _ = Sign.typ_match thy (rty_schematic, rty_forced) Vartab.empty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
325 |
handle Type.TYPE_MATCH => raise CHECK_RTY (rty_schematic, rty_forced) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
326 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
327 |
() |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
328 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
329 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
330 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
331 |
The function tries to prove that rty and qty form a quotient. |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
332 |
|
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
333 |
Returns: Quotient theorem; an abstract type of the theorem is exactly |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
334 |
qty, a representation type of the theorem is an instance of rty in general. |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
335 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
336 |
|
60217 | 337 |
|
338 |
local |
|
339 |
val id_actions = { constr = K I, lift = K I, comp_lift = K I } |
|
340 |
in |
|
341 |
fun prove_quot_thm ctxt (rty, qty) = |
|
342 |
let |
|
60222 | 343 |
val quotients = Lifting_Info.get_quotients ctxt |
344 |
val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) () |
|
345 |
val quot_thm = force_qty_type ctxt qty schematic_quot_thm |
|
60217 | 346 |
val _ = check_rty_type ctxt rty quot_thm |
347 |
in |
|
348 |
quot_thm |
|
349 |
end |
|
350 |
end |
|
47308 | 351 |
|
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
352 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
353 |
Computes the composed abstraction function for rty and qty. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
354 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
355 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
356 |
fun abs_fun ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
357 |
quot_thm_abs (prove_quot_thm ctxt (rty, qty)) |
47350 | 358 |
|
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
359 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
360 |
Computes the composed equivalence relation for rty and qty. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
361 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
362 |
|
47308 | 363 |
fun equiv_relation ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
364 |
quot_thm_rel (prove_quot_thm ctxt (rty, qty)) |
47308 | 365 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
366 |
val get_fresh_Q_t = |
50227 | 367 |
let |
69593 | 368 |
val Q_t = \<^term>\<open>Trueprop (Quotient R Abs Rep T)\<close> |
50227 | 369 |
val frees_Q_t = Term.add_free_names Q_t [] |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
370 |
val tfrees_Q_t = rev (Term.add_tfree_names Q_t []) |
50227 | 371 |
in |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
372 |
fn ctxt => |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
373 |
let |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
374 |
fun rename_free_var tab (Free (name, typ)) = Free (the_default name (AList.lookup op= tab name),typ) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
375 |
| rename_free_var _ t = t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
376 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
377 |
fun rename_free_vars tab = map_aterms (rename_free_var tab) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
378 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
379 |
fun rename_free_tvars tab = |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
380 |
map_types (map_type_tfree (fn (name, sort) => TFree (the_default name (AList.lookup op= tab name), sort))) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
381 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
382 |
val (new_frees_Q_t, ctxt) = Variable.variant_fixes frees_Q_t ctxt |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
383 |
val tab_frees = frees_Q_t ~~ new_frees_Q_t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
384 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
385 |
val (new_tfrees_Q_t, ctxt) = Variable.invent_types (replicate (length tfrees_Q_t) []) ctxt |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
386 |
val tab_tfrees = tfrees_Q_t ~~ (fst o split_list) new_tfrees_Q_t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
387 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
388 |
val renamed_Q_t = rename_free_vars tab_frees Q_t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
389 |
val renamed_Q_t = rename_free_tvars tab_tfrees renamed_Q_t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
390 |
in |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
391 |
(renamed_Q_t, ctxt) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
392 |
end |
50227 | 393 |
end |
394 |
||
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
395 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
396 |
For the given type, it proves a composed Quotient map theorem, where for each type variable |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
397 |
extra Quotient assumption is generated. E.g., for 'a list it generates exactly |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
398 |
the Quotient map theorem for the list type. The function generalizes this for the whole |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
399 |
type universe. New fresh variables in the assumptions are fixed in the returned context. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
400 |
|
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
401 |
Returns: the composed Quotient map theorem and list mapping each type variable in ty |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
402 |
to the corresponding assumption in the returned theorem. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
403 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
404 |
|
50227 | 405 |
fun prove_param_quot_thm ctxt ty = |
406 |
let |
|
407 |
fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = |
|
408 |
if null tys |
|
409 |
then |
|
410 |
let |
|
59582 | 411 |
val instantiated_id_quot_thm = |
60801 | 412 |
Thm.instantiate' [SOME (Thm.ctyp_of ctxt ty)] [] @{thm identity_quotient} |
50227 | 413 |
in |
414 |
(instantiated_id_quot_thm, (table, ctxt)) |
|
415 |
end |
|
416 |
else |
|
417 |
let |
|
418 |
val (args, table_ctxt) = fold_map generate tys table_ctxt |
|
419 |
in |
|
420 |
(args MRSL (get_rel_quot_thm ctxt s), table_ctxt) |
|
421 |
end |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
422 |
| generate ty (table, ctxt) = |
50227 | 423 |
if AList.defined (op=) table ty |
424 |
then (the (AList.lookup (op=) table ty), (table, ctxt)) |
|
425 |
else |
|
426 |
let |
|
427 |
val (Q_t, ctxt') = get_fresh_Q_t ctxt |
|
59630 | 428 |
val Q_thm = Thm.assume (Thm.cterm_of ctxt' Q_t) |
429 |
val table' = (ty, Q_thm) :: table |
|
50227 | 430 |
in |
431 |
(Q_thm, (table', ctxt')) |
|
432 |
end |
|
433 |
||
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
434 |
val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt) |
50227 | 435 |
in |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
436 |
(param_quot_thm, rev table, ctxt) |
50227 | 437 |
end |
438 |
handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) |
|
439 |
||
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
440 |
(* |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
441 |
It computes a parametrized relator for the given type ty. E.g., for 'a dlist: |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
442 |
list_all2 ?R OO cr_dlist with parameters [?R]. |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
443 |
|
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
444 |
Returns: the definitional term and list of parameters (relations). |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
445 |
*) |
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
446 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
447 |
fun generate_parametrized_relator ctxt ty = |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
448 |
let |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
449 |
val orig_ctxt = ctxt |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
450 |
val (quot_thm, table, ctxt) = prove_param_quot_thm ctxt ty |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
451 |
val parametrized_relator = quot_thm_crel quot_thm |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
452 |
val args = map (fn (_, q_thm) => quot_thm_crel q_thm) table |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
453 |
val exported_terms = Variable.exportT_terms ctxt orig_ctxt (parametrized_relator :: args) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
454 |
in |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
455 |
(hd exported_terms, tl exported_terms) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
456 |
end |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
457 |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
458 |
(* Parametrization *) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
459 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
460 |
local |
59582 | 461 |
fun get_lhs rule = (Thm.dest_fun o Thm.dest_arg o strip_imp_concl o Thm.cprop_of) rule; |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
462 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
463 |
fun no_imp _ = raise CTERM ("no implication", []); |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
464 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
465 |
infix 0 else_imp |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
466 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
467 |
fun (cv1 else_imp cv2) ct = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
468 |
(cv1 ct |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
469 |
handle THM _ => cv2 ct |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
470 |
| CTERM _ => cv2 ct |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
471 |
| TERM _ => cv2 ct |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
472 |
| TYPE _ => cv2 ct); |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
473 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
474 |
fun first_imp cvs = fold_rev (curry op else_imp) cvs no_imp |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
475 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
476 |
fun rewr_imp rule ct = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
477 |
let |
59586 | 478 |
val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule; |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
479 |
val lhs_rule = get_lhs rule1; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
480 |
val rule2 = Thm.rename_boundvars (Thm.term_of lhs_rule) (Thm.term_of ct) rule1; |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
481 |
val lhs_ct = Thm.dest_fun ct |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
482 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
483 |
Thm.instantiate (Thm.match (lhs_rule, lhs_ct)) rule2 |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
484 |
handle Pattern.MATCH => raise CTERM ("rewr_imp", [lhs_rule, lhs_ct]) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
485 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
486 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
487 |
fun rewrs_imp rules = first_imp (map rewr_imp rules) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
488 |
in |
54335
03b10317ba78
update documentation of important public ML functions in Lifting
kuncar
parents:
53651
diff
changeset
|
489 |
|
60222 | 490 |
fun gen_merge_transfer_relations quotients ctxt ctm = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
491 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
492 |
val ctm = Thm.dest_arg ctm |
59582 | 493 |
val tm = Thm.term_of ctm |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
494 |
val rel = (hd o get_args 2) tm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
495 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
496 |
fun same_constants (Const (n1,_)) (Const (n2,_)) = n1 = n2 |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
497 |
| same_constants _ _ = false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
498 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
499 |
fun prove_extra_assms ctxt ctm distr_rule = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
500 |
let |
59582 | 501 |
fun prove_assm assm = try (Goal.prove ctxt [] [] (Thm.term_of assm)) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
57663
diff
changeset
|
502 |
(fn _ => SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt (Transfer.get_transfer_raw ctxt))) 1) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
503 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
504 |
fun is_POS_or_NEG ctm = |
59582 | 505 |
case (head_of o Thm.term_of o Thm.dest_arg) ctm of |
69593 | 506 |
Const (\<^const_name>\<open>POS\<close>, _) => true |
507 |
| Const (\<^const_name>\<open>NEG\<close>, _) => true |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
508 |
| _ => false |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
509 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
510 |
val inst_distr_rule = rewr_imp distr_rule ctm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
511 |
val extra_assms = filter_out is_POS_or_NEG (cprems_of inst_distr_rule) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
512 |
val proved_assms = map_interrupt prove_assm extra_assms |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
513 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
514 |
Option.map (curry op OF inst_distr_rule) proved_assms |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
515 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
516 |
handle CTERM _ => NONE |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
517 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
518 |
fun cannot_merge_error_msg () = Pretty.block |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
519 |
[Pretty.str "Rewriting (merging) of this term has failed:", |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
520 |
Pretty.brk 1, |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
521 |
Syntax.pretty_term ctxt rel] |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
522 |
|
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
523 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
524 |
case get_args 2 rel of |
69593 | 525 |
[Const (\<^const_name>\<open>HOL.eq\<close>, _), _] => rewrs_imp @{thms neg_eq_OO pos_eq_OO} ctm |
526 |
| [_, Const (\<^const_name>\<open>HOL.eq\<close>, _)] => rewrs_imp @{thms neg_OO_eq pos_OO_eq} ctm |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
527 |
| [_, trans_rel] => |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
528 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
529 |
val (rty', qty) = (relation_types o fastype_of) trans_rel |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
530 |
in |
55454 | 531 |
if same_type_constrs (rty', qty) then |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
532 |
let |
55454 | 533 |
val distr_rules = get_rel_distr_rules ctxt ((fst o dest_Type) rty') (head_of tm) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
534 |
val distr_rule = get_first (prove_extra_assms ctxt ctm) distr_rules |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
535 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
536 |
case distr_rule of |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
537 |
NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ()) |
60222 | 538 |
| SOME distr_rule => (map (gen_merge_transfer_relations quotients ctxt) |
539 |
(cprems_of distr_rule)) |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
540 |
MRSL distr_rule |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
541 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
542 |
else |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
543 |
let |
60222 | 544 |
val pcrel_def = get_pcrel_def quotients ctxt ((fst o dest_Type) qty) |
59582 | 545 |
val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
546 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
547 |
if same_constants pcrel_const (head_of trans_rel) then |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
548 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
549 |
val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
550 |
val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm |
60222 | 551 |
val result = (map (gen_merge_transfer_relations quotients ctxt) |
552 |
(cprems_of distr_rule)) MRSL distr_rule |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
553 |
val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def) |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
554 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
555 |
Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
556 |
(Conv.arg_conv (Conv.arg_conv fold_pcr_rel)) fold_pcr_rel)) result |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
557 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
558 |
else |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
559 |
raise MERGE_TRANSFER_REL (Pretty.str "Non-parametric correspondence relation used.") |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
560 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
561 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
562 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
563 |
handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg |
60222 | 564 |
|
565 |
(* |
|
566 |
ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer |
|
567 |
relation for t and T is a transfer relation between t and f, which consists only from |
|
568 |
parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes |
|
569 |
co-variance or contra-variance. |
|
570 |
||
571 |
The function merges par_R OO T using definitions of parametrized correspondence relations |
|
572 |
(e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T). |
|
573 |
*) |
|
574 |
||
575 |
fun merge_transfer_relations ctxt ctm = gen_merge_transfer_relations |
|
576 |
(Lifting_Info.get_quotients ctxt) ctxt ctm |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
577 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
578 |
|
60222 | 579 |
fun gen_parametrize_transfer_rule quotients ctxt thm = |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
580 |
let |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
581 |
fun parametrize_relation_conv ctm = |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
582 |
let |
59582 | 583 |
val (rty, qty) = (relation_types o fastype_of) (Thm.term_of ctm) |
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
584 |
in |
55454 | 585 |
if same_type_constrs (rty, qty) then |
586 |
if forall op= (Targs rty ~~ Targs qty) then |
|
587 |
Conv.all_conv ctm |
|
588 |
else |
|
589 |
all_args_conv parametrize_relation_conv ctm |
|
590 |
else |
|
591 |
if is_Type qty then |
|
592 |
let |
|
593 |
val q = (fst o dest_Type) qty |
|
594 |
in |
|
595 |
let |
|
60222 | 596 |
val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty) |
597 |
val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) |
|
55454 | 598 |
else (Targs rty', Targs rtyq) |
599 |
in |
|
600 |
if forall op= (rty's ~~ rtyqs) then |
|
601 |
let |
|
60222 | 602 |
val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq quotients ctxt q) |
55454 | 603 |
in |
604 |
Conv.rewr_conv pcr_cr_eq ctm |
|
605 |
end |
|
606 |
handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm |
|
607 |
else |
|
60222 | 608 |
if has_pcrel_info quotients q then |
55455
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
609 |
let |
60222 | 610 |
val pcrel_def = Thm.symmetric (get_pcrel_def quotients ctxt q) |
55455
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
611 |
in |
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
612 |
(Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm |
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
613 |
end |
2cf404a469be
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
kuncar
parents:
55454
diff
changeset
|
614 |
else Conv.arg1_conv (all_args_conv parametrize_relation_conv) ctm |
55454 | 615 |
end |
616 |
end |
|
617 |
else Conv.all_conv ctm |
|
51374
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
618 |
end |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
619 |
in |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
620 |
Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm |
84d01fd733cf
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents:
50288
diff
changeset
|
621 |
end |
60222 | 622 |
|
623 |
(* |
|
624 |
It replaces cr_T by pcr_T op= in the transfer relation. For composed |
|
625 |
abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized |
|
626 |
correspondce relation does not exist, the original relation is kept. |
|
627 |
||
628 |
thm - a transfer rule |
|
629 |
*) |
|
630 |
||
631 |
fun parametrize_transfer_rule ctxt thm = |
|
632 |
gen_parametrize_transfer_rule (Lifting_Info.get_quotients ctxt) ctxt thm |
|
633 |
||
53651 | 634 |
end |