author | bulwahn |
Thu, 17 Nov 2011 14:35:32 +0100 | |
changeset 45534 | 4ab21521b393 |
parent 45340 | 98ec8b51af9c |
child 45628 | f21eb7073895 |
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) |
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
|
128 |
| mk_dummyT _ = error "Expecting abs/rep term to be a constant" |
41444 | 129 |
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
|
130 |
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
|
131 |
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
|
132 |
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
|
133 |
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
|
134 |
| 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
|
135 |
| NONE => error ("No abs/rep terms for " ^ quote qty_str) |
41444 | 136 |
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
|
137 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
(* 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
|
139 |
fun absrep_const_chk flag ctxt qty_str = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
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
|
141 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
fun absrep_match_err ctxt ty_pat ty = |
41444 | 143 |
let |
144 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
145 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
146 |
in |
|
147 |
raise LIFT_MATCH (space_implode " " |
|
148 |
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
149 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
150 |
|
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 |
(** generation of an aggregate absrep function **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
153 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
(* - 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
|
155 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
- 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
|
157 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
- In case of function types we recurse taking |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
the polarity change into account. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
160 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
161 |
- 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
|
162 |
arguments and build the appropriate map function. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
- 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
|
165 |
instance of quotient types: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
166 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
- 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
|
168 |
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
|
169 |
must be some distinct TVars |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
170 |
- 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
|
171 |
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
|
172 |
- 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
|
173 |
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
|
174 |
assignments |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
175 |
- 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
|
176 |
which is an abstraction over all type variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
177 |
- finally we compose the result with the appropriate |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
178 |
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
|
179 |
a non-identity function / |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
180 |
otherwise we just return the appropriate absrep |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
181 |
function |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
182 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
183 |
The composition is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
184 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
185 |
('a list) list / ('a foo) foo |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
186 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
187 |
The matching is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
188 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
189 |
('a * 'a) list / 'a bar |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
190 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
191 |
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
|
192 |
identity maps. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
193 |
*) |
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 |
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
|
196 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
197 |
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
|
198 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
199 |
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
|
200 |
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
|
201 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
202 |
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
|
203 |
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => |
41444 | 204 |
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
|
205 |
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
|
206 |
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
|
207 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
208 |
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
|
209 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
210 |
(* 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
|
211 |
| (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
|
212 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
213 |
val arg = absrep_fun (negF flag) ctxt (ty, ty') |
41444 | 214 |
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
|
215 |
get_mapfun thy "Set.set" $ arg |
41444 | 216 |
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
|
217 |
| (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
|
218 |
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
|
219 |
then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
220 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
221 |
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
|
222 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
223 |
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
|
224 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
225 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
226 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
227 |
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
|
228 |
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
|
229 |
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
|
230 |
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
|
231 |
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
|
232 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
233 |
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
|
234 |
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
|
235 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
236 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
237 |
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
|
238 |
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
|
239 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
240 |
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
|
241 |
end |
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 |
| (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
|
244 |
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
|
245 |
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
|
246 |
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
|
247 |
| (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
|
248 |
| _ => 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
|
249 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
fun absrep_fun_chk flag ctxt (rty, qty) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
absrep_fun flag ctxt (rty, qty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
254 |
|
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 |
(*** Aggregate Equivalence Relation ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
259 |
|
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 |
(* works very similar to the absrep generation, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
262 |
except there is no need for polarities |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
263 |
*) |
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 |
(* 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
|
266 |
fun force_typ ctxt trm ty = |
41444 | 267 |
let |
42361 | 268 |
val thy = Proof_Context.theory_of ctxt |
41444 | 269 |
val trm_ty = fastype_of trm |
270 |
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
|
271 |
in |
|
272 |
map_types (Envir.subst_type ty_inst) trm |
|
273 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
274 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
275 |
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
|
276 |
| is_eq _ = false |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
277 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
278 |
fun mk_rel_compose (trm1, trm2) = |
35402 | 279 |
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
|
280 |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
281 |
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
|
282 |
(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
|
283 |
SOME map_data => Const (#relmap map_data, dummyT) |
45279 | 284 |
| 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
|
285 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
286 |
fun mk_relmap ctxt vs rty = |
41444 | 287 |
let |
288 |
val vs' = map (mk_Free) vs |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
289 |
|
41444 | 290 |
fun mk_relmap_aux rty = |
291 |
case rty of |
|
292 |
TVar _ => mk_Free rty |
|
293 |
| Type (_, []) => HOLogic.eq_const rty |
|
294 |
| Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys) |
|
295 |
| _ => raise LIFT_MATCH ("mk_relmap (default)") |
|
296 |
in |
|
297 |
fold_rev Term.lambda vs' (mk_relmap_aux rty) |
|
298 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
299 |
|
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
300 |
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
|
301 |
(case Quotient_Info.lookup_quotients thy s of |
45279 | 302 |
SOME qdata => #equiv_rel qdata |
303 |
| 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
|
304 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
305 |
fun equiv_match_err ctxt ty_pat ty = |
41444 | 306 |
let |
307 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
308 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
309 |
in |
|
310 |
raise LIFT_MATCH (space_implode " " |
|
311 |
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
312 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
313 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
314 |
(* builds the aggregate equivalence relation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
315 |
that will be the argument of Respects |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
316 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
317 |
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
|
318 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
319 |
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
|
320 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
321 |
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
|
322 |
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
|
323 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
324 |
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
|
325 |
(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
|
326 |
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
|
327 |
then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
328 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
329 |
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
|
330 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
331 |
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
|
332 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
333 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
334 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
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
|
338 |
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
|
339 |
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
|
340 |
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
|
341 |
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
|
342 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
343 |
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
|
344 |
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
|
345 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
346 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
347 |
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
|
348 |
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
|
349 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
350 |
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
|
351 |
end |
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 |
| _ => 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
|
354 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
355 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
356 |
fun equiv_relation_chk ctxt (rty, qty) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
357 |
equiv_relation ctxt (rty, qty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
358 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
359 |
|
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 |
(*** Regularization ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
363 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
364 |
(* Regularizing an rtrm means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
365 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
366 |
- Quantifiers over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
367 |
by bounded quantifiers, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
368 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
369 |
All P ----> All (Respects R) P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
370 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
371 |
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
|
372 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
373 |
- Abstractions over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
374 |
by bounded abstractions, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
375 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
376 |
%x. P ----> Ball (Respects R) %x. P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
377 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
378 |
- 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
|
379 |
corresponding equivalence relations, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
380 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
381 |
A = B ----> R A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
382 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
383 |
or |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
384 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
385 |
A = B ----> (R ===> R) A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
386 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
387 |
for more complicated types of A and B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
388 |
|
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 |
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
|
391 |
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
|
392 |
but also accepts partially regularized terms. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
393 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
394 |
This means that the raw theorems can have: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
395 |
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
|
396 |
in the places where: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
397 |
All, Ex, Ex1, %, (op =) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
398 |
is required the lifted theorem. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
399 |
|
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 |
val mk_babs = Const (@{const_name Babs}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
403 |
val mk_ball = Const (@{const_name Ball}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
404 |
val mk_bex = Const (@{const_name Bex}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
405 |
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
|
406 |
val mk_resp = Const (@{const_name Respects}, dummyT) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
407 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
408 |
(* - applies f to the subterm of an abstraction, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
409 |
otherwise to the given term, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
410 |
- used by regularize, therefore abstracted |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
411 |
variables do not have to be treated specially |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
412 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
413 |
fun apply_subt f (trm1, trm2) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
414 |
case (trm1, trm2) of |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
415 |
(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
|
416 |
| _ => f (trm1, trm2) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
417 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
418 |
fun term_mismatch str ctxt t1 t2 = |
41444 | 419 |
let |
420 |
val t1_str = Syntax.string_of_term ctxt t1 |
|
421 |
val t2_str = Syntax.string_of_term ctxt t2 |
|
422 |
val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
|
423 |
val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
|
424 |
in |
|
425 |
raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
|
426 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
427 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
428 |
(* the major type of All and Ex quantifiers *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
429 |
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
|
430 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
431 |
(* Checks that two types match, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
432 |
rty -> rty matches qty -> qty *) |
45280 | 433 |
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
|
434 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
435 |
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
|
436 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
437 |
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
|
438 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
439 |
(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
|
440 |
(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
|
441 |
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
|
442 |
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
|
443 |
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
|
444 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
445 |
(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
|
446 |
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
|
447 |
| 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
|
448 |
| _ => 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 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
450 |
|
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 |
(* produces a regularized version of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
453 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
454 |
- the result might contain dummyTs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
455 |
|
38718 | 456 |
- for regularization we do not need any |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
457 |
special treatment of bound variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
458 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
459 |
fun regularize_trm ctxt (rtrm, qtrm) = |
45280 | 460 |
(case (rtrm, qtrm) of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
461 |
(Abs (x, ty, t), Abs (_, ty', t')) => |
41444 | 462 |
let |
463 |
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
|
464 |
in |
|
465 |
if ty = ty' then subtrm |
|
466 |
else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
|
467 |
end |
|
45280 | 468 |
|
37677 | 469 |
| (Const (@{const_name Babs}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
41444 | 470 |
let |
471 |
val subtrm = regularize_trm ctxt (t, t') |
|
472 |
val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
|
473 |
in |
|
474 |
if resrel <> needres |
|
475 |
then term_mismatch "regularize (Babs)" ctxt resrel needres |
|
476 |
else mk_babs $ resrel $ subtrm |
|
477 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
478 |
|
37677 | 479 |
| (Const (@{const_name All}, ty) $ t, Const (@{const_name All}, ty') $ t') => |
41444 | 480 |
let |
481 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
482 |
in |
|
483 |
if ty = ty' then Const (@{const_name All}, ty) $ subtrm |
|
484 |
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
485 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
486 |
|
37677 | 487 |
| (Const (@{const_name Ex}, ty) $ t, Const (@{const_name Ex}, ty') $ t') => |
41444 | 488 |
let |
489 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
490 |
in |
|
491 |
if ty = ty' then Const (@{const_name Ex}, ty) $ subtrm |
|
492 |
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
493 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
494 |
|
37677 | 495 |
| (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
|
496 |
(Const (@{const_name HOL.conj}, _) $ (Const (@{const_name Set.member}, _) $ _ $ |
37677 | 497 |
(Const (@{const_name Respects}, _) $ resrel)) $ (t $ _)))), |
498 |
Const (@{const_name Ex1}, ty') $ t') => |
|
41444 | 499 |
let |
500 |
val t_ = incr_boundvars (~1) t |
|
501 |
val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
|
502 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
503 |
in |
|
504 |
if resrel <> needrel |
|
505 |
then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
506 |
else mk_bex1_rel $ resrel $ subtrm |
|
507 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
508 |
|
38558 | 509 |
| (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') => |
41444 | 510 |
let |
511 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
512 |
in |
|
513 |
if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm |
|
514 |
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
|
515 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
516 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
517 |
| (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
38558 | 518 |
Const (@{const_name All}, ty') $ t') => |
41444 | 519 |
let |
520 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
521 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
522 |
in |
|
523 |
if resrel <> needrel |
|
524 |
then term_mismatch "regularize (Ball)" ctxt resrel needrel |
|
525 |
else mk_ball $ (mk_resp $ resrel) $ subtrm |
|
526 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
527 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
528 |
| (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t, |
38558 | 529 |
Const (@{const_name Ex}, ty') $ t') => |
41444 | 530 |
let |
531 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
532 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
533 |
in |
|
534 |
if resrel <> needrel |
|
535 |
then term_mismatch "regularize (Bex)" ctxt resrel needrel |
|
536 |
else mk_bex $ (mk_resp $ resrel) $ subtrm |
|
537 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
538 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
539 |
| (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') => |
41444 | 540 |
let |
541 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
542 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
543 |
in |
|
544 |
if resrel <> needrel |
|
545 |
then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
|
546 |
else mk_bex1_rel $ resrel $ subtrm |
|
547 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
548 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
549 |
| (* equalities need to be replaced by appropriate equivalence relations *) |
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
550 |
(Const (@{const_name HOL.eq}, ty), Const (@{const_name HOL.eq}, ty')) => |
41444 | 551 |
if ty = ty' then rtrm |
552 |
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
|
553 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
554 |
| (* 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
|
555 |
(rel, Const (@{const_name HOL.eq}, ty')) => |
41444 | 556 |
let |
557 |
val rel_ty = fastype_of rel |
|
558 |
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
|
559 |
in |
|
560 |
if rel' aconv rel then rtrm |
|
561 |
else term_mismatch "regularize (relation mismatch)" ctxt rel rel' |
|
562 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
563 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
564 |
| (_, Const _) => |
41444 | 565 |
let |
42361 | 566 |
val thy = Proof_Context.theory_of ctxt |
45280 | 567 |
fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T' |
41444 | 568 |
| same_const _ _ = false |
569 |
in |
|
570 |
if same_const rtrm qtrm then rtrm |
|
571 |
else |
|
572 |
let |
|
45279 | 573 |
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
|
574 |
(case Quotient_Info.lookup_quotconsts_global thy qtrm of |
45279 | 575 |
SOME qconst_info => #rconst qconst_info |
576 |
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) |
|
41444 | 577 |
in |
578 |
if Pattern.matches thy (rtrm', rtrm) |
|
579 |
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
|
580 |
end |
|
581 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
582 |
|
37591 | 583 |
| (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
584 |
((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
|
585 |
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
|
586 |
|
37591 | 587 |
| (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)), |
588 |
((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
|
589 |
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
|
590 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
591 |
| (t1 $ t2, t1' $ t2') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
592 |
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
|
593 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
594 |
| (Bound i, Bound i') => |
41444 | 595 |
if i = i' then rtrm |
596 |
else raise (LIFT_MATCH "regularize (bounds mismatch)") |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
597 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
598 |
| _ => |
41444 | 599 |
let |
600 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
601 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
602 |
in |
|
603 |
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
|
45280 | 604 |
end) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
605 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
606 |
fun regularize_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
607 |
regularize_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
608 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
609 |
|
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 |
(*** Rep/Abs Injection ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
613 |
|
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 |
Injection of Rep/Abs means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
616 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
617 |
For abstractions: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
618 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
619 |
* 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
|
620 |
around the abstraction; otherwise we leave it unchanged. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
621 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
622 |
For applications: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
623 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
624 |
* 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
|
625 |
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
|
626 |
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
|
627 |
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
|
628 |
arguments. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
629 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
630 |
For constants: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
631 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
632 |
* 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
|
633 |
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
|
634 |
and Rep/Abs around it. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
635 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
636 |
For free variables: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
637 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
638 |
* 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
|
639 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
640 |
Vars case cannot occur. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
641 |
*) |
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 |
fun mk_repabs ctxt (T, T') trm = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
644 |
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
|
645 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
646 |
fun inj_repabs_err ctxt msg rtrm qtrm = |
41444 | 647 |
let |
648 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
649 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
650 |
in |
|
651 |
raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
|
652 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
653 |
|
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 |
(* bound variables need to be treated properly, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
656 |
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
|
657 |
fun inj_repabs_trm ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
658 |
case (rtrm, qtrm) of |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
659 |
(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
|
660 |
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
|
661 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
662 |
| (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
|
663 |
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
|
664 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
665 |
| (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
|
666 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
667 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
668 |
val qty = fastype_of qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
669 |
in |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
670 |
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
|
671 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
672 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
673 |
| (Abs (x, T, t), Abs (x', T', t')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
674 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
675 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
676 |
val qty = fastype_of qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
677 |
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
|
678 |
val (_, 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 yvar = Free (y, T) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
680 |
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
|
681 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
682 |
if rty = qty then result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
683 |
else mk_repabs ctxt (rty, qty) result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
684 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
685 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
686 |
| (t $ s, t' $ s') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
687 |
(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
|
688 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
689 |
| (Free (_, T), Free (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
690 |
if T = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
691 |
else mk_repabs ctxt (T, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
692 |
|
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38795
diff
changeset
|
693 |
| (_, Const (@{const_name HOL.eq}, _)) => rtrm |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
694 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
695 |
| (_, Const (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
696 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
697 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
698 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
699 |
if rty = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
700 |
else mk_repabs ctxt (rty, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
701 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
702 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
703 |
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
704 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
705 |
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
706 |
inj_repabs_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
707 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
708 |
|
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 |
(*** 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
|
712 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
713 |
(* 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
|
714 |
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
|
715 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
716 |
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
|
717 |
case rty of |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
718 |
Type (s, rtys) => |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
719 |
let |
42361 | 720 |
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
|
721 |
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
|
722 |
|
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
723 |
fun matches [] = rty' |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
724 |
| matches ((rty, qty)::tail) = |
45280 | 725 |
(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
|
726 |
NONE => matches tail |
45280 | 727 |
| 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
|
728 |
in |
41444 | 729 |
matches ty_subst |
730 |
end |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
731 |
| _ => rty |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
732 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
733 |
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
|
734 |
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
|
735 |
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
|
736 |
| 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
|
737 |
| 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
|
738 |
| 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
|
739 |
| Bound i => Bound i |
41444 | 740 |
| 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
|
741 |
let |
42361 | 742 |
val thy = Proof_Context.theory_of ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
743 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
744 |
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
|
745 |
| matches ((rconst, qconst)::tail) = |
45280 | 746 |
(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
|
747 |
NONE => matches tail |
45280 | 748 |
| 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
|
749 |
in |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
750 |
matches trm_subst |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
751 |
end |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
752 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
753 |
(* generate type and term substitutions out of the |
41444 | 754 |
qtypes involved in a quotient; the direction flag |
755 |
indicates in which direction the substitutions work: |
|
756 |
||
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
757 |
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
|
758 |
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
|
759 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
760 |
fun mk_ty_subst qtys direction ctxt = |
41444 | 761 |
let |
42361 | 762 |
val thy = Proof_Context.theory_of ctxt |
41444 | 763 |
in |
45279 | 764 |
Quotient_Info.dest_quotients ctxt |
41444 | 765 |
|> map (fn x => (#rtyp x, #qtyp x)) |
766 |
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) |
|
767 |
|> map (if direction then swap else I) |
|
768 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
769 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
770 |
fun mk_trm_subst qtys direction ctxt = |
41444 | 771 |
let |
772 |
val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) |
|
773 |
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
|
774 |
|
41444 | 775 |
val const_substs = |
45279 | 776 |
Quotient_Info.dest_quotconsts ctxt |
41444 | 777 |
|> map (fn x => (#rconst x, #qconst x)) |
778 |
|> 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
|
779 |
|
41444 | 780 |
val rel_substs = |
45279 | 781 |
Quotient_Info.dest_quotients ctxt |
41444 | 782 |
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) |
783 |
|> map (if direction then swap else I) |
|
784 |
in |
|
785 |
filter proper (const_substs @ rel_substs) |
|
786 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
787 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
788 |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
789 |
(* derives a qtyp and qtrm out of a rtyp and rtrm, |
41444 | 790 |
respectively |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
791 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
792 |
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
|
793 |
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
|
794 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
795 |
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
|
796 |
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
|
797 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
798 |
(* derives a rtyp and rtrm out of a qtyp and qtrm, |
41444 | 799 |
respectively |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
800 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
801 |
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
|
802 |
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
|
803 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
804 |
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
|
805 |
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
|
806 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
807 |
|
45279 | 808 |
end; |