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