author | kuncar |
Thu, 29 Nov 2012 17:54:20 +0100 | |
changeset 50288 | 986598b0efd1 |
parent 50227 | 01d545993e8c |
child 51374 | 84d01fd733cf |
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 |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
11 |
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
|
12 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
13 |
val prove_quot_thm: Proof.context -> typ * typ -> thm |
47308 | 14 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
15 |
val abs_fun: Proof.context -> typ * typ -> term |
47308 | 16 |
|
17 |
val equiv_relation: Proof.context -> typ * typ -> term |
|
50227 | 18 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
19 |
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
|
20 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
21 |
val generate_parametrized_relator: Proof.context -> typ -> term * term list |
47308 | 22 |
end |
23 |
||
24 |
structure Lifting_Term: LIFTING_TERM = |
|
25 |
struct |
|
47698 | 26 |
open Lifting_Util |
27 |
||
28 |
infix 0 MRSL |
|
29 |
||
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
30 |
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
|
31 |
exception QUOT_THM of typ * typ * Pretty.T |
50227 | 32 |
exception PARAM_QUOT_THM of typ * Pretty.T |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
33 |
exception CHECK_RTY of typ * typ |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
34 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
35 |
fun match ctxt err ty_pat ty = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
36 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
37 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
38 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
39 |
Sign.typ_match thy (ty_pat, ty) Vartab.empty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
40 |
handle Type.TYPE_MATCH => err ctxt ty_pat ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
41 |
end |
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 equiv_match_err ctxt 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 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
|
46 |
val ty_str = Syntax.string_of_typ ctxt ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
47 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
48 |
raise QUOT_THM_INTERNAL (Pretty.block |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
49 |
[Pretty.str ("The quotient type " ^ quote ty_str), |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
50 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
51 |
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
|
52 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
53 |
Pretty.str "don't match."]) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
54 |
end |
47308 | 55 |
|
56 |
fun get_quot_thm ctxt s = |
|
57 |
let |
|
58 |
val thy = Proof_Context.theory_of ctxt |
|
59 |
in |
|
60 |
(case Lifting_Info.lookup_quotients ctxt s of |
|
61 |
SOME qdata => Thm.transfer thy (#quot_thm qdata) |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
62 |
| 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
|
63 |
[Pretty.str ("No quotient type " ^ quote s), |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
64 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
65 |
Pretty.str "found."])) |
47308 | 66 |
end |
67 |
||
68 |
fun get_rel_quot_thm ctxt s = |
|
69 |
let |
|
70 |
val thy = Proof_Context.theory_of ctxt |
|
71 |
in |
|
72 |
(case Lifting_Info.lookup_quotmaps ctxt s of |
|
47777
f29e7dcd7c40
use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents:
47698
diff
changeset
|
73 |
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
|
74 |
| 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
|
75 |
[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
|
76 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
77 |
Pretty.str "found."])) |
47308 | 78 |
end |
79 |
||
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
80 |
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
|
81 |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
[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
|
86 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
87 |
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
|
88 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
89 |
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
|
90 |
else |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
91 |
() |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
92 |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
93 |
fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
94 |
case try (get_rel_quot_thm ctxt) type_name of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
95 |
NONE => rty_Tvars ~~ qty_Tvars |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
96 |
| SOME rel_quot_thm => |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
97 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
98 |
fun quot_term_absT quot_term = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
99 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
100 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
101 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
102 |
fastype_of abs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
103 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
104 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
105 |
fun equiv_univ_err ctxt ty_pat ty = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
106 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
107 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
108 |
val ty_str = Syntax.string_of_typ ctxt ty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
109 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
110 |
raise QUOT_THM_INTERNAL (Pretty.block |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
111 |
[Pretty.str ("The type " ^ quote ty_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
112 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
113 |
Pretty.str ("and the relator type pattern " ^ quote ty_pat_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
114 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
115 |
Pretty.str "don't unify."]) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
116 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
117 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
118 |
fun raw_match (TVar (v, S), T) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
119 |
(case Vartab.defined subs v of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
120 |
false => Vartab.update_new (v, (S, T)) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
121 |
| true => subs) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
122 |
| raw_match (Type (_, Ts), Type (_, Us)) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
123 |
raw_matches (Ts, Us) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
124 |
| raw_match _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
125 |
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
|
126 |
| raw_matches _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
127 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
128 |
val rty = Type (type_name, rty_Tvars) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
129 |
val qty = Type (type_name, qty_Tvars) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
130 |
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
|
131 |
val schematic_rel_absT = quot_term_absT rel_quot_thm_concl; |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
132 |
val ctxt' = Variable.declare_typ schematic_rel_absT ctxt |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
133 |
val thy = Proof_Context.theory_of ctxt' |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
134 |
val absT = rty --> qty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
135 |
val schematic_absT = Logic.type_map (singleton (Variable.polymorphic ctxt')) absT |
47853 | 136 |
val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT] |
137 |
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
|
138 |
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
|
139 |
val subs = raw_match (schematic_rel_absT, absT) Vartab.empty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
140 |
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
|
141 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
142 |
map (dest_funT o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
143 |
Envir.subst_type subs o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
144 |
quot_term_absT) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
145 |
rel_quot_thm_prems |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
146 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
147 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
148 |
fun prove_schematic_quot_thm ctxt (rty, qty) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
149 |
(case (rty, qty) of |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
150 |
(Type (s, tys), Type (s', tys')) => |
47308 | 151 |
if s = s' |
152 |
then |
|
153 |
let |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
154 |
val args = map (prove_schematic_quot_thm ctxt) (zip_Tvars ctxt s tys tys') |
47308 | 155 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
156 |
if forall is_id_quot args |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
157 |
then |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
158 |
@{thm identity_quotient} |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
159 |
else |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
160 |
args MRSL (get_rel_quot_thm ctxt s) |
47308 | 161 |
end |
162 |
else |
|
163 |
let |
|
164 |
val quot_thm = get_quot_thm ctxt s' |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
165 |
val (Type (rs, rtys), qty_pat) = quot_thm_rty_qty quot_thm |
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
166 |
val _ = check_raw_types (s, rs) s' |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
167 |
val qtyenv = match ctxt equiv_match_err qty_pat qty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
168 |
val rtys' = map (Envir.subst_type qtyenv) rtys |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
169 |
val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys') |
47308 | 170 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
171 |
if forall is_id_quot args |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
172 |
then |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
173 |
quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
174 |
else |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
175 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
176 |
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
|
177 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
178 |
[rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
179 |
end |
47308 | 180 |
end |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
181 |
| (_, Type (s', tys')) => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
182 |
(case try (get_quot_thm ctxt) s' of |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
183 |
SOME quot_thm => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
184 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
185 |
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
|
186 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
187 |
prove_schematic_quot_thm ctxt (rty_pat, qty) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
188 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
189 |
| NONE => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
190 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
191 |
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
|
192 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
193 |
prove_schematic_quot_thm ctxt (rty_pat, qty) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
194 |
end) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
195 |
| _ => @{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
|
196 |
handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg) |
47308 | 197 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
198 |
fun force_qty_type thy qty quot_thm = |
47308 | 199 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
200 |
val (_, qty_schematic) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
201 |
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
|
202 |
fun prep_ty thy (x, (S, ty)) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
203 |
(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
|
204 |
val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env [] |
47308 | 205 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
206 |
Thm.instantiate (ty_inst, []) quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
207 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
208 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
209 |
fun check_rty_type ctxt rty quot_thm = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
210 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
211 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
212 |
val (rty_forced, _) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
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
|
216 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
217 |
() |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
218 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
219 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
220 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
221 |
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
|
222 |
|
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
223 |
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
|
224 |
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
|
225 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
226 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
227 |
fun prove_quot_thm ctxt (rty, qty) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
228 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
229 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
230 |
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
|
231 |
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
|
232 |
val _ = check_rty_type ctxt rty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
233 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
234 |
quot_thm |
47308 | 235 |
end |
236 |
||
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
237 |
fun abs_fun ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
238 |
quot_thm_abs (prove_quot_thm ctxt (rty, qty)) |
47350 | 239 |
|
47308 | 240 |
fun equiv_relation ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
241 |
quot_thm_rel (prove_quot_thm ctxt (rty, qty)) |
47308 | 242 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
243 |
val get_fresh_Q_t = |
50227 | 244 |
let |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
245 |
val Q_t = @{term "Trueprop (Quotient R Abs Rep T)"} |
50227 | 246 |
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
|
247 |
val tfrees_Q_t = rev (Term.add_tfree_names Q_t []) |
50227 | 248 |
in |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
249 |
fn ctxt => |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
250 |
let |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
251 |
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
|
252 |
| rename_free_var _ t = t |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
253 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
254 |
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
|
255 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
256 |
fun rename_free_tvars tab = |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
257 |
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
|
258 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
259 |
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
|
260 |
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
|
261 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
|
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
265 |
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
|
266 |
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
|
267 |
in |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
268 |
(renamed_Q_t, ctxt) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
269 |
end |
50227 | 270 |
end |
271 |
||
272 |
fun prove_param_quot_thm ctxt ty = |
|
273 |
let |
|
274 |
fun generate (ty as Type (s, tys)) (table_ctxt as (table, ctxt)) = |
|
275 |
if null tys |
|
276 |
then |
|
277 |
let |
|
278 |
val thy = Proof_Context.theory_of ctxt |
|
279 |
val instantiated_id_quot_thm = instantiate' [SOME (ctyp_of thy ty)] [] @{thm identity_quotient} |
|
280 |
in |
|
281 |
(instantiated_id_quot_thm, (table, ctxt)) |
|
282 |
end |
|
283 |
else |
|
284 |
let |
|
285 |
val (args, table_ctxt) = fold_map generate tys table_ctxt |
|
286 |
in |
|
287 |
(args MRSL (get_rel_quot_thm ctxt s), table_ctxt) |
|
288 |
end |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
289 |
| generate (ty as (TFree _)) (table, ctxt) = |
50227 | 290 |
if AList.defined (op=) table ty |
291 |
then (the (AList.lookup (op=) table ty), (table, ctxt)) |
|
292 |
else |
|
293 |
let |
|
294 |
val thy = Proof_Context.theory_of ctxt |
|
295 |
val (Q_t, ctxt') = get_fresh_Q_t ctxt |
|
296 |
val Q_thm = Thm.assume (cterm_of thy Q_t) |
|
297 |
val table' = (ty, Q_thm)::table |
|
298 |
in |
|
299 |
(Q_thm, (table', ctxt')) |
|
300 |
end |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
301 |
| generate _ _ = error "generate_param_quot_thm: TVar" |
50227 | 302 |
|
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
303 |
val (param_quot_thm, (table, ctxt)) = generate ty ([], ctxt) |
50227 | 304 |
in |
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
305 |
(param_quot_thm, rev table, ctxt) |
50227 | 306 |
end |
307 |
handle QUOT_THM_INTERNAL pretty_msg => raise PARAM_QUOT_THM (ty, pretty_msg) |
|
308 |
||
50288
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
309 |
fun generate_parametrized_relator ctxt ty = |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
310 |
let |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
311 |
val orig_ctxt = ctxt |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
312 |
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
|
313 |
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
|
314 |
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
|
315 |
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
|
316 |
in |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
317 |
(hd exported_terms, tl exported_terms) |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
318 |
end |
986598b0efd1
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
kuncar
parents:
50227
diff
changeset
|
319 |
|
47308 | 320 |
end; |