author | blanchet |
Fri, 16 Aug 2013 18:06:37 +0200 | |
changeset 53035 | b139670d88d9 |
parent 53034 | 6067703399ad |
child 53036 | 7dd103c29f9d |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49504
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_util.ML |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
49282 | 5 |
Library for bounded natural functors. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
signature BNF_UTIL = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
sig |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
'i list -> 'j list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
'i list -> 'j list -> 'k list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
'i list -> 'j list -> 'k list -> 'l list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
'i list -> 'j list -> 'k list -> 'l list -> 'm list |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
35 |
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
37 |
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
39 |
val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h |
51758 | 43 |
val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) -> |
44 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i -> |
|
45 |
'j list * 'i |
|
51767
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
46 |
val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) -> |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
47 |
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
48 |
'i list -> 'j -> 'k list * 'j |
51903 | 49 |
val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list |
49668 | 50 |
val splice: 'a list -> 'a list -> 'a list |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
val transpose: 'a list list -> 'a list list |
52279 | 52 |
val sort_like: ('a * 'b -> bool) -> 'b list -> 'c list -> 'a list -> 'c list |
49212 | 53 |
val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list |
51757 | 54 |
val pad_list: 'a -> int -> 'a list -> 'a list |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
val mk_fresh_names: Proof.context -> int -> string -> string list * Proof.context |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
val mk_TFrees: int -> Proof.context -> typ list * Proof.context |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
58 |
val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context |
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49282
diff
changeset
|
59 |
val mk_TFrees': sort list -> Proof.context -> typ list * Proof.context |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
60 |
val mk_Frees: string -> typ list -> Proof.context -> term list * Proof.context |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
61 |
val mk_Freess: string -> typ list list -> Proof.context -> term list list * Proof.context |
49177
db8ce685073f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
blanchet
parents:
49176
diff
changeset
|
62 |
val mk_Freesss: string -> typ list list list -> Proof.context -> |
db8ce685073f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
blanchet
parents:
49176
diff
changeset
|
63 |
term list list list * Proof.context |
49200 | 64 |
val mk_Freessss: string -> typ list list list list -> Proof.context -> |
65 |
term list list list list * Proof.context |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
66 |
val mk_Frees': string -> typ list -> Proof.context -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
67 |
(term list * (string * typ) list) * Proof.context |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
val mk_Freess': string -> typ list list -> Proof.context -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
(term list list * (string * typ) list list) * Proof.context |
53034
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
70 |
val nonzero_string_of_int: int -> string |
53035 | 71 |
val resort_tfree: sort -> typ -> typ |
51762 | 72 |
val retype_free: typ -> term -> term |
53034
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
73 |
val typ_subst_nonatomic: (typ * typ) list -> typ -> typ |
52937 | 74 |
val variant_types: string list -> sort list -> Proof.context -> |
75 |
(string * sort) list * Proof.context |
|
76 |
val variant_tfrees: string list -> Proof.context -> typ list * Proof.context |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
|
52280 | 78 |
val num_binder_types: typ -> int |
49395
323414474c1f
use strip_typeN in bnf_def (instead of repairing strip_type)
traytel
parents:
49366
diff
changeset
|
79 |
val strip_typeN: int -> typ -> typ list * typ |
323414474c1f
use strip_typeN in bnf_def (instead of repairing strip_type)
traytel
parents:
49366
diff
changeset
|
80 |
|
49463 | 81 |
val mk_predT: typ list -> typ |
82 |
val mk_pred1T: typ -> typ |
|
83 |
val mk_pred2T: typ -> typ -> typ |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
val mk_relT: typ * typ -> typ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
val dest_relT: typ -> typ * typ |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
86 |
val dest_pred2T: typ -> typ * typ |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
val mk_sumT: typ * typ -> typ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
val ctwo: term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
val fst_const: typ -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
val snd_const: typ -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
val Id_const: typ -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
val mk_Ball: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
val mk_Bex: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
val mk_Card_order: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
val mk_Field: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
val mk_Gr: term -> term -> term |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
99 |
val mk_Grp: term -> term -> term |
49210 | 100 |
val mk_IfN: typ -> term list -> term list -> term |
49123
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49119
diff
changeset
|
101 |
val mk_Trueprop_eq: term * term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
val mk_UNION: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
val mk_Union: typ -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
val mk_card_binop: string -> (typ * typ -> typ) -> term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
val mk_card_of: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
val mk_card_order: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
val mk_cexp: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
val mk_cinfinite: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
val mk_collect: term list -> typ -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
val mk_converse: term -> term |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
111 |
val mk_conversep: term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
val mk_cprod: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
val mk_csum: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
val mk_dir_image: term -> term -> term |
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
115 |
val mk_fun_rel: term -> term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
val mk_image: term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
val mk_in: term list -> term list -> typ -> term |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
118 |
val mk_leq: term -> term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
119 |
val mk_ordLeq: term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
val mk_rel_comp: term * term -> term |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
121 |
val mk_rel_compp: term * term -> term |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
|
49536 | 124 |
val rapp: term -> term -> term |
125 |
||
49075 | 126 |
val list_all_free: term list -> term -> term |
127 |
val list_exists_free: term list -> term -> term |
|
128 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
(*parameterized terms*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
val mk_nthN: int -> term -> int -> term |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
(*parameterized thms*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
val mk_Un_upper: int -> int -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
val mk_conjIN: int -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
val mk_conjunctN: int -> int -> thm |
49337 | 136 |
val conj_dests: int -> thm -> thm list |
49075 | 137 |
val mk_disjIN: int -> int -> thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
val mk_nthI: int -> int -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
val mk_nth_conv: int -> int -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
val mk_ordLeq_csum: int -> int -> thm -> thm |
49366 | 141 |
val mk_UnIN: int -> int -> thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
|
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
143 |
val Pair_eqD: thm |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
144 |
val Pair_eqI: thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
val ctrans: thm |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
146 |
val id_apply: thm |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
147 |
val meta_mp: thm |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
148 |
val meta_spec: thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
val o_apply: thm |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49484
diff
changeset
|
150 |
val set_mp: thm |
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49484
diff
changeset
|
151 |
val set_rev_mp: thm |
49490 | 152 |
val subset_UNIV: thm |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
val mk_sym: thm -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
val mk_trans: thm -> thm -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
val mk_unabs_def: int -> thm -> thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
|
49605
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
157 |
val is_triv_implies: thm -> bool |
49484 | 158 |
val is_refl: thm -> bool |
49605
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
159 |
val is_concl_refl: thm -> bool |
49484 | 160 |
val no_refl: thm list -> thm list |
161 |
val no_reflexive: thm list -> thm list |
|
162 |
||
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
163 |
val cterm_instantiate_pos: cterm option list -> thm -> thm |
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
164 |
val fold_thms: Proof.context -> thm list -> thm -> thm |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
165 |
val unfold_thms: Proof.context -> thm list -> thm -> thm |
49463 | 166 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
val mk_permute: ''a list -> ''a list -> 'b list -> 'b list |
52985 | 168 |
val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
|
49075 | 170 |
val certifyT: Proof.context -> typ -> ctyp |
171 |
val certify: Proof.context -> term -> cterm |
|
172 |
||
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
173 |
val standard_binding: binding |
51790
22517d04d20b
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset
|
174 |
val equal_binding: binding |
52079 | 175 |
val parse_binding: binding parser |
176 |
val parse_binding_colon: binding parser |
|
177 |
val parse_opt_binding_colon: binding parser |
|
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49425
diff
changeset
|
178 |
|
49835 | 179 |
val typedef: binding * (string * sort) list * mixfix -> term -> |
49228 | 180 |
(binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory |
181 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
val CONJ_WRAP_GEN: tactic -> ('a -> tactic) -> 'a list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
val CONJ_WRAP_GEN': (int -> tactic) -> ('a -> int -> tactic) -> 'a list -> int -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
val CONJ_WRAP: ('a -> tactic) -> 'a list -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
val CONJ_WRAP': ('a -> int -> tactic) -> 'a list -> int -> tactic |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
structure BNF_Util : BNF_UTIL = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
struct |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
(* Library proper *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
196 |
fun map3 _ [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
197 |
| map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
198 |
| map3 _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
199 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
200 |
fun map4 _ [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
201 |
| map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
202 |
| map4 _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
203 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
204 |
fun map5 _ [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
205 |
| map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
206 |
f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
207 |
| map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
208 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
209 |
fun map6 _ [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
210 |
| map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
211 |
f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
212 |
| map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
213 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
214 |
fun map7 _ [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
215 |
| map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
216 |
f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
217 |
| map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
218 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
219 |
fun map8 _ [] [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
220 |
| map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
221 |
f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
222 |
| map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
223 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
224 |
fun map9 _ [] [] [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
225 |
| map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
226 |
(x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
227 |
f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
228 |
| map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
229 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
230 |
fun map10 _ [] [] [] [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
231 |
| map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
232 |
(x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
233 |
f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
234 |
| map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
235 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
236 |
fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
237 |
| map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
238 |
(x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
239 |
f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
240 |
| map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
241 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
242 |
fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
243 |
| map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
244 |
(x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
245 |
f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 :: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
246 |
map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
247 |
| map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
248 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
249 |
fun fold_map2 _ [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
250 |
| fold_map2 f (x1::x1s) (x2::x2s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
251 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
252 |
val (x, acc') = f x1 x2 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
253 |
val (xs, acc'') = fold_map2 f x1s x2s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
254 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
255 |
| fold_map2 _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
256 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
257 |
fun fold_map3 _ [] [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
258 |
| fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
259 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
260 |
val (x, acc') = f x1 x2 x3 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
261 |
val (xs, acc'') = fold_map3 f x1s x2s x3s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
262 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
263 |
| fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
264 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
265 |
fun fold_map4 _ [] [] [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
266 |
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
267 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
268 |
val (x, acc') = f x1 x2 x3 x4 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
269 |
val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
270 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
271 |
| fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
fun fold_map5 _ [] [] [] [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
274 |
| fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
275 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
276 |
val (x, acc') = f x1 x2 x3 x4 x5 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
277 |
val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
278 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
279 |
| fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
280 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
281 |
fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
282 |
| fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
283 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
284 |
val (x, acc') = f x1 x2 x3 x4 x5 x6 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
286 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
| fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
289 |
fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
| fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
292 |
val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc'; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
294 |
in (x :: xs, acc'') end |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
295 |
| fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
296 |
|
51758 | 297 |
fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc) |
298 |
| fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) |
|
299 |
acc = |
|
300 |
let |
|
301 |
val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc; |
|
302 |
val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc'; |
|
303 |
in (x :: xs, acc'') end |
|
304 |
| fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
|
305 |
||
51767
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
306 |
fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc) |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
307 |
| fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
308 |
(x9::x9s) acc = |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
309 |
let |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
310 |
val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc; |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
311 |
val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc'; |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
312 |
in (x :: xs, acc'') end |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
313 |
| fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; |
bbcdd8519253
honor user-specified name for relator + generalize syntax
blanchet
parents:
51762
diff
changeset
|
314 |
|
51903 | 315 |
fun split_list4 [] = ([], [], [], []) |
316 |
| split_list4 ((x1, x2, x3, x4) :: xs) = |
|
317 |
let val (xs1, xs2, xs3, xs4) = split_list4 xs; |
|
318 |
in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end; |
|
319 |
||
49075 | 320 |
(*stolen from ~~/src/HOL/Tools/SMT/smt_utils.ML*) |
321 |
fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt); |
|
322 |
fun certifyT ctxt = Thm.ctyp_of (Proof_Context.theory_of ctxt); |
|
323 |
||
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
324 |
(* The standard binding stands for a name generated following the canonical convention (e.g. |
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
325 |
"is_Nil" from "Nil"). The smart binding is either the standard binding or no binding at all, |
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
326 |
depending on the context. *) |
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
327 |
val standard_binding = @{binding _}; |
51790
22517d04d20b
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset
|
328 |
val equal_binding = @{binding "="}; |
51787
1267c28c7bdd
changed discriminator default: avoid mixing ctor and dtor views
blanchet
parents:
51767
diff
changeset
|
329 |
|
51790
22517d04d20b
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset
|
330 |
val parse_binding = Parse.binding || @{keyword "="} >> K equal_binding; |
22517d04d20b
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset
|
331 |
val parse_binding_colon = parse_binding --| @{keyword ":"}; |
22517d04d20b
more intuitive syntax for equality-style discriminators of nullary constructors
blanchet
parents:
51787
diff
changeset
|
332 |
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty; |
49434
433dc7e028c8
separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)
traytel
parents:
49425
diff
changeset
|
333 |
|
49228 | 334 |
(*TODO: is this really different from Typedef.add_typedef_global?*) |
49835 | 335 |
fun typedef typ set opt_morphs tac lthy = |
49228 | 336 |
let |
337 |
val ((name, info), (lthy, lthy_old)) = |
|
338 |
lthy |
|
49835 | 339 |
|> Typedef.add_typedef typ set opt_morphs tac |
49228 | 340 |
||> `Local_Theory.restore; |
341 |
val phi = Proof_Context.export_morphism lthy_old lthy; |
|
342 |
in |
|
343 |
((name, Typedef.transform_info phi info), lthy) |
|
344 |
end; |
|
345 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
346 |
(*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
347 |
fun WRAP gen_before gen_after xs core_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
348 |
fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
349 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
350 |
fun WRAP' gen_before gen_after xs core_tac = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
351 |
fold_rev (fn x => fn tac => gen_before x THEN' tac THEN' gen_after x) xs core_tac; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
352 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
353 |
fun CONJ_WRAP_GEN conj_tac gen_tac xs = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
354 |
let val (butlast, last) = split_last xs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
355 |
in WRAP (fn thm => conj_tac THEN gen_tac thm) (K all_tac) butlast (gen_tac last) end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
356 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
357 |
fun CONJ_WRAP_GEN' conj_tac gen_tac xs = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
358 |
let val (butlast, last) = split_last xs; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
359 |
in WRAP' (fn thm => conj_tac THEN' gen_tac thm) (K (K all_tac)) butlast (gen_tac last) end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
360 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
361 |
(*not eta-converted because of monotype restriction*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
362 |
fun CONJ_WRAP gen_tac = CONJ_WRAP_GEN (rtac conjI 1) gen_tac; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
363 |
fun CONJ_WRAP' gen_tac = CONJ_WRAP_GEN' (rtac conjI) gen_tac; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
364 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
365 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
366 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
367 |
(* Term construction *) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
368 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
369 |
(** Fresh variables **) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
370 |
|
49425 | 371 |
fun nonzero_string_of_int 0 = "" |
372 |
| nonzero_string_of_int n = string_of_int n; |
|
373 |
||
49298
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49282
diff
changeset
|
374 |
val mk_TFrees' = apfst (map TFree) oo Variable.invent_types; |
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49282
diff
changeset
|
375 |
|
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49282
diff
changeset
|
376 |
fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS); |
36e551d3af3b
support for sort constraints in new (co)data commands
blanchet
parents:
49282
diff
changeset
|
377 |
val mk_TFreess = fold_map mk_TFrees; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
378 |
|
53035 | 379 |
fun resort_tfree S (TFree (s, _)) = TFree (s, S); |
380 |
||
53034
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
381 |
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*) |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
382 |
fun typ_subst_nonatomic [] = I |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
383 |
| typ_subst_nonatomic inst = |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
384 |
let |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
385 |
fun subst (Type (s, Ts)) = perhaps (AList.lookup (op =) inst) (Type (s, map subst Ts)) |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
386 |
| subst T = perhaps (AList.lookup (op =) inst) T; |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
387 |
in subst end; |
6067703399ad
moved library function where it belongs, and used Dmitriy's inside-out implementation
blanchet
parents:
52985
diff
changeset
|
388 |
|
49178 | 389 |
fun mk_names n x = if n = 1 then [x] else map (fn i => x ^ string_of_int i) (1 upto n); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
390 |
|
49178 | 391 |
fun mk_fresh_names ctxt = (fn xs => Variable.variant_fixes xs ctxt) oo mk_names; |
392 |
fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts); |
|
49177
db8ce685073f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
blanchet
parents:
49176
diff
changeset
|
393 |
fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss; |
db8ce685073f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
blanchet
parents:
49176
diff
changeset
|
394 |
fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss; |
49200 | 395 |
fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss; |
49178 | 396 |
fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts)); |
49177
db8ce685073f
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
blanchet
parents:
49176
diff
changeset
|
397 |
fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
398 |
|
51894 | 399 |
fun retype_free T (Free (s, _)) = Free (s, T) |
400 |
| retype_free _ t = raise TERM ("retype_free", [t]); |
|
51762 | 401 |
|
52937 | 402 |
fun ensure_prefix pre s = s |> not (String.isPrefix pre s) ? prefix pre; |
403 |
||
404 |
fun variant_types ss Ss ctxt = |
|
405 |
let |
|
406 |
val (tfrees, _) = |
|
407 |
fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt); |
|
408 |
val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt; |
|
409 |
in (tfrees, ctxt') end; |
|
410 |
||
411 |
fun variant_tfrees ss = |
|
412 |
apfst (map TFree) o |
|
413 |
variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS); |
|
414 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
415 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
416 |
(** Types **) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
417 |
|
52280 | 418 |
(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*) |
419 |
fun num_binder_types (Type (@{type_name fun}, [_, T2])) = |
|
420 |
1 + num_binder_types T2 |
|
421 |
| num_binder_types _ = 0 |
|
422 |
||
49395
323414474c1f
use strip_typeN in bnf_def (instead of repairing strip_type)
traytel
parents:
49366
diff
changeset
|
423 |
fun strip_typeN 0 T = ([], T) |
323414474c1f
use strip_typeN in bnf_def (instead of repairing strip_type)
traytel
parents:
49366
diff
changeset
|
424 |
| strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T |
49463 | 425 |
| strip_typeN _ T = raise TYPE ("strip_typeN", [T], []); |
49395
323414474c1f
use strip_typeN in bnf_def (instead of repairing strip_type)
traytel
parents:
49366
diff
changeset
|
426 |
|
49463 | 427 |
fun mk_predT Ts = Ts ---> HOLogic.boolT; |
428 |
fun mk_pred1T T = mk_predT [T]; |
|
429 |
fun mk_pred2T T U = mk_predT [T, U]; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
430 |
val mk_relT = HOLogic.mk_setT o HOLogic.mk_prodT; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
431 |
val dest_relT = HOLogic.dest_prodT o HOLogic.dest_setT; |
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
432 |
val dest_pred2T = apsnd Term.domain_type o Term.dest_funT; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
433 |
fun mk_sumT (LT, RT) = Type (@{type_name Sum_Type.sum}, [LT, RT]); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
434 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
435 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
436 |
(** Constants **) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
437 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
438 |
fun fst_const T = Const (@{const_name fst}, T --> fst (HOLogic.dest_prodT T)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
439 |
fun snd_const T = Const (@{const_name snd}, T --> snd (HOLogic.dest_prodT T)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
440 |
fun Id_const T = Const (@{const_name Id}, mk_relT (T, T)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
441 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
442 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
443 |
(** Operators **) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
444 |
|
49123
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49119
diff
changeset
|
445 |
val mk_Trueprop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
263b0e330d8b
more work on sugar + simplify Trueprop + eq idiom everywhere
blanchet
parents:
49119
diff
changeset
|
446 |
|
49210 | 447 |
fun mk_IfN _ _ [t] = t |
448 |
| mk_IfN T (c :: cs) (t :: ts) = |
|
449 |
Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ c $ t $ mk_IfN T cs ts; |
|
450 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
451 |
fun mk_converse R = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
452 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
453 |
val RT = dest_relT (fastype_of R); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
454 |
val RST = mk_relT (snd RT, fst RT); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
455 |
in Const (@{const_name converse}, fastype_of R --> RST) $ R end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
456 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
457 |
fun mk_rel_comp (R, S) = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
458 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
459 |
val RT = fastype_of R; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
460 |
val ST = fastype_of S; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
461 |
val RST = mk_relT (fst (dest_relT RT), snd (dest_relT ST)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
462 |
in Const (@{const_name relcomp}, RT --> ST --> RST) $ R $ S end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
463 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
464 |
fun mk_Gr A f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
465 |
let val ((AT, BT), FT) = `dest_funT (fastype_of f); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
466 |
in Const (@{const_name Gr}, HOLogic.mk_setT AT --> FT --> mk_relT (AT, BT)) $ A $ f end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
467 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
468 |
fun mk_conversep R = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
469 |
let |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
470 |
val RT = dest_pred2T (fastype_of R); |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
471 |
val RST = mk_pred2T (snd RT) (fst RT); |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
472 |
in Const (@{const_name conversep}, fastype_of R --> RST) $ R end; |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
473 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
474 |
fun mk_rel_compp (R, S) = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
475 |
let |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
476 |
val RT = fastype_of R; |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
477 |
val ST = fastype_of S; |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
478 |
val RST = mk_pred2T (fst (dest_pred2T RT)) (snd (dest_pred2T ST)); |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
479 |
in Const (@{const_name relcompp}, RT --> ST --> RST) $ R $ S end; |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
480 |
|
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
481 |
fun mk_Grp A f = |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
482 |
let val ((AT, BT), FT) = `dest_funT (fastype_of f); |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
483 |
in Const (@{const_name Grp}, HOLogic.mk_setT AT --> FT --> mk_pred2T AT BT) $ A $ f end; |
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
484 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
485 |
fun mk_image f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
486 |
let val (T, U) = dest_funT (fastype_of f); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
487 |
in Const (@{const_name image}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
488 |
(T --> U) --> (HOLogic.mk_setT T) --> (HOLogic.mk_setT U)) $ f end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
489 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
490 |
fun mk_Ball X f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
491 |
Const (@{const_name Ball}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
492 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
493 |
fun mk_Bex X f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
494 |
Const (@{const_name Bex}, fastype_of X --> fastype_of f --> HOLogic.boolT) $ X $ f; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
495 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
496 |
fun mk_UNION X f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
497 |
let val (T, U) = dest_funT (fastype_of f); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
498 |
in Const (@{const_name SUPR}, fastype_of X --> (T --> U) --> U) $ X $ f end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
499 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
500 |
fun mk_Union T = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
501 |
Const (@{const_name Sup}, HOLogic.mk_setT (HOLogic.mk_setT T) --> HOLogic.mk_setT T); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
502 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
503 |
fun mk_Field r = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
504 |
let val T = fst (dest_relT (fastype_of r)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
505 |
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
506 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
507 |
fun mk_card_order bd = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
508 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
509 |
val T = fastype_of bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
510 |
val AT = fst (dest_relT T); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
511 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
512 |
Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
513 |
(HOLogic.mk_UNIV AT) $ bd |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
514 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
515 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
516 |
fun mk_Card_order bd = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
517 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
518 |
val T = fastype_of bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
519 |
val AT = fst (dest_relT T); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
520 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
521 |
Const (@{const_name card_order_on}, HOLogic.mk_setT AT --> T --> HOLogic.boolT) $ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
522 |
mk_Field bd $ bd |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
523 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
524 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
525 |
fun mk_cinfinite bd = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
526 |
Const (@{const_name cinfinite}, fastype_of bd --> HOLogic.boolT) $ bd; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
527 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
528 |
fun mk_ordLeq t1 t2 = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
529 |
HOLogic.mk_mem (HOLogic.mk_prod (t1, t2), |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
530 |
Const (@{const_name ordLeq}, mk_relT (fastype_of t1, fastype_of t2))); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
531 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
532 |
fun mk_card_of A = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
533 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
534 |
val AT = fastype_of A; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
535 |
val T = HOLogic.dest_setT AT; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
536 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
537 |
Const (@{const_name card_of}, AT --> mk_relT (T, T)) $ A |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
538 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
539 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
540 |
fun mk_dir_image r f = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
541 |
let val (T, U) = dest_funT (fastype_of f); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
542 |
in Const (@{const_name dir_image}, mk_relT (T, T) --> (T --> U) --> mk_relT (U, U)) $ r $ f end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
543 |
|
52719
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
544 |
fun mk_fun_rel R S = |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
545 |
let |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
546 |
val ((RA, RB), RT) = `dest_pred2T (fastype_of R); |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
547 |
val ((SA, SB), ST) = `dest_pred2T (fastype_of S); |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
548 |
in Const (@{const_name fun_rel}, RT --> ST --> mk_pred2T (RA --> SA) (RB --> SB)) $ R $ S end; |
480a3479fa47
transfer rule for map (not yet registered as a transfer rule)
traytel
parents:
52545
diff
changeset
|
549 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
550 |
(*FIXME: "x"?*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
551 |
(*(nth sets i) must be of type "T --> 'ai set"*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
552 |
fun mk_in As sets T = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
553 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
554 |
fun in_single set A = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
555 |
let val AT = fastype_of A; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
556 |
in Const (@{const_name less_eq}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
557 |
AT --> AT --> HOLogic.boolT) $ (set $ Free ("x", T)) $ A end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
558 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
559 |
if length sets > 0 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
560 |
then HOLogic.mk_Collect ("x", T, foldr1 (HOLogic.mk_conj) (map2 in_single sets As)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
561 |
else HOLogic.mk_UNIV T |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
562 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
563 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
564 |
fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
565 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
566 |
val AT = fastype_of A; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
567 |
val BT1 = fastype_of B1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
568 |
val BT2 = fastype_of B2; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
569 |
val FT1 = fastype_of f1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
570 |
val FT2 = fastype_of f2; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
571 |
val PT1 = fastype_of p1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
572 |
val PT2 = fastype_of p2; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
573 |
val T1 = HOLogic.dest_setT BT1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
574 |
val T2 = HOLogic.dest_setT BT2; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
575 |
val domP = domain_type PT1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
576 |
val ranF = range_type FT1; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
577 |
val _ = if is_some pseudo orelse |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
578 |
(HOLogic.dest_setT AT = domP andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
579 |
domain_type FT1 = T1 andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
580 |
domain_type FT2 = T2 andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
581 |
domain_type PT2 = domP andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
582 |
range_type PT1 = T1 andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
583 |
range_type PT2 = T2 andalso |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
584 |
range_type FT2 = ranF) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
585 |
then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
586 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
587 |
(case pseudo of |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
588 |
NONE => Const (@{const_name wpull}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
589 |
AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
590 |
A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
591 |
| SOME (e1, e2) => Const (@{const_name wppull}, |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
592 |
AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 --> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
593 |
PT1 --> PT2 --> HOLogic.boolT) $ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
594 |
A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
595 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
596 |
|
51893
596baae88a88
got rid of the set based relator---use (binary) predicate based relator instead
traytel
parents:
51861
diff
changeset
|
597 |
fun mk_leq t1 t2 = |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
598 |
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
599 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
600 |
fun mk_card_binop binop typop t1 t2 = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
601 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
602 |
val (T1, relT1) = `(fst o dest_relT) (fastype_of t1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
603 |
val (T2, relT2) = `(fst o dest_relT) (fastype_of t2); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
604 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
605 |
Const (binop, relT1 --> relT2 --> mk_relT (typop (T1, T2), typop (T1, T2))) $ t1 $ t2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
606 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
607 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
608 |
val mk_csum = mk_card_binop @{const_name csum} mk_sumT; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
609 |
val mk_cprod = mk_card_binop @{const_name cprod} HOLogic.mk_prodT; |
52545
d2ad6eae514f
Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
traytel
parents:
52280
diff
changeset
|
610 |
val mk_cexp = mk_card_binop @{const_name cexp} (op --> o swap); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
611 |
val ctwo = @{term ctwo}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
612 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
613 |
fun mk_collect xs defT = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
614 |
let val T = (case xs of [] => defT | (x::_) => fastype_of x); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
615 |
in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
616 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
617 |
fun mk_permute src dest xs = map (nth xs o (fn x => find_index ((curry op =) x) src)) dest; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
618 |
|
49536 | 619 |
fun rapp u t = betapply (t, u); |
620 |
||
49075 | 621 |
val list_all_free = |
622 |
fold_rev (fn free => fn P => |
|
623 |
let val (x, T) = Term.dest_Free free; |
|
624 |
in HOLogic.all_const T $ Term.absfree (x, T) P end); |
|
625 |
||
626 |
val list_exists_free = |
|
627 |
fold_rev (fn free => fn P => |
|
628 |
let val (x, T) = Term.dest_Free free; |
|
629 |
in HOLogic.exists_const T $ Term.absfree (x, T) P end); |
|
630 |
||
52985 | 631 |
fun find_indices eq xs ys = map_filter I |
632 |
(map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
633 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
634 |
fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; |
52913
2d2d9d1de1a9
theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
traytel
parents:
52719
diff
changeset
|
635 |
fun mk_sym thm = thm RS sym; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
636 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
637 |
(*TODO: antiquote heavily used theorems once*) |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
638 |
val Pair_eqD = @{thm iffD1[OF Pair_eq]}; |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
639 |
val Pair_eqI = @{thm iffD2[OF Pair_eq]}; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
640 |
val ctrans = @{thm ordLeq_transitive}; |
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
641 |
val id_apply = @{thm id_apply}; |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
642 |
val meta_mp = @{thm meta_mp}; |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
643 |
val meta_spec = @{thm meta_spec}; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
644 |
val o_apply = @{thm o_apply}; |
49488
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49484
diff
changeset
|
645 |
val set_mp = @{thm set_mp}; |
02eb07152998
use iffD* instead of (s)subst instantiated with identity; tuned antiquotations;
traytel
parents:
49484
diff
changeset
|
646 |
val set_rev_mp = @{thm set_rev_mp}; |
49490 | 647 |
val subset_UNIV = @{thm subset_UNIV}; |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
648 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
649 |
fun mk_nthN 1 t 1 = t |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
650 |
| mk_nthN _ t 1 = HOLogic.mk_fst t |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
651 |
| mk_nthN 2 t 2 = HOLogic.mk_snd t |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
652 |
| mk_nthN n t m = mk_nthN (n - 1) (HOLogic.mk_snd t) (m - 1); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
653 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
654 |
fun mk_nth_conv n m = |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
655 |
let |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
656 |
fun thm b = if b then @{thm fst_snd} else @{thm snd_snd} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
657 |
fun mk_nth_conv _ 1 1 = refl |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
658 |
| mk_nth_conv _ _ 1 = @{thm fst_conv} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
659 |
| mk_nth_conv _ 2 2 = @{thm snd_conv} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
660 |
| mk_nth_conv b _ 2 = @{thm snd_conv} RS thm b |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
661 |
| mk_nth_conv b n m = mk_nth_conv false (n - 1) (m - 1) RS thm b; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
662 |
in mk_nth_conv (not (m = n)) n m end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
663 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
664 |
fun mk_nthI 1 1 = @{thm TrueE[OF TrueI]} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
665 |
| mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI}) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
666 |
(if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI}); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
667 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
668 |
fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
669 |
| mk_conjunctN _ 1 = conjunct1 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
670 |
| mk_conjunctN 2 2 = conjunct2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
671 |
| mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1)); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
672 |
|
49337 | 673 |
fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n); |
674 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
675 |
fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
676 |
| mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
677 |
|
49075 | 678 |
fun mk_disjIN 1 1 = @{thm TrueE[OF TrueI]} |
679 |
| mk_disjIN _ 1 = disjI1 |
|
680 |
| mk_disjIN 2 2 = disjI2 |
|
681 |
| mk_disjIN n m = (mk_disjIN (n - 1) (m - 1)) RS disjI2; |
|
682 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
683 |
fun mk_ordLeq_csum 1 1 thm = thm |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
684 |
| mk_ordLeq_csum _ 1 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum1}] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
685 |
| mk_ordLeq_csum 2 2 thm = @{thm ordLeq_transitive} OF [thm, @{thm ordLeq_csum2}] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
686 |
| mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
687 |
[mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}]; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
688 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
689 |
local |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
690 |
fun mk_Un_upper' 0 = subset_refl |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
691 |
| mk_Un_upper' 1 = @{thm Un_upper1} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
692 |
| mk_Un_upper' k = Library.foldr (op RS o swap) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
693 |
(replicate (k - 1) @{thm subset_trans[OF Un_upper1]}, @{thm Un_upper1}); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
694 |
in |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
695 |
fun mk_Un_upper 1 1 = subset_refl |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
696 |
| mk_Un_upper n 1 = mk_Un_upper' (n - 2) RS @{thm subset_trans[OF Un_upper1]} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
697 |
| mk_Un_upper n m = mk_Un_upper' (n - m) RS @{thm subset_trans[OF Un_upper2]}; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
698 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
699 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
700 |
local |
49366 | 701 |
fun mk_UnIN' 0 = @{thm UnI2} |
702 |
| mk_UnIN' m = mk_UnIN' (m - 1) RS @{thm UnI1}; |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
703 |
in |
49366 | 704 |
fun mk_UnIN 1 1 = @{thm TrueE[OF TrueI]} |
705 |
| mk_UnIN n 1 = Library.foldr1 (op RS o swap) (replicate (n - 1) @{thm UnI1}) |
|
706 |
| mk_UnIN n m = mk_UnIN' (n - m) |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
707 |
end; |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
708 |
|
49668 | 709 |
fun splice xs ys = flat (map2 (fn x => fn y => [x, y]) xs ys); |
49075 | 710 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
711 |
fun transpose [] = [] |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
712 |
| transpose ([] :: xss) = transpose xss |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
713 |
| transpose xss = map hd xss :: transpose (map tl xss); |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
714 |
|
52985 | 715 |
(*FIXME: merge with mk_permute*) |
52279 | 716 |
fun sort_like eq xs ys = map (fn x => nth ys (find_index (curry eq x) xs)); |
51861 | 717 |
|
49212 | 718 |
fun seq_conds f n k xs = |
719 |
if k = n then |
|
720 |
map (f false) (take (k - 1) xs) |
|
721 |
else |
|
722 |
let val (negs, pos) = split_last (take k xs) in |
|
723 |
map (f false) negs @ [f true pos] |
|
724 |
end; |
|
725 |
||
51757 | 726 |
fun pad_list x n xs = xs @ replicate (n - length xs) x; |
727 |
||
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
728 |
fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong); |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
729 |
|
49605
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
730 |
fun is_triv_implies thm = |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
731 |
op aconv (Logic.dest_implies (Thm.prop_of thm)) |
49484 | 732 |
handle TERM _ => false; |
733 |
||
49605
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
734 |
fun is_refl_prop t = |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
735 |
op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop t)) |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
736 |
handle TERM _ => false; |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
737 |
|
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
738 |
val is_refl = is_refl_prop o Thm.prop_of; |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
739 |
val is_concl_refl = is_refl_prop o Logic.strip_imp_concl o Thm.prop_of; |
ea566f5e1724
avoid another brand of trivial "disc_rel" theorems (which made the simplifier loop for all single-constructor types)
blanchet
parents:
49585
diff
changeset
|
740 |
|
49484 | 741 |
val no_refl = filter_out is_refl; |
742 |
val no_reflexive = filter_out Thm.is_reflexive; |
|
743 |
||
49585
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
744 |
fun cterm_instantiate_pos cts thm = |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
745 |
let |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
746 |
val cert = Thm.cterm_of (Thm.theory_of_thm thm); |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
747 |
val vars = Term.add_vars (prop_of thm) []; |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
748 |
val vars' = rev (drop (length vars - length cts) vars); |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
749 |
val ps = map_filter (fn (_, NONE) => NONE |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
750 |
| (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts); |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
751 |
in |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
752 |
Drule.cterm_instantiate ps thm |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
753 |
end; |
5c4a12550491
generate high-level "maps", "sets", and "rels" properties
blanchet
parents:
49536
diff
changeset
|
754 |
|
49504
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
755 |
fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms); |
df9b897fb254
renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
blanchet
parents:
49490
diff
changeset
|
756 |
fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms); |
49463 | 757 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
758 |
end; |