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