author | wenzelm |
Fri, 15 Oct 2021 19:25:31 +0200 | |
changeset 74525 | c960bfcb91db |
parent 69593 | 3dda49e08b9d |
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 |
|
45797 | 14 |
val absrep_fun: Proof.context -> flag -> typ * typ -> term |
15 |
val absrep_fun_chk: Proof.context -> flag -> typ * typ -> term |
|
35222
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 *) |
45797 | 18 |
val absrep_const_chk: Proof.context -> flag -> string -> term |
35222
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 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
23 |
val get_rel_from_quot_thm: thm -> term |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47308
diff
changeset
|
24 |
val prove_quot_thm: Proof.context -> typ * typ -> thm |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
25 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
val regularize_trm: Proof.context -> term * term -> term |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
27 |
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
|
28 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
29 |
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
|
30 |
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
|
31 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
32 |
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
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
end; |
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 |
structure Quotient_Term: QUOTIENT_TERM = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
39 |
struct |
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 |
exception LIFT_MATCH of string |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
42 |
|
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 |
(*** Aggregate Rep/Abs Function ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
46 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
47 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
48 |
(* 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
|
49 |
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
|
50 |
treated specially, since there the polarity changes. |
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 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
53 |
datatype flag = AbsF | RepF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
54 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
55 |
fun negF AbsF = RepF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
56 |
| negF RepF = AbsF |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
57 |
|
69593 | 58 |
fun is_identity (Const (\<^const_name>\<open>id\<close>, _)) = true |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
59 |
| is_identity _ = false |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
60 |
|
69593 | 61 |
fun mk_identity ty = Const (\<^const_name>\<open>id\<close>, ty --> ty) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
62 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
63 |
fun mk_fun_compose flag (trm1, trm2) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
64 |
case flag of |
69593 | 65 |
AbsF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm1 $ trm2 |
66 |
| RepF => Const (\<^const_name>\<open>comp\<close>, dummyT) $ trm2 $ trm1 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
67 |
|
45796 | 68 |
fun get_mapfun_data ctxt s = |
55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55414
diff
changeset
|
69 |
(case Symtab.lookup (Functor.entries ctxt) s of |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
70 |
SOME [map_data] => (case try dest_Const (#mapper map_data) of |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
71 |
SOME (c, _) => (Const (c, dummyT), #variances map_data) |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
72 |
| NONE => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is not a constant.")) |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
73 |
| SOME _ => raise LIFT_MATCH ("map function for type " ^ quote s ^ " is non-singleton entry.") |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
74 |
| 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
|
75 |
|
55467
a5c9002bc54d
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
blanchet
parents:
55414
diff
changeset
|
76 |
fun defined_mapfun_data ctxt = Symtab.defined (Functor.entries ctxt) |
35222
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 |
(* looks up the (varified) rty and qty for |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
79 |
a quotient definition |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
80 |
*) |
45796 | 81 |
fun get_rty_qty ctxt s = |
82 |
let |
|
83 |
val thy = Proof_Context.theory_of ctxt |
|
84 |
in |
|
85 |
(case Quotient_Info.lookup_quotients_global thy s of |
|
67632 | 86 |
SOME {rtyp, qtyp, ...} => (rtyp, qtyp) |
45796 | 87 |
| NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")) |
88 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
89 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
90 |
(* matches a type pattern with a type *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
91 |
fun match ctxt err ty_pat ty = |
41444 | 92 |
let |
42361 | 93 |
val thy = Proof_Context.theory_of ctxt |
41444 | 94 |
in |
95 |
Sign.typ_match thy (ty_pat, ty) Vartab.empty |
|
96 |
handle Type.TYPE_MATCH => err ctxt ty_pat ty |
|
97 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
98 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
99 |
(* produces the rep or abs constant for a qty *) |
45797 | 100 |
fun absrep_const ctxt flag qty_str = |
41444 | 101 |
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
|
102 |
(* 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
|
103 |
fun mk_dummyT (Const (c, _)) = Const (c, dummyT) |
45628
f21eb7073895
in a local context, also the free variable case needs to be analysed default tip
Christian Urban <urbanc@in.tum.de>
parents:
45534
diff
changeset
|
104 |
| mk_dummyT (Free (c, _)) = Free (c, dummyT) |
f21eb7073895
in a local context, also the free variable case needs to be analysed default tip
Christian Urban <urbanc@in.tum.de>
parents:
45534
diff
changeset
|
105 |
| mk_dummyT _ = error "Expecting abs/rep term to be a constant or a free variable" |
41444 | 106 |
in |
67632 | 107 |
(case Quotient_Info.lookup_abs_rep ctxt qty_str of |
108 |
SOME {abs, rep} => mk_dummyT (case flag of AbsF => abs | RepF => rep) |
|
109 |
| NONE => error ("No abs/rep terms for " ^ quote qty_str)) |
|
41444 | 110 |
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
|
111 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
112 |
(* Lets Nitpick represent elements of quotient types as elements of the raw type *) |
45797 | 113 |
fun absrep_const_chk ctxt flag qty_str = |
114 |
Syntax.check_term ctxt (absrep_const ctxt flag qty_str) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
115 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
116 |
fun absrep_match_err ctxt ty_pat ty = |
41444 | 117 |
let |
118 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
119 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
120 |
in |
|
121 |
raise LIFT_MATCH (space_implode " " |
|
122 |
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
123 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
124 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
125 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
126 |
(** generation of an aggregate absrep function **) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
128 |
(* - 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
|
129 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
- 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
|
131 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
132 |
- In case of function types we recurse taking |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
133 |
the polarity change into account. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
134 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
135 |
- 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
|
136 |
arguments and build the appropriate map function. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
137 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
138 |
- 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
|
139 |
instance of quotient types: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
140 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
141 |
- 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
|
142 |
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
|
143 |
must be some distinct TVars |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
144 |
- 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
|
145 |
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
|
146 |
- 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
|
147 |
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
|
148 |
assignments |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
149 |
- 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
|
150 |
which is an abstraction over all type variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
151 |
- finally we compose the result with the appropriate |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
152 |
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
|
153 |
a non-identity function / |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
154 |
otherwise we just return the appropriate absrep |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
155 |
function |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
156 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
157 |
The composition is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
158 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
159 |
('a list) list / ('a foo) foo |
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 |
The matching is necessary for types like |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
('a * 'a) list / 'a bar |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
164 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
165 |
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
|
166 |
identity maps. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
167 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
168 |
|
45797 | 169 |
fun absrep_fun ctxt flag (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
|
170 |
let |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
171 |
fun absrep_args tys tys' variances = |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
172 |
let |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
173 |
fun absrep_arg (types, (_, variant)) = |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
174 |
(case variant of |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
175 |
(false, false) => [] |
45797 | 176 |
| (true, false) => [(absrep_fun ctxt flag types)] |
177 |
| (false, true) => [(absrep_fun ctxt (negF flag) types)] |
|
178 |
| (true, true) => [(absrep_fun ctxt flag types),(absrep_fun ctxt (negF flag) types)]) |
|
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
179 |
in |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
180 |
maps absrep_arg ((tys ~~ tys') ~~ variances) |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
181 |
end |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
182 |
fun test_identities tys rtys' s s' = |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
183 |
let |
45797 | 184 |
val args = map (absrep_fun ctxt flag) (tys ~~ rtys') |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
185 |
in |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
186 |
if forall is_identity args |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
187 |
then |
45797 | 188 |
absrep_const ctxt flag s' |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
189 |
else |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
190 |
raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
191 |
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
|
192 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
193 |
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
|
194 |
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
|
195 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
196 |
case (rty, qty) of |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
197 |
(Type (s, tys), Type (s', tys')) => |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
198 |
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
|
199 |
then |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
200 |
let |
45796 | 201 |
val (map_fun, variances) = get_mapfun_data ctxt s |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
202 |
val args = absrep_args tys tys' variances |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
203 |
in |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
204 |
list_comb (map_fun, args) |
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 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
206 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
207 |
let |
45796 | 208 |
val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
209 |
val qtyenv = match ctxt absrep_match_err qty_pat qty |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
210 |
val rtys' = map (Envir.subst_type qtyenv) rtys |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
211 |
in |
45796 | 212 |
if not (defined_mapfun_data ctxt s) |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
213 |
then |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
214 |
(* |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
215 |
If we don't know a map function for the raw type, |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
216 |
we are not necessarilly in troubles because |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
217 |
it can still be the case we don't need the map |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
218 |
function <=> all abs/rep functions are identities. |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
219 |
*) |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
220 |
test_identities tys rtys' s s' |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
221 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
222 |
let |
45796 | 223 |
val (map_fun, variances) = get_mapfun_data ctxt s |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
224 |
val args = absrep_args tys rtys' variances |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
225 |
in |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
226 |
if forall is_identity args |
45797 | 227 |
then absrep_const ctxt flag s' |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
228 |
else |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
229 |
let |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
230 |
val result = list_comb (map_fun, args) |
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
231 |
in |
45797 | 232 |
mk_fun_compose flag (absrep_const ctxt flag s', result) |
45795
2d8949268303
maps are taken from enriched type infrastracture, rewritten lifting of constants, now we can lift even contravariant and co/contravariant types
kuncar
parents:
45628
diff
changeset
|
233 |
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
|
234 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
235 |
end |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
236 |
| (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
|
237 |
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
|
238 |
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
|
239 |
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
|
240 |
| (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
|
241 |
| _ => 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
|
242 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
243 |
|
45797 | 244 |
fun absrep_fun_chk ctxt flag (rty, qty) = |
245 |
absrep_fun ctxt flag (rty, qty) |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
246 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
247 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
248 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
249 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
250 |
(*** Aggregate Equivalence Relation ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
252 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
253 |
(* works very similar to the absrep generation, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
254 |
except there is no need for polarities |
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 |
(* 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
|
258 |
fun force_typ ctxt trm ty = |
41444 | 259 |
let |
42361 | 260 |
val thy = Proof_Context.theory_of ctxt |
41444 | 261 |
val trm_ty = fastype_of trm |
262 |
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty |
|
263 |
in |
|
264 |
map_types (Envir.subst_type ty_inst) trm |
|
265 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
266 |
|
69593 | 267 |
fun is_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _)) = true |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
268 |
| is_eq _ = false |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
269 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
270 |
fun mk_rel_compose (trm1, trm2) = |
69593 | 271 |
Const (\<^const_abbrev>\<open>rel_conj\<close>, dummyT) $ trm1 $ trm2 |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
272 |
|
67632 | 273 |
fun get_relmap ctxt s = |
274 |
(case Quotient_Info.lookup_quotmaps ctxt s of |
|
275 |
SOME {relmap, ...} => Const (relmap, dummyT) |
|
45279 | 276 |
| 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
|
277 |
|
67632 | 278 |
fun get_equiv_rel ctxt s = |
279 |
(case Quotient_Info.lookup_quotients ctxt s of |
|
280 |
SOME {equiv_rel, ...} => equiv_rel |
|
47095
b43ddeea727f
simplified code of generation of aggregate relations
kuncar
parents:
46416
diff
changeset
|
281 |
| NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")")) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
282 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
283 |
fun equiv_match_err ctxt ty_pat ty = |
41444 | 284 |
let |
285 |
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat |
|
286 |
val ty_str = Syntax.string_of_typ ctxt ty |
|
287 |
in |
|
288 |
raise LIFT_MATCH (space_implode " " |
|
289 |
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
|
290 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
291 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
292 |
(* builds the aggregate equivalence relation |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
293 |
that will be the argument of Respects |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
294 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
295 |
fun equiv_relation ctxt (rty, qty) = |
45796 | 296 |
if rty = qty |
297 |
then HOLogic.eq_const rty |
|
298 |
else |
|
299 |
case (rty, qty) of |
|
300 |
(Type (s, tys), Type (s', tys')) => |
|
301 |
if s = s' |
|
302 |
then |
|
303 |
let |
|
304 |
val args = map (equiv_relation ctxt) (tys ~~ tys') |
|
305 |
in |
|
306 |
list_comb (get_relmap ctxt s, args) |
|
307 |
end |
|
308 |
else |
|
309 |
let |
|
47095
b43ddeea727f
simplified code of generation of aggregate relations
kuncar
parents:
46416
diff
changeset
|
310 |
val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' |
45796 | 311 |
val qtyenv = match ctxt equiv_match_err qty_pat qty |
47095
b43ddeea727f
simplified code of generation of aggregate relations
kuncar
parents:
46416
diff
changeset
|
312 |
val rtys' = map (Envir.subst_type qtyenv) rtys |
b43ddeea727f
simplified code of generation of aggregate relations
kuncar
parents:
46416
diff
changeset
|
313 |
val args = map (equiv_relation ctxt) (tys ~~ rtys') |
45796 | 314 |
val eqv_rel = get_equiv_rel ctxt s' |
69593 | 315 |
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> \<^typ>\<open>bool\<close>) |
45796 | 316 |
in |
317 |
if forall is_eq args |
|
318 |
then eqv_rel' |
|
319 |
else |
|
320 |
let |
|
47095
b43ddeea727f
simplified code of generation of aggregate relations
kuncar
parents:
46416
diff
changeset
|
321 |
val result = list_comb (get_relmap ctxt s, args) |
45796 | 322 |
in |
323 |
mk_rel_compose (result, eqv_rel') |
|
324 |
end |
|
325 |
end |
|
326 |
| _ => HOLogic.eq_const rty |
|
327 |
||
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
328 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
329 |
fun equiv_relation_chk ctxt (rty, qty) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
330 |
equiv_relation ctxt (rty, qty) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
331 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
332 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
333 |
(* generation of the Quotient theorem *) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
334 |
|
47106
dfa5ed8d94b4
use Thm.transfer for thms stored in generic context data storage
kuncar
parents:
47096
diff
changeset
|
335 |
exception CODE_GEN of string |
dfa5ed8d94b4
use Thm.transfer for thms stored in generic context data storage
kuncar
parents:
47096
diff
changeset
|
336 |
|
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
337 |
fun get_quot_thm ctxt s = |
67633
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
338 |
(case Quotient_Info.lookup_quotients ctxt s of |
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
339 |
SOME {quot_thm, ...} => quot_thm |
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
340 |
| NONE => raise CODE_GEN ("No quotient type " ^ quote s ^ " found.")); |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
341 |
|
47106
dfa5ed8d94b4
use Thm.transfer for thms stored in generic context data storage
kuncar
parents:
47096
diff
changeset
|
342 |
fun get_rel_quot_thm ctxt s = |
67633
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
343 |
(case Quotient_Info.lookup_quotmaps ctxt s of |
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
344 |
SOME {quot_thm, ...} => quot_thm |
9a1212f4393e
clarified data operations, with trim_context and transfer;
wenzelm
parents:
67632
diff
changeset
|
345 |
| NONE => raise CODE_GEN ("get_relmap (no relation map function found for type " ^ s ^ ")")); |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
346 |
|
59848 | 347 |
fun is_id_quot thm = Thm.eq_thm_prop (thm, @{thm identity_quotient3}) |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
348 |
|
47698 | 349 |
open Lifting_Util |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
350 |
|
47698 | 351 |
infix 0 MRSL |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
352 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
353 |
exception NOT_IMPL of string |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
354 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
355 |
fun get_rel_from_quot_thm quot_thm = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
356 |
let |
59582 | 357 |
val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o Thm.prop_of) quot_thm |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
358 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
359 |
rel |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
360 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
361 |
|
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
362 |
fun mk_quot_thm_compose (rel_quot_thm, quot_thm) = |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
363 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
364 |
val quot_thm_rel = get_rel_from_quot_thm quot_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
365 |
in |
47308 | 366 |
if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient3} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
367 |
else raise NOT_IMPL "nested quotients: not implemented yet" |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
368 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
369 |
|
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47308
diff
changeset
|
370 |
fun prove_quot_thm ctxt (rty, qty) = |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
371 |
if rty = qty |
47308 | 372 |
then @{thm identity_quotient3} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
373 |
else |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
374 |
case (rty, qty) of |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
375 |
(Type (s, tys), Type (s', tys')) => |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
376 |
if s = s' |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
377 |
then |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
378 |
let |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47308
diff
changeset
|
379 |
val args = map (prove_quot_thm ctxt) (tys ~~ tys') |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
380 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
381 |
args MRSL (get_rel_quot_thm ctxt s) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
382 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
383 |
else |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
384 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
385 |
val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s' |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
386 |
val qtyenv = match ctxt equiv_match_err qty_pat qty |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
387 |
val rtys' = map (Envir.subst_type qtyenv) rtys |
47504
aa1b8a59017f
go back to the explicit compisition of quotient theorems
kuncar
parents:
47308
diff
changeset
|
388 |
val args = map (prove_quot_thm ctxt) (tys ~~ rtys') |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
389 |
val quot_thm = get_quot_thm ctxt s' |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
390 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
391 |
if forall is_id_quot args |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
392 |
then |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
393 |
quot_thm |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
394 |
else |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
395 |
let |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
396 |
val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
397 |
in |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
398 |
mk_quot_thm_compose (rel_quot_thm, quot_thm) |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
399 |
end |
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
400 |
end |
47308 | 401 |
| _ => @{thm identity_quotient3} |
47096
3ea48c19673e
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents:
47095
diff
changeset
|
402 |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
403 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
404 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
405 |
(*** Regularization ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
406 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
407 |
(* Regularizing an rtrm means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
408 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
409 |
- Quantifiers over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
410 |
by bounded quantifiers, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
411 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
412 |
All P ----> All (Respects R) P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
413 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
414 |
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
|
415 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
416 |
- Abstractions over types that need lifting are replaced |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
417 |
by bounded abstractions, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
418 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
419 |
%x. P ----> Ball (Respects R) %x. P |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
420 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
421 |
- 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
|
422 |
corresponding equivalence relations, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
423 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
424 |
A = B ----> R A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
425 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
426 |
or |
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 |
A = B ----> (R ===> R) A B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
429 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
430 |
for more complicated types of A and B |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
431 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
432 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
433 |
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
|
434 |
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
|
435 |
but also accepts partially regularized terms. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
436 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
437 |
This means that the raw theorems can have: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
438 |
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
|
439 |
in the places where: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
440 |
All, Ex, Ex1, %, (op =) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
441 |
is required the lifted theorem. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
442 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
443 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
444 |
|
69593 | 445 |
val mk_babs = Const (\<^const_name>\<open>Babs\<close>, dummyT) |
446 |
val mk_ball = Const (\<^const_name>\<open>Ball\<close>, dummyT) |
|
447 |
val mk_bex = Const (\<^const_name>\<open>Bex\<close>, dummyT) |
|
448 |
val mk_bex1_rel = Const (\<^const_name>\<open>Bex1_rel\<close>, dummyT) |
|
449 |
val mk_resp = Const (\<^const_name>\<open>Respects\<close>, dummyT) |
|
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 |
(* - applies f to the subterm of an abstraction, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
452 |
otherwise to the given term, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
453 |
- used by regularize, therefore abstracted |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
454 |
variables do not have to be treated specially |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
455 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
456 |
fun apply_subt f (trm1, trm2) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
457 |
case (trm1, trm2) of |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
458 |
(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
|
459 |
| _ => f (trm1, trm2) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
460 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
461 |
fun term_mismatch str ctxt t1 t2 = |
41444 | 462 |
let |
463 |
val t1_str = Syntax.string_of_term ctxt t1 |
|
464 |
val t2_str = Syntax.string_of_term ctxt t2 |
|
465 |
val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1) |
|
466 |
val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2) |
|
467 |
in |
|
468 |
raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str]) |
|
469 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
470 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
471 |
(* the major type of All and Ex quantifiers *) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
472 |
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
|
473 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
474 |
(* Checks that two types match, for example: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
475 |
rty -> rty matches qty -> qty *) |
45280 | 476 |
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
|
477 |
let |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
478 |
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
|
479 |
in |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
480 |
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
|
481 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
482 |
(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
|
483 |
(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
|
484 |
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
|
485 |
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
|
486 |
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
|
487 |
else |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
488 |
(case Quotient_Info.lookup_quotients_global thy qs of |
67632 | 489 |
SOME {rtyp, ...} => Sign.typ_instance thy (rT, rtyp) |
45340
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
490 |
| 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
|
491 |
| _ => false) |
98ec8b51af9c
prefer global Quotient_Info lookup to accomodate Quotient_Term, which is not quite localized yet (cf. 9fd6fce8a230);
wenzelm
parents:
45280
diff
changeset
|
492 |
end |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
493 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
494 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
495 |
(* produces a regularized version of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
496 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
497 |
- the result might contain dummyTs |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
498 |
|
38718 | 499 |
- for regularization we do not need any |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
500 |
special treatment of bound variables |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
501 |
*) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
502 |
fun regularize_trm ctxt (rtrm, qtrm) = |
45280 | 503 |
(case (rtrm, qtrm) of |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
504 |
(Abs (x, ty, t), Abs (_, ty', t')) => |
41444 | 505 |
let |
506 |
val subtrm = Abs(x, ty, regularize_trm ctxt (t, t')) |
|
507 |
in |
|
508 |
if ty = ty' then subtrm |
|
509 |
else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm |
|
510 |
end |
|
45280 | 511 |
|
69593 | 512 |
| (Const (\<^const_name>\<open>Babs\<close>, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) => |
41444 | 513 |
let |
514 |
val subtrm = regularize_trm ctxt (t, t') |
|
515 |
val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty') |
|
516 |
in |
|
517 |
if resrel <> needres |
|
518 |
then term_mismatch "regularize (Babs)" ctxt resrel needres |
|
519 |
else mk_babs $ resrel $ subtrm |
|
520 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
521 |
|
69593 | 522 |
| (Const (\<^const_name>\<open>All\<close>, ty) $ t, Const (\<^const_name>\<open>All\<close>, ty') $ t') => |
41444 | 523 |
let |
524 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
525 |
in |
|
69593 | 526 |
if ty = ty' then Const (\<^const_name>\<open>All\<close>, ty) $ subtrm |
41444 | 527 |
else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
528 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
529 |
|
69593 | 530 |
| (Const (\<^const_name>\<open>Ex\<close>, ty) $ t, Const (\<^const_name>\<open>Ex\<close>, ty') $ t') => |
41444 | 531 |
let |
532 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
533 |
in |
|
69593 | 534 |
if ty = ty' then Const (\<^const_name>\<open>Ex\<close>, ty) $ subtrm |
41444 | 535 |
else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
536 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
537 |
|
69593 | 538 |
| (Const (\<^const_name>\<open>Ex1\<close>, ty) $ (Abs (_, _, |
539 |
(Const (\<^const_name>\<open>HOL.conj\<close>, _) $ (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ |
|
540 |
(Const (\<^const_name>\<open>Respects\<close>, _) $ resrel)) $ (t $ _)))), |
|
541 |
Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
|
41444 | 542 |
let |
543 |
val t_ = incr_boundvars (~1) t |
|
544 |
val subtrm = apply_subt (regularize_trm ctxt) (t_, t') |
|
545 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
546 |
in |
|
547 |
if resrel <> needrel |
|
548 |
then term_mismatch "regularize (Bex1)" ctxt resrel needrel |
|
549 |
else mk_bex1_rel $ resrel $ subtrm |
|
550 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
551 |
|
69593 | 552 |
| (Const (\<^const_name>\<open>Ex1\<close>, ty) $ t, Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
41444 | 553 |
let |
554 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
555 |
in |
|
69593 | 556 |
if ty = ty' then Const (\<^const_name>\<open>Ex1\<close>, ty) $ subtrm |
41444 | 557 |
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm |
558 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
559 |
|
69593 | 560 |
| (Const (\<^const_name>\<open>Ball\<close>, ty) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ resrel) $ t, |
561 |
Const (\<^const_name>\<open>All\<close>, ty') $ t') => |
|
41444 | 562 |
let |
563 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
564 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
565 |
in |
|
566 |
if resrel <> needrel |
|
567 |
then term_mismatch "regularize (Ball)" ctxt resrel needrel |
|
568 |
else mk_ball $ (mk_resp $ resrel) $ subtrm |
|
569 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
570 |
|
69593 | 571 |
| (Const (\<^const_name>\<open>Bex\<close>, ty) $ (Const (\<^const_name>\<open>Respects\<close>, _) $ resrel) $ t, |
572 |
Const (\<^const_name>\<open>Ex\<close>, ty') $ t') => |
|
41444 | 573 |
let |
574 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
575 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
576 |
in |
|
577 |
if resrel <> needrel |
|
578 |
then term_mismatch "regularize (Bex)" ctxt resrel needrel |
|
579 |
else mk_bex $ (mk_resp $ resrel) $ subtrm |
|
580 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
581 |
|
69593 | 582 |
| (Const (\<^const_name>\<open>Bex1_rel\<close>, ty) $ resrel $ t, Const (\<^const_name>\<open>Ex1\<close>, ty') $ t') => |
41444 | 583 |
let |
584 |
val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
585 |
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty') |
|
586 |
in |
|
587 |
if resrel <> needrel |
|
588 |
then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel |
|
589 |
else mk_bex1_rel $ resrel $ subtrm |
|
590 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
591 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
592 |
| (* equalities need to be replaced by appropriate equivalence relations *) |
69593 | 593 |
(Const (\<^const_name>\<open>HOL.eq\<close>, ty), Const (\<^const_name>\<open>HOL.eq\<close>, ty')) => |
41444 | 594 |
if ty = ty' then rtrm |
595 |
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
|
596 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
597 |
| (* in this case we just check whether the given equivalence relation is correct *) |
69593 | 598 |
(rel, Const (\<^const_name>\<open>HOL.eq\<close>, ty')) => |
41444 | 599 |
let |
600 |
val rel_ty = fastype_of rel |
|
601 |
val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') |
|
602 |
in |
|
603 |
if rel' aconv rel then rtrm |
|
604 |
else term_mismatch "regularize (relation mismatch)" ctxt rel rel' |
|
605 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
606 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
607 |
| (_, Const _) => |
41444 | 608 |
let |
42361 | 609 |
val thy = Proof_Context.theory_of ctxt |
45280 | 610 |
fun same_const (Const (s, T)) (Const (s', T')) = s = s' andalso matches_typ ctxt T T' |
41444 | 611 |
| same_const _ _ = false |
612 |
in |
|
613 |
if same_const rtrm qtrm then rtrm |
|
614 |
else |
|
615 |
let |
|
45279 | 616 |
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
|
617 |
(case Quotient_Info.lookup_quotconsts_global thy qtrm of |
67632 | 618 |
SOME {rconst, ...} => rconst |
45279 | 619 |
| NONE => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm) |
41444 | 620 |
in |
621 |
if Pattern.matches thy (rtrm', rtrm) |
|
622 |
then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm |
|
623 |
end |
|
624 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
625 |
|
69593 | 626 |
| (((t1 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v1, ty, Abs(v1', ty', s1))), |
627 |
((t2 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) => |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
628 |
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
|
629 |
|
69593 | 630 |
| (((t1 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v1, ty, s1)), |
631 |
((t2 as Const (\<^const_name>\<open>case_prod\<close>, _)) $ Abs (v2, _ , s2))) => |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
632 |
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
|
633 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
634 |
| (t1 $ t2, t1' $ t2') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
635 |
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
|
636 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
637 |
| (Bound i, Bound i') => |
41444 | 638 |
if i = i' then rtrm |
639 |
else raise (LIFT_MATCH "regularize (bounds mismatch)") |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
640 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
641 |
| _ => |
41444 | 642 |
let |
643 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
644 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
645 |
in |
|
646 |
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")")) |
|
45280 | 647 |
end) |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
648 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
649 |
fun regularize_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
650 |
regularize_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
651 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
652 |
|
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 |
(*** Rep/Abs Injection ***) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
656 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
657 |
(* |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
658 |
Injection of Rep/Abs means: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
659 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
660 |
For abstractions: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
661 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
662 |
* 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
|
663 |
around the abstraction; otherwise we leave it unchanged. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
664 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
665 |
For applications: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
666 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
667 |
* 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
|
668 |
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
|
669 |
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
|
670 |
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
|
671 |
arguments. |
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 |
For constants: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
674 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
675 |
* 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
|
676 |
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
|
677 |
and Rep/Abs around it. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
678 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
679 |
For free variables: |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
680 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
681 |
* 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
|
682 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
683 |
Vars case cannot occur. |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
684 |
*) |
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 |
fun mk_repabs ctxt (T, T') trm = |
45797 | 687 |
absrep_fun ctxt RepF (T, T') $ (absrep_fun ctxt AbsF (T, T') $ trm) |
35222
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 |
fun inj_repabs_err ctxt msg rtrm qtrm = |
41444 | 690 |
let |
691 |
val rtrm_str = Syntax.string_of_term ctxt rtrm |
|
692 |
val qtrm_str = Syntax.string_of_term ctxt qtrm |
|
693 |
in |
|
694 |
raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str]) |
|
695 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
696 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
697 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
698 |
(* bound variables need to be treated properly, |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
699 |
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
|
700 |
fun inj_repabs_trm ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
701 |
case (rtrm, qtrm) of |
69593 | 702 |
(Const (\<^const_name>\<open>Ball\<close>, T) $ r $ t, Const (\<^const_name>\<open>All\<close>, _) $ t') => |
703 |
Const (\<^const_name>\<open>Ball\<close>, 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
|
704 |
|
69593 | 705 |
| (Const (\<^const_name>\<open>Bex\<close>, T) $ r $ t, Const (\<^const_name>\<open>Ex\<close>, _) $ t') => |
706 |
Const (\<^const_name>\<open>Bex\<close>, 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
|
707 |
|
69593 | 708 |
| (Const (\<^const_name>\<open>Babs\<close>, T) $ r $ t, t' as (Abs _)) => |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
709 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
710 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
711 |
val qty = fastype_of qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
712 |
in |
69593 | 713 |
mk_repabs ctxt (rty, qty) (Const (\<^const_name>\<open>Babs\<close>, 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
|
714 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
715 |
|
74525
c960bfcb91db
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents:
69593
diff
changeset
|
716 |
| (t as Abs _, t' as Abs _) => |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
717 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
718 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
719 |
val qty = fastype_of qtrm |
74525
c960bfcb91db
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents:
69593
diff
changeset
|
720 |
val ((y, T), s) = Term.dest_abs_global t |
c960bfcb91db
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
wenzelm
parents:
69593
diff
changeset
|
721 |
val (_, s') = Term.dest_abs_global t' |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
722 |
val yvar = Free (y, T) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
723 |
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
|
724 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
725 |
if rty = qty then result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
726 |
else mk_repabs ctxt (rty, qty) result |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
727 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
728 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
729 |
| (t $ s, t' $ s') => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
730 |
(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
|
731 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
732 |
| (Free (_, T), Free (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
733 |
if T = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
734 |
else mk_repabs ctxt (T, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
735 |
|
69593 | 736 |
| (_, Const (\<^const_name>\<open>HOL.eq\<close>, _)) => rtrm |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
737 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
738 |
| (_, Const (_, T')) => |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
739 |
let |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
740 |
val rty = fastype_of rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
741 |
in |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
742 |
if rty = T' then rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
743 |
else mk_repabs ctxt (rty, T') rtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
744 |
end |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
745 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
746 |
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
747 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
748 |
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) = |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
749 |
inj_repabs_trm ctxt (rtrm, qtrm) |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
750 |
|> Syntax.check_term ctxt |
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
751 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
752 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
753 |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
754 |
(*** 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
|
755 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
756 |
(* 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
|
757 |
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
|
758 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
759 |
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
|
760 |
case rty of |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
761 |
Type (s, rtys) => |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
762 |
let |
42361 | 763 |
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
|
764 |
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
|
765 |
|
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
766 |
fun matches [] = rty' |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
767 |
| matches ((rty, qty)::tail) = |
45280 | 768 |
(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
|
769 |
NONE => matches tail |
46416
5f5665a0b973
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
45797
diff
changeset
|
770 |
| SOME inst => subst_typ ctxt ty_subst (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
|
771 |
in |
41444 | 772 |
matches ty_subst |
773 |
end |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
774 |
| _ => rty |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
775 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
776 |
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
|
777 |
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
|
778 |
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
|
779 |
| 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
|
780 |
| 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
|
781 |
| 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
|
782 |
| Bound i => Bound i |
41444 | 783 |
| 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
|
784 |
let |
42361 | 785 |
val thy = Proof_Context.theory_of ctxt |
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
786 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
787 |
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
|
788 |
| matches ((rconst, qconst)::tail) = |
45280 | 789 |
(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
|
790 |
NONE => matches tail |
46416
5f5665a0b973
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
45797
diff
changeset
|
791 |
| SOME inst => subst_trm ctxt ty_subst trm_subst (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
|
792 |
in |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
793 |
matches trm_subst |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
794 |
end |
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
795 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
796 |
(* generate type and term substitutions out of the |
41444 | 797 |
qtypes involved in a quotient; the direction flag |
798 |
indicates in which direction the substitutions work: |
|
799 |
||
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
800 |
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
|
801 |
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
|
802 |
*) |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
803 |
fun mk_ty_subst qtys direction ctxt = |
41444 | 804 |
let |
42361 | 805 |
val thy = Proof_Context.theory_of ctxt |
41444 | 806 |
in |
45279 | 807 |
Quotient_Info.dest_quotients ctxt |
41444 | 808 |
|> map (fn x => (#rtyp x, #qtyp x)) |
809 |
|> filter (fn (_, qty) => member (Sign.typ_instance thy o swap) qtys qty) |
|
810 |
|> map (if direction then swap else I) |
|
811 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
812 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
813 |
fun mk_trm_subst qtys direction ctxt = |
41444 | 814 |
let |
815 |
val subst_typ' = subst_typ ctxt (mk_ty_subst qtys direction ctxt) |
|
816 |
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
|
817 |
|
41444 | 818 |
val const_substs = |
45279 | 819 |
Quotient_Info.dest_quotconsts ctxt |
41444 | 820 |
|> map (fn x => (#rconst x, #qconst x)) |
821 |
|> 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
|
822 |
|
41444 | 823 |
val rel_substs = |
45279 | 824 |
Quotient_Info.dest_quotients ctxt |
41444 | 825 |
|> map (fn x => (#equiv_rel x, HOLogic.eq_const (#qtyp x))) |
826 |
|> map (if direction then swap else I) |
|
827 |
in |
|
828 |
filter proper (const_substs @ rel_substs) |
|
829 |
end |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
830 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
831 |
|
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
832 |
(* derives a qtyp and qtrm out of a rtyp and rtrm, |
41444 | 833 |
respectively |
37560
1b5bbc4a14bc
streamlined the generation of quotient theorems out of raw theorems
Christian Urban <urbanc@in.tum.de>
parents:
37532
diff
changeset
|
834 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
835 |
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
|
836 |
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
|
837 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
838 |
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
|
839 |
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
|
840 |
|
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
841 |
(* derives a rtyp and rtrm out of a qtyp and qtrm, |
41444 | 842 |
respectively |
37592
e16495cfdde0
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
Christian Urban <urbanc@in.tum.de>
parents:
37591
diff
changeset
|
843 |
*) |
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
844 |
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
|
845 |
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
|
846 |
|
38624
9bb0016f7e60
changed to a more convenient argument order
Christian Urban <urbanc@in.tum.de>
parents:
38558
diff
changeset
|
847 |
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
|
848 |
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
|
849 |
|
45279 | 850 |
end; |