author | kuncar |
Mon, 21 May 2012 16:36:48 +0200 | |
changeset 47951 | 8c8a03765de7 |
parent 47853 | c01ba36769f5 |
child 50227 | 01d545993e8c |
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 |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
10 |
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
|
11 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
12 |
val prove_quot_thm: Proof.context -> typ * typ -> thm |
47308 | 13 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
14 |
val abs_fun: Proof.context -> typ * typ -> term |
47308 | 15 |
|
16 |
val equiv_relation: Proof.context -> typ * typ -> term |
|
17 |
end |
|
18 |
||
19 |
structure Lifting_Term: LIFTING_TERM = |
|
20 |
struct |
|
21 |
||
47698 | 22 |
open Lifting_Util |
23 |
||
24 |
infix 0 MRSL |
|
25 |
||
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
26 |
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
|
27 |
exception QUOT_THM of typ * typ * Pretty.T |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
28 |
exception CHECK_RTY of typ * typ |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
29 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
30 |
fun match ctxt err ty_pat ty = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
31 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
32 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
33 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
34 |
Sign.typ_match thy (ty_pat, ty) Vartab.empty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
35 |
handle Type.TYPE_MATCH => err ctxt ty_pat ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
36 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
37 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
38 |
fun equiv_match_err ctxt ty_pat ty = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
39 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
40 |
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
|
41 |
val ty_str = Syntax.string_of_typ ctxt ty |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
42 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
43 |
raise QUOT_THM_INTERNAL (Pretty.block |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
44 |
[Pretty.str ("The quotient type " ^ quote ty_str), |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
45 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
46 |
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
|
47 |
Pretty.brk 1, |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
48 |
Pretty.str "don't match."]) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
49 |
end |
47308 | 50 |
|
51 |
fun get_quot_thm ctxt s = |
|
52 |
let |
|
53 |
val thy = Proof_Context.theory_of ctxt |
|
54 |
in |
|
55 |
(case Lifting_Info.lookup_quotients ctxt s of |
|
56 |
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
|
57 |
| 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
|
58 |
[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
|
59 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
60 |
Pretty.str "found."])) |
47308 | 61 |
end |
62 |
||
63 |
fun get_rel_quot_thm ctxt s = |
|
64 |
let |
|
65 |
val thy = Proof_Context.theory_of ctxt |
|
66 |
in |
|
67 |
(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
|
68 |
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
|
69 |
| 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
|
70 |
[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
|
71 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
72 |
Pretty.str "found."])) |
47308 | 73 |
end |
74 |
||
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
75 |
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
|
76 |
|
47379
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
[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
|
81 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
82 |
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
|
83 |
Pretty.brk 1, |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
84 |
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
|
85 |
else |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
86 |
() |
075d22b3a32f
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
kuncar
parents:
47350
diff
changeset
|
87 |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
88 |
fun zip_Tvars ctxt type_name rty_Tvars qty_Tvars = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
89 |
case try (get_rel_quot_thm ctxt) type_name of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
90 |
NONE => rty_Tvars ~~ qty_Tvars |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
91 |
| SOME rel_quot_thm => |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
92 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
93 |
fun quot_term_absT quot_term = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
94 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
95 |
val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
96 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
97 |
fastype_of abs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
98 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
99 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
100 |
fun equiv_univ_err ctxt ty_pat ty = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
101 |
let |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
102 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
103 |
val ty_str = Syntax.string_of_typ ctxt ty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
104 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
105 |
raise QUOT_THM_INTERNAL (Pretty.block |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
106 |
[Pretty.str ("The type " ^ quote ty_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
107 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
108 |
Pretty.str ("and the relator type pattern " ^ quote ty_pat_str), |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
109 |
Pretty.brk 1, |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
110 |
Pretty.str "don't unify."]) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
111 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
112 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
113 |
fun raw_match (TVar (v, S), T) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
114 |
(case Vartab.defined subs v of |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
115 |
false => Vartab.update_new (v, (S, T)) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
116 |
| true => subs) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
117 |
| raw_match (Type (_, Ts), Type (_, Us)) subs = |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
118 |
raw_matches (Ts, Us) subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
119 |
| raw_match _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
120 |
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
|
121 |
| raw_matches _ subs = subs |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
122 |
|
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
123 |
val rty = Type (type_name, rty_Tvars) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
124 |
val qty = Type (type_name, qty_Tvars) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
125 |
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
|
126 |
val schematic_rel_absT = quot_term_absT rel_quot_thm_concl; |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
127 |
val ctxt' = Variable.declare_typ schematic_rel_absT ctxt |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
128 |
val thy = Proof_Context.theory_of ctxt' |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
129 |
val absT = rty --> qty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
130 |
val schematic_absT = Logic.type_map (singleton (Variable.polymorphic ctxt')) absT |
47853 | 131 |
val maxidx = Term.maxidx_of_typs [schematic_rel_absT, schematic_absT] |
132 |
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
|
133 |
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
|
134 |
val subs = raw_match (schematic_rel_absT, absT) Vartab.empty |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
135 |
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
|
136 |
in |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
137 |
map (dest_funT o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
138 |
Envir.subst_type subs o |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
139 |
quot_term_absT) |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
140 |
rel_quot_thm_prems |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
141 |
end |
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
142 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
143 |
fun prove_schematic_quot_thm ctxt (rty, qty) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
144 |
(case (rty, qty) of |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
145 |
(Type (s, tys), Type (s', tys')) => |
47308 | 146 |
if s = s' |
147 |
then |
|
148 |
let |
|
47778
7bcdaa255a00
support Quotient map theorems with invariant parameters
kuncar
parents:
47777
diff
changeset
|
149 |
val args = map (prove_schematic_quot_thm ctxt) (zip_Tvars ctxt s tys tys') |
47308 | 150 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
151 |
if forall is_id_quot args |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
152 |
then |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
153 |
@{thm identity_quotient} |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
154 |
else |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
155 |
args MRSL (get_rel_quot_thm ctxt s) |
47308 | 156 |
end |
157 |
else |
|
158 |
let |
|
159 |
val quot_thm = get_quot_thm ctxt s' |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
160 |
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
|
161 |
val _ = check_raw_types (s, rs) s' |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
162 |
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
|
163 |
val rtys' = map (Envir.subst_type qtyenv) rtys |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
164 |
val args = map (prove_schematic_quot_thm ctxt) (tys ~~ rtys') |
47308 | 165 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
166 |
if forall is_id_quot args |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
167 |
then |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
168 |
quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
169 |
else |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
170 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
171 |
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
|
172 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
173 |
[rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose} |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
174 |
end |
47308 | 175 |
end |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
176 |
| (_, Type (s', tys')) => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
177 |
(case try (get_quot_thm ctxt) s' of |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
178 |
SOME quot_thm => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
179 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
180 |
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
|
181 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
182 |
prove_schematic_quot_thm ctxt (rty_pat, qty) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
183 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
184 |
| NONE => |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
185 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
186 |
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
|
187 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
188 |
prove_schematic_quot_thm ctxt (rty_pat, qty) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
189 |
end) |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
190 |
| _ => @{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
|
191 |
handle QUOT_THM_INTERNAL pretty_msg => raise QUOT_THM (rty, qty, pretty_msg) |
47308 | 192 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
193 |
fun force_qty_type thy qty quot_thm = |
47308 | 194 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
195 |
val (_, qty_schematic) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
196 |
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
|
197 |
fun prep_ty thy (x, (S, ty)) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
198 |
(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
|
199 |
val ty_inst = Vartab.fold (cons o (prep_ty thy)) match_env [] |
47308 | 200 |
in |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
201 |
Thm.instantiate (ty_inst, []) quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
202 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
203 |
|
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
204 |
fun check_rty_type ctxt rty quot_thm = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
205 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
206 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
207 |
val (rty_forced, _) = quot_thm_rty_qty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
212 |
() |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
213 |
end |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
214 |
|
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
215 |
(* |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
216 |
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
|
217 |
|
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
218 |
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
|
219 |
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
|
220 |
*) |
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
221 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
222 |
fun prove_quot_thm ctxt (rty, qty) = |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
223 |
let |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
224 |
val thy = Proof_Context.theory_of ctxt |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
225 |
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
|
226 |
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
|
227 |
val _ = check_rty_type ctxt rty quot_thm |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
228 |
in |
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
229 |
quot_thm |
47308 | 230 |
end |
231 |
||
47852
0c3b8d036a5c
documentation of the Lifting package on the ML level & tuned
kuncar
parents:
47778
diff
changeset
|
232 |
fun abs_fun ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
233 |
quot_thm_abs (prove_quot_thm ctxt (rty, qty)) |
47350 | 234 |
|
47308 | 235 |
fun equiv_relation ctxt (rty, qty) = |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47386
diff
changeset
|
236 |
quot_thm_rel (prove_quot_thm ctxt (rty, qty)) |
47308 | 237 |
|
238 |
end; |