author | Christian Urban <urbanc@in.tum.de> |
Fri, 25 Nov 2011 00:18:59 +0000 | |
changeset 45628 | f21eb7073895 |
parent 45534 | 4ab21521b393 |
child 45795 | 2d8949268303 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Quotient/quotient_term.ML |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk and Christian Urban |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
|
35788 | 4 |
Constructs terms corresponding to goals from lifting theorems to |
5 |
quotient types. |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
signature QUOTIENT_TERM = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
sig |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
exception LIFT_MATCH of string |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
datatype flag = AbsF | RepF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
val absrep_fun: flag -> Proof.context -> typ * typ -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
(* Allows Nitpick to represent quotient types as single elements from raw type *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
val absrep_const_chk: flag -> Proof.context -> string -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
val equiv_relation: Proof.context -> typ * typ -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
21 |
val equiv_relation_chk: Proof.context -> typ * typ -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
22 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
23 |
val regularize_trm: Proof.context -> term * term -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
24 |
val regularize_trm_chk: Proof.context -> term * term -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
25 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
val inj_repabs_trm: Proof.context -> term * term -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
val inj_repabs_trm_chk: Proof.context -> term * term -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
28 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
29 |
val derive_qtyp: Proof.context -> typ list -> typ -> typ |
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
30 |
val derive_qtrm: Proof.context -> typ list -> term -> term |
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
31 |
val derive_rtyp: Proof.context -> typ list -> typ -> typ |
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
32 |
val derive_rtrm: Proof.context -> typ list -> term -> term |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
33 |
end; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
34 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
35 |
structure Quotient_Term: QUOTIENT_TERM = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
36 |
struct |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
37 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
38 |
exception LIFT_MATCH of string |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
40 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
41 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
(*** Aggregate Rep/Abs Function ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
43 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
44 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
45 |
(* The flag RepF is for types in negative position; AbsF is for types |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
in positive position. Because of this, function types need to be |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
treated specially, since there the polarity changes. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
49 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
50 |
datatype flag = AbsF | RepF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
51 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
52 |
fun negF AbsF = RepF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
| negF RepF = AbsF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
|
37677 | 55 |
fun is_identity (Const (@{const_name id}, _)) = true |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
| is_identity _ = false |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
|
37677 | 58 |
fun mk_identity ty = Const (@{const_name id}, ty --> ty) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
fun mk_fun_compose flag (trm1, trm2) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
61 |
case flag of |
37677 | 62 |
AbsF => Const (@{const_name comp}, dummyT) $ trm1 $ trm2 |
63 |
| RepF => Const (@{const_name comp}, dummyT) $ trm2 $ trm1 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
65 |
fun get_mapfun thy s = |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
66 |
(case Quotient_Info.lookup_quotmaps_global thy s of |
45273
728ed9d28c63
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
bulwahn
parents:
45272
diff
changeset
|
67 |
SOME map_data => Const (#mapfun map_data, dummyT) |
45279 | 68 |
| NONE => raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
69 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
70 |
(* makes a Free out of a TVar *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
71 |
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
72 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
73 |
(* produces an aggregate map function for the |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
74 |
rty-part of a quotient definition; abstracts |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
over all variables listed in vs (these variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
76 |
correspond to the type variables in rty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
77 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
78 |
for example for: (?'a list * ?'b) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
it produces: %a b. prod_map (map a) b |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
*) |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
81 |
fun mk_mapfun thy vs rty = |
41444 | 82 |
let |
83 |
val vs' = map mk_Free vs |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
84 |
|
41444 | 85 |
fun mk_mapfun_aux rty = |
86 |
case rty of |
|
87 |
TVar _ => mk_Free rty |
|
88 |
| Type (_, []) => mk_identity rty |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
89 |
| Type (s, tys) => list_comb (get_mapfun thy s, map mk_mapfun_aux tys) |
41444 | 90 |
| _ => raise LIFT_MATCH "mk_mapfun (default)" |
91 |
in |
|
92 |
fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
|
93 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
94 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
95 |
(* looks up the (varified) rty and qty for |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
96 |
a quotient definition |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
*) |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
98 |
fun get_rty_qty thy s = |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
99 |
(case Quotient_Info.lookup_quotients_global thy s of |
45272
5995ab88a00f
respecting isabelle's programming style in the quotient package by simplifying quotdata_lookup function for data access
bulwahn
parents:
44413
diff
changeset
|
100 |
SOME qdata => (#rtyp qdata, #qtyp qdata) |
45280 | 101 |
| NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
102 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
103 |
(* takes two type-environments and looks |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
104 |
up in both of them the variable v, which |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
105 |
must be listed in the environment |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
fun double_lookup rtyenv qtyenv v = |
41444 | 108 |
let |
109 |
val v' = fst (dest_TVar v) |
|
110 |
in |
|
111 |
(snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) |
|
112 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
113 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
114 |
(* matches a type pattern with a type *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
fun match ctxt err ty_pat ty = |
41444 | 116 |
let |
42361 | 117 |
val thy = Proof_Context.theory_of ctxt |
41444 | 118 |
in |
119 |
Sign.typ_match thy (ty_pat, ty) Vartab.empty |
|
120 |
handle Type.TYPE_MATCH => err ctxt ty_pat ty |
|
121 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
122 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
123 |
(* produces the rep or abs constant for a qty *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
fun absrep_const flag ctxt qty_str = |
41444 | 125 |
let |
45534
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
126 |
(* FIXME *) |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
127 |
fun mk_dummyT (Const (c, _)) = Const (c, dummyT) |
45628
f21eb7073895
in a local context, also the free variable case needs to be analysed default tip
Christian Urban <urbanc@in.tum.de>
parents:
45534
diff
changeset
|
128 |
| mk_dummyT (Free (c, _)) = Free (c, dummyT) |
f21eb7073895
in a local context, also the free variable case needs to be analysed default tip
Christian Urban <urbanc@in.tum.de>
parents:
45534
diff
changeset
|
129 |
| mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable" |
41444 | 130 |
in |
45534
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
131 |
case Quotient_Info.lookup_abs_rep ctxt qty_str of |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
132 |
SOME abs_rep => |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
133 |
mk_dummyT (case flag of |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
134 |
AbsF => #abs abs_rep |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
135 |
| RepF => #rep abs_rep) |
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
136 |
| NONE => error ("No abs/rep terms for " ^ quote qty_str) |
41444 | 137 |
end |
45534
4ab21521b393
adding database of abs and rep terms to the quotient package; registering abs and rep terms in quotient_type and using them in quotient_definition
bulwahn
parents:
45340
diff
changeset
|
138 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
139 |
(* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
fun absrep_const_chk flag ctxt qty_str = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
Syntax.check_term ctxt (absrep_const flag ctxt qty_str) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
143 |
fun absrep_match_err ctxt ty_pat ty = |
41444 | 144 |
let |
145 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
146 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
147 |
in |
|
148 |
raise LIFT_MATCH (space_implode " " |
|
149 |
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
150 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
(** generation of an aggregate absrep function **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
(* - In case of equal types we just return the identity. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
- In case of TFrees we also return the identity. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
- In case of function types we recurse taking |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
the polarity change into account. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
- If the type constructors are equal, we recurse for the |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
arguments and build the appropriate map function. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
- If the type constructors are unequal, there must be an |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
instance of quotient types: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
- we first look up the corresponding rty_pat and qty_pat |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
169 |
from the quotient definition; the arguments of qty_pat |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
must be some distinct TVars |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
171 |
- we then match the rty_pat with rty and qty_pat with qty; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
172 |
if matching fails the types do not correspond -> error |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
173 |
- the matching produces two environments; we look up the |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
174 |
assignments for the qty_pat variables and recurse on the |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
assignments |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
176 |
- we prefix the aggregate map function for the rty_pat, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
which is an abstraction over all type variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
- finally we compose the result with the appropriate |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
179 |
absrep function in case at least one argument produced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
a non-identity function / |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
otherwise we just return the appropriate absrep |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
function |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
The composition is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
186 |
('a list) list / ('a foo) foo |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
The matching is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
('a * 'a) list / 'a bar |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
191 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
192 |
The test is necessary in order to eliminate superfluous |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
identity maps. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
194 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
195 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
196 |
fun absrep_fun flag ctxt (rty, qty) = |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
197 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
198 |
val thy = Proof_Context.theory_of ctxt |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
199 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
200 |
if rty = qty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
201 |
then mk_identity rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
202 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
203 |
case (rty, qty) of |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
204 |
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
41444 | 205 |
let |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
206 |
val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
207 |
val arg2 = absrep_fun flag ctxt (ty2, ty2') |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
208 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
209 |
list_comb (get_mapfun thy "fun", [arg1, arg2]) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
210 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
211 |
(* FIXME: use type_name antiquotation if set type becomes explicit *) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
212 |
| (Type ("Set.set", [ty]), Type ("Set.set", [ty'])) => |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
213 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
214 |
val arg = absrep_fun (negF flag) ctxt (ty, ty') |
41444 | 215 |
in |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
216 |
get_mapfun thy "Set.set" $ arg |
41444 | 217 |
end |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
218 |
| (Type (s, tys), Type (s', tys')) => |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
219 |
if s = s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
220 |
then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
221 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
222 |
val args = map (absrep_fun flag ctxt) (tys ~~ tys') |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
223 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
224 |
list_comb (get_mapfun thy s, args) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
225 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
226 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
227 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
228 |
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
229 |
val rtyenv = match ctxt absrep_match_err rty_pat rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
230 |
val qtyenv = match ctxt absrep_match_err qty_pat qty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
231 |
val args_aux = map (double_lookup rtyenv qtyenv) vs |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
232 |
val args = map (absrep_fun flag ctxt) args_aux |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
233 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
234 |
if forall is_identity args |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
235 |
then absrep_const flag ctxt s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
236 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
237 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
238 |
val map_fun = mk_mapfun thy vs rty_pat |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
239 |
val result = list_comb (map_fun, args) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
240 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
241 |
mk_fun_compose flag (absrep_const flag ctxt s', result) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
242 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
243 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
244 |
| (TFree x, TFree x') => |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
245 |
if x = x' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
246 |
then mk_identity rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
247 |
else raise (LIFT_MATCH "absrep_fun (frees)") |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
248 |
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
249 |
| _ => raise (LIFT_MATCH "absrep_fun (default)") |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
250 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
fun absrep_fun_chk flag ctxt (rty, qty) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |
absrep_fun flag ctxt (rty, qty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
254 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
255 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
256 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
257 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
258 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
259 |
(*** Aggregate Equivalence Relation ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
260 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
261 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
(* works very similar to the absrep generation, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
263 |
except there is no need for polarities |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
264 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
265 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
266 |
(* instantiates TVars so that the term is of type ty *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
267 |
fun force_typ ctxt trm ty = |
41444 | 268 |
let |
42361 | 269 |
val thy = Proof_Context.theory_of ctxt |
41444 | 270 |
val trm_ty = fastype_of trm |
271 |
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
|
272 |
in |
|
273 |
map_types (Envir.subst_type ty_inst) trm |
|
274 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
275 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
276 |
fun is_eq (Const (@{const_name HOL.eq}, _)) = true |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
277 |
| is_eq _ = false |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
278 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
279 |
fun mk_rel_compose (trm1, trm2) = |
35402 | 280 |
Const (@{const_abbrev "rel_conj"}, dummyT) $ trm1 $ trm2 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
281 |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
282 |
fun get_relmap thy s = |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
283 |
(case Quotient_Info.lookup_quotmaps thy s of |
45273
728ed9d28c63
respecting isabelle's programming style in the quotient package by simplifying map_lookup function for data access
bulwahn
parents:
45272
diff
changeset
|
284 |
SOME map_data => Const (#relmap map_data, dummyT) |
45279 | 285 |
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
286 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
287 |
fun mk_relmap ctxt vs rty = |
41444 | 288 |
let |
289 |
val vs' = map (mk_Free) vs |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
290 |
|
41444 | 291 |
fun mk_relmap_aux rty = |
292 |
case rty of |
|
293 |
TVar _ => mk_Free rty |
|
294 |
| Type (_, []) => HOLogic.eq_const rty |
|
295 |
| Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
|
296 |
| _ => raise LIFT_MATCH ("mk_relmap (default)") |
|
297 |
in |
|
298 |
fold_rev Term.lambda vs' (mk_relmap_aux rty) |
|
299 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
300 |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
301 |
fun get_equiv_rel thy s = |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
302 |
(case Quotient_Info.lookup_quotients thy s of |
45279 | 303 |
SOME qdata => #equiv_rel qdata |
304 |
| NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
305 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
306 |
fun equiv_match_err ctxt ty_pat ty = |
41444 | 307 |
let |
308 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
309 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
310 |
in |
|
311 |
raise LIFT_MATCH (space_implode " " |
|
312 |
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
313 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
314 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
315 |
(* builds the aggregate equivalence relation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
316 |
that will be the argument of Respects |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
317 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
318 |
fun equiv_relation ctxt (rty, qty) = |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
319 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
320 |
val thy = Proof_Context.theory_of ctxt |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
321 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
322 |
if rty = qty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
323 |
then HOLogic.eq_const rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
324 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
325 |
case (rty, qty) of |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
326 |
(Type (s, tys), Type (s', tys')) => |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
327 |
if s = s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
328 |
then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
329 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
330 |
val args = map (equiv_relation ctxt) (tys ~~ tys') |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
331 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
332 |
list_comb (get_relmap ctxt s, args) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
333 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
334 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
335 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
336 |
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty thy s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
337 |
val rtyenv = match ctxt equiv_match_err rty_pat rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
338 |
val qtyenv = match ctxt equiv_match_err qty_pat qty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
339 |
val args_aux = map (double_lookup rtyenv qtyenv) vs |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
340 |
val args = map (equiv_relation ctxt) args_aux |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
341 |
val eqv_rel = get_equiv_rel ctxt s' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
342 |
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool}) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
343 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
344 |
if forall is_eq args |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
345 |
then eqv_rel' |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
346 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
347 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
348 |
val rel_map = mk_relmap ctxt vs rty_pat |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
349 |
val result = list_comb (rel_map, args) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
350 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
351 |
mk_rel_compose (result, eqv_rel') |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
352 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
353 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
354 |
| _ => HOLogic.eq_const rty |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
355 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
356 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
357 |
fun equiv_relation_chk ctxt (rty, qty) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
358 |
equiv_relation ctxt (rty, qty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
359 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
360 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
361 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
362 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
363 |
(*** Regularization ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
364 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
365 |
(* Regularizing an rtrm means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
366 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
367 |
- Quantifiers over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
368 |
by bounded quantifiers, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
369 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
370 |
All P ----> All (Respects R) P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
371 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
372 |
where the aggregate relation R is given by the rty and qty; |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
373 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
374 |
- Abstractions over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
375 |
by bounded abstractions, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
376 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
377 |
%x. P ----> Ball (Respects R) %x. P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
378 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
379 |
- Equalities over types that need lifting are replaced by |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
380 |
corresponding equivalence relations, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
381 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
382 |
A = B ----> R A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
383 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
384 |
or |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
385 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
386 |
A = B ----> (R ===> R) A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
387 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
388 |
for more complicated types of A and B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
389 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
390 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
391 |
The regularize_trm accepts raw theorems in which equalities |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
392 |
and quantifiers match exactly the ones in the lifted theorem |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
393 |
but also accepts partially regularized terms. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
394 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
395 |
This means that the raw theorems can have: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
396 |
Ball (Respects R), Bex (Respects R), Bex1_rel (Respects R), Babs, R |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
397 |
in the places where: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
398 |
All, Ex, Ex1, %, (op =) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
399 |
is required the lifted theorem. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
400 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
401 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
402 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
403 |
val mk_babs = Const (@{const_name Babs}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
404 |
val mk_ball = Const (@{const_name Ball}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
405 |
val mk_bex = Const (@{const_name Bex}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
406 |
val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
407 |
val mk_resp = Const (@{const_name Respects}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
408 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
409 |
(* - applies f to the subterm of an abstraction, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
410 |
otherwise to the given term, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
411 |
- used by regularize, therefore abstracted |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
412 |
variables do not have to be treated specially |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
413 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
414 |
fun apply_subt f (trm1, trm2) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
415 |
case (trm1, trm2) of |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
416 |
(Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t')) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
417 |
| _ => f (trm1, trm2) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
418 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
419 |
fun term_mismatch str ctxt t1 t2 = |
41444 | 420 |
let |
421 |
val t1_str = Syntax.string_of_term ctxt t1 |
|
422 |
val t2_str = Syntax.string_of_term ctxt t2 |
|
423 |
val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
|
424 |
val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
|
425 |
in |
|
426 |
raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
|
427 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
428 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
429 |
(* the major type of All and Ex quantifiers *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
430 |
fun qnt_typ ty = domain_type (domain_type ty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
431 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
432 |
(* Checks that two types match, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
433 |
rty -> rty matches qty -> qty *) |
45280 | 434 |
fun matches_typ ctxt rT qT = |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
435 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
436 |
val thy = Proof_Context.theory_of ctxt |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
437 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
438 |
if rT = qT then true |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
439 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
440 |
(case (rT, qT) of |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
441 |
(Type (rs, rtys), Type (qs, qtys)) => |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
442 |
if rs = qs then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
443 |
if length rtys <> length qtys then false |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
444 |
else forall (fn x => x = true) (map2 (matches_typ ctxt) rtys qtys) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
445 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
446 |
(case Quotient_Info.lookup_quotients_global thy qs of |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
447 |
SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
448 |
| NONE => false) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
449 |
| _ => false) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
450 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
451 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
452 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
453 |
(* produces a regularized version of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
454 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
455 |
- the result might contain dummyTs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
456 |
|
38718 | 457 |
- for regularization we do not need any |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
458 |
special treatment of bound variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
459 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
460 |
fun regularize_trm ctxt (rtrm, qtrm) = |
45280 | 461 |
(case (rtrm, qtrm) of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
462 |
(Abs (x, ty, t), Abs (_, ty', t')) => |
41444 | 463 |
let |
464 |
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
|
465 |
in |
|
466 |
if ty = ty' then subtrm |
|
467 |
else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
|
468 |
end |
|
45280 | 469 |
|
37677 | 470 |
| (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
41444 | 471 |
let |
472 |
val subtrm = regularize_trm ctxt (t, t') |
|
473 |
val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
|
474 |
in |
|
475 |
if resrel <> needres |
|
476 |
then term_mismatch "regularize (Babs)" ctxt resrel needres |
|
477 |
else mk_babs $ resrel $ subtrm |
|
478 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
479 |
|
37677 | 480 |
| (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => |
41444 | 481 |
let |
482 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
483 |
in |
|
484 |
if ty = ty' then Const (@{const_name All}, ty) $ subtrm |
|
485 |
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
486 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
487 |
|
37677 | 488 |
| (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => |
41444 | 489 |
let |
490 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
491 |
in |
|
492 |
if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm |
|
493 |
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
494 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
495 |
|
37677 | 496 |
| (Const (@{const_name Ex1}, ty) $ (Abs (_, _, |
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38718
diff
changeset
|
497 |
(Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $ |
37677 | 498 |
(Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), |
499 |
Const (@{const_name Ex1}, ty') $ t') => |
|
41444 | 500 |
let |
501 |
val t_ = incr_boundvars (~1) t |
|
502 |
val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
|
503 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
504 |
in |
|
505 |
if resrel <> needrel |
|
506 |
then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
507 |
else mk_bex1_rel $ resrel $ subtrm |
|
508 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
509 |
|
38558 | 510 |
| (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') => |
41444 | 511 |
let |
512 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
513 |
in |
|
514 |
if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm |
|
515 |
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
516 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
517 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
518 |
| (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
38558 | 519 |
Const (@{const_name All}, ty') $ t') => |
41444 | 520 |
let |
521 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
522 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
523 |
in |
|
524 |
if resrel <> needrel |
|
525 |
then term_mismatch "regularize (Ball)" ctxt resrel needrel |
|
526 |
else mk_ball $ (mk_resp $ resrel) $ subtrm |
|
527 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
528 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
529 |
| (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
38558 | 530 |
Const (@{const_name Ex}, ty') $ t') => |
41444 | 531 |
let |
532 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
533 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
534 |
in |
|
535 |
if resrel <> needrel |
|
536 |
then term_mismatch "regularize (Bex)" ctxt resrel needrel |
|
537 |
else mk_bex $ (mk_resp $ resrel) $ subtrm |
|
538 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
539 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
540 |
| (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => |
41444 | 541 |
let |
542 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
543 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
544 |
in |
|
545 |
if resrel <> needrel |
|
546 |
then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
|
547 |
else mk_bex1_rel $ resrel $ subtrm |
|
548 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
549 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
550 |
| (* equalities need to be replaced by appropriate equivalence relations *) |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
551 |
(Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) => |
41444 | 552 |
if ty = ty' then rtrm |
553 |
else equiv_relation ctxt (domain_type ty, domain_type ty') |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
554 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
555 |
| (* in this case we just check whether the given equivalence relation is correct *) |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
556 |
(rel, Const (@{const_name HOL.eq}, ty')) => |
41444 | 557 |
let |
558 |
val rel_ty = fastype_of rel |
|
559 |
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
|
560 |
in |
|
561 |
if rel' aconv rel then rtrm |
|
562 |
else term_mismatch "regularize (relation mismatch)" ctxt rel rel' |
|
563 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
564 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
565 |
| (_, Const _) => |
41444 | 566 |
let |
42361 | 567 |
val thy = Proof_Context.theory_of ctxt |
45280 | 568 |
fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T' |
41444 | 569 |
| same_const _ _ = false |
570 |
in |
|
571 |
if same_const rtrm qtrm then rtrm |
|
572 |
else |
|
573 |
let |
|
45279 | 574 |
val rtrm' = |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
575 |
(case Quotient_Info.lookup_quotconsts_global thy qtrm of |
45279 | 576 |
SOME qconst_info => #rconst qconst_info |
577 |
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) |
|
41444 | 578 |
in |
579 |
if Pattern.matches thy (rtrm', rtrm) |
|
580 |
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
|
581 |
end |
|
582 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
583 |
|
37591 | 584 |
| (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
585 |
((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
586 |
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2))) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
587 |
|
37591 | 588 |
| (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)), |
589 |
((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) => |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
590 |
regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2)) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
591 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
592 |
| (t1 $ t2, t1' $ t2') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
593 |
regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2') |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
594 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
595 |
| (Bound i, Bound i') => |
41444 | 596 |
if i = i' then rtrm |
597 |
else raise (LIFT_MATCH "regularize (bounds mismatch)") |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
598 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
599 |
| _ => |
41444 | 600 |
let |
601 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
602 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
603 |
in |
|
604 |
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
|
45280 | 605 |
end) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
606 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
607 |
fun regularize_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
608 |
regularize_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
609 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
610 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
611 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
612 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
613 |
(*** Rep/Abs Injection ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
614 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
615 |
(* |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
616 |
Injection of Rep/Abs means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
617 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
618 |
For abstractions: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
619 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
620 |
* If the type of the abstraction needs lifting, then we add Rep/Abs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
621 |
around the abstraction; otherwise we leave it unchanged. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
622 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
623 |
For applications: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
624 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
625 |
* If the application involves a bounded quantifier, we recurse on |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
626 |
the second argument. If the application is a bounded abstraction, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
627 |
we always put an Rep/Abs around it (since bounded abstractions |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
628 |
are assumed to always need lifting). Otherwise we recurse on both |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
629 |
arguments. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
630 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
631 |
For constants: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
632 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
633 |
* If the constant is (op =), we leave it always unchanged. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
634 |
Otherwise the type of the constant needs lifting, we put |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
635 |
and Rep/Abs around it. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
636 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
637 |
For free variables: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
638 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
639 |
* We put a Rep/Abs around it if the type needs lifting. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
640 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
641 |
Vars case cannot occur. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
642 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
643 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
644 |
fun mk_repabs ctxt (T, T') trm = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
645 |
absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
646 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
647 |
fun inj_repabs_err ctxt msg rtrm qtrm = |
41444 | 648 |
let |
649 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
650 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
651 |
in |
|
652 |
raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
|
653 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
654 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
655 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
656 |
(* bound variables need to be treated properly, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
657 |
as the type of subterms needs to be calculated *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
658 |
fun inj_repabs_trm ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
659 |
case (rtrm, qtrm) of |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
660 |
(Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') => |
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
661 |
Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
662 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
663 |
| (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') => |
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
664 |
Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t')) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
665 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
666 |
| (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) => |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
667 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
668 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
669 |
val qty = fastype_of qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
670 |
in |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
671 |
mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t'))) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
672 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
673 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
674 |
| (Abs (x, T, t), Abs (x', T', t')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
675 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
676 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
677 |
val qty = fastype_of qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
678 |
val (y, s) = Term.dest_abs (x, T, t) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
679 |
val (_, s') = Term.dest_abs (x', T', t') |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
680 |
val yvar = Free (y, T) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
681 |
val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s')) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
682 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
683 |
if rty = qty then result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
684 |
else mk_repabs ctxt (rty, qty) result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
685 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
686 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
687 |
| (t $ s, t' $ s') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
688 |
(inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s')) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
689 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
690 |
| (Free (_, T), Free (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
691 |
if T = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
692 |
else mk_repabs ctxt (T, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
693 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
694 |
| (_, Const (@{const_name HOL.eq}, _)) => rtrm |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
695 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
696 |
| (_, Const (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
697 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
698 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
699 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
700 |
if rty = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
701 |
else mk_repabs ctxt (rty, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
702 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
703 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
704 |
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
705 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
706 |
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
707 |
inj_repabs_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
708 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
709 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
710 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
711 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
712 |
(*** Wrapper for automatically transforming an rthm into a qthm ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
713 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
714 |
(* substitutions functions for r/q-types and |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
715 |
r/q-constants, respectively |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
716 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
717 |
fun subst_typ ctxt ty_subst rty = |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
718 |
case rty of |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
719 |
Type (s, rtys) => |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
720 |
let |
42361 | 721 |
val thy = Proof_Context.theory_of ctxt |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
722 |
val rty' = Type (s, map (subst_typ ctxt ty_subst) rtys) |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
723 |
|
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
724 |
fun matches [] = rty' |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
725 |
| matches ((rty, qty)::tail) = |
45280 | 726 |
(case try (Sign.typ_match thy (rty, rty')) Vartab.empty of |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
727 |
NONE => matches tail |
45280 | 728 |
| SOME inst => Envir.subst_type inst qty) |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
729 |
in |
41444 | 730 |
matches ty_subst |
731 |
end |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
732 |
| _ => rty |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
733 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
734 |
fun subst_trm ctxt ty_subst trm_subst rtrm = |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
735 |
case rtrm of |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
736 |
t1 $ t2 => (subst_trm ctxt ty_subst trm_subst t1) $ (subst_trm ctxt ty_subst trm_subst t2) |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
737 |
| Abs (x, ty, t) => Abs (x, subst_typ ctxt ty_subst ty, subst_trm ctxt ty_subst trm_subst t) |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
738 |
| Free(n, ty) => Free(n, subst_typ ctxt ty_subst ty) |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
739 |
| Var(n, ty) => Var(n, subst_typ ctxt ty_subst ty) |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
740 |
| Bound i => Bound i |
41444 | 741 |
| Const (a, ty) => |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
742 |
let |
42361 | 743 |
val thy = Proof_Context.theory_of ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
744 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
745 |
fun matches [] = Const (a, subst_typ ctxt ty_subst ty) |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
746 |
| matches ((rconst, qconst)::tail) = |
45280 | 747 |
(case try (Pattern.match thy (rconst, rtrm)) (Vartab.empty, Vartab.empty) of |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
748 |
NONE => matches tail |
45280 | 749 |
| SOME inst => Envir.subst_term inst qconst) |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
750 |
in |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
751 |
matches trm_subst |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
752 |
end |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
753 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
754 |
(* generate type and term substitutions out of the |
41444 | 755 |
qtypes involved in a quotient; the direction flag |
756 |
indicates in which direction the substitutions work: |
|
757 |
||
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
758 |
true: quotient -> raw |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
759 |
false: raw -> quotient |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
760 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
761 |
fun mk_ty_subst qtys direction ctxt = |
41444 | 762 |
let |
42361 | 763 |
val thy = Proof_Context.theory_of ctxt |
41444 | 764 |
in |
45279 | 765 |
Quotient_Info.dest_quotients ctxt |
41444 | 766 |
|> map (fn x => (#rtyp x, #qtyp x)) |
767 |
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) |
|
768 |
|> map (if direction then swap else I) |
|
769 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
770 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
771 |
fun mk_trm_subst qtys direction ctxt = |
41444 | 772 |
let |
773 |
val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) |
|
774 |
fun proper (t1, t2) = subst_typ' (fastype_of t1) = fastype_of t2 |
|
37563
6cf28a1dfd75
Add reverse lifting flag to automated theorem derivation
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
37560
diff
changeset
|
775 |
|
41444 | 776 |
val const_substs = |
45279 | 777 |
Quotient_Info.dest_quotconsts ctxt |
41444 | 778 |
|> map (fn x => (#rconst x, #qconst x)) |
779 |
|> map (if direction then swap else I) |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
780 |
|
41444 | 781 |
val rel_substs = |
45279 | 782 |
Quotient_Info.dest_quotients ctxt |
41444 | 783 |
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) |
784 |
|> map (if direction then swap else I) |
|
785 |
in |
|
786 |
filter proper (const_substs @ rel_substs) |
|
787 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
788 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
789 |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
790 |
(* derives a qtyp and qtrm out of a rtyp and rtrm, |
41444 | 791 |
respectively |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
792 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
793 |
fun derive_qtyp ctxt qtys rty = |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
794 |
subst_typ ctxt (mk_ty_subst qtys false ctxt) rty |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
795 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
796 |
fun derive_qtrm ctxt qtys rtrm = |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
797 |
subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
798 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
799 |
(* derives a rtyp and rtrm out of a qtyp and qtrm, |
41444 | 800 |
respectively |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
801 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
802 |
fun derive_rtyp ctxt qtys qty = |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
803 |
subst_typ ctxt (mk_ty_subst qtys true ctxt) qty |
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
804 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
805 |
fun derive_rtrm ctxt qtys qtrm = |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
806 |
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
807 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
808 |
|
45279 | 809 |
end; |