author | blanchet |
Wed, 28 Dec 2016 17:22:16 +0100 | |
changeset 64674 | ef0a5fd30f3b |
parent 62687 | 1c4842b32bfb |
child 64705 | 7596b0736ab9 |
permissions | -rw-r--r-- |
55061 | 1 |
(* Title: HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
2 |
Author: Lorenz Panny, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
4 |
Copyright 2013 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
5 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
6 |
Library for recursor and corecursor sugar. |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
7 |
*) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
8 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
9 |
signature BNF_FP_REC_SUGAR_UTIL = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
10 |
sig |
59595 | 11 |
val error_at: Proof.context -> term list -> string -> 'a |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
12 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
13 |
datatype fp_kind = Least_FP | Greatest_FP |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
14 |
|
55966 | 15 |
val case_fp: fp_kind -> 'a -> 'a -> 'a |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
16 |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
17 |
type fp_rec_sugar = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
18 |
{transfers: bool list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
19 |
fun_names: string list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
20 |
funs: term list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
21 |
fun_defs: thm list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
22 |
fpTs: typ list} |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
23 |
|
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
24 |
val morph_fp_rec_sugar: morphism -> fp_rec_sugar -> fp_rec_sugar |
59281 | 25 |
val transfer_fp_rec_sugar: theory -> fp_rec_sugar -> fp_rec_sugar |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
26 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
27 |
val flat_rec_arg_args: 'a list list -> 'a list |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
28 |
|
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
29 |
val indexed: 'a list -> int -> int list * int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
30 |
val indexedd: 'a list list -> int -> int list list * int |
54299 | 31 |
val indexeddd: 'a list list list -> int -> int list list list * int |
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
32 |
val indexedddd: 'a list list list list -> int -> int list list list list * int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
33 |
val find_index_eq: ''a list -> ''a -> int |
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
34 |
val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
35 |
val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
|
62687 | 37 |
val order_strong_conn: ('a * 'a -> bool) -> ((('a * unit) * 'a list) list -> 'b) -> |
38 |
('b -> 'a list) -> ('a * 'a list) list -> 'a list list -> 'a list list |
|
39 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
40 |
val mk_common_name: string list -> string |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
41 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
42 |
val num_binder_types: typ -> int |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
43 |
val exists_subtype_in: typ list -> typ -> bool |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
44 |
val exists_strict_subtype_in: typ list -> typ -> bool |
55571 | 45 |
val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list |
46 |
||
56651 | 47 |
val retype_const_or_free: typ -> term -> term |
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54614
diff
changeset
|
48 |
val drop_all: term -> term |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
49 |
val permute_args: int -> term -> term |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
50 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
51 |
val mk_partial_compN: int -> typ -> term -> term |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
52 |
val mk_compN: int -> typ list -> term * term -> term |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
53 |
val mk_comp: typ list -> term * term -> term |
54202
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
54 |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
56651
diff
changeset
|
55 |
val mk_co_rec: theory -> fp_kind -> typ list -> typ -> term -> term |
55571 | 56 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
57 |
val mk_conjunctN: int -> int -> thm |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
58 |
val conj_dests: int -> thm -> thm list |
64674
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
59 |
|
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
60 |
val print_def_consts: bool -> (term * (string * thm)) list -> Proof.context -> unit |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
61 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
62 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
63 |
structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
64 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
65 |
|
59595 | 66 |
fun error_at ctxt ts str = |
67 |
error (str ^ (if null ts then "" |
|
68 |
else " at\n " ^ space_implode "\n " (map (quote o Syntax.string_of_term ctxt) ts))); |
|
69 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
70 |
datatype fp_kind = Least_FP | Greatest_FP; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
71 |
|
55966 | 72 |
fun case_fp Least_FP l _ = l |
73 |
| case_fp Greatest_FP _ g = g; |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
74 |
|
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
75 |
type fp_rec_sugar = |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
76 |
{transfers: bool list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
77 |
fun_names: string list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
78 |
funs: term list, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
79 |
fun_defs: thm list, |
59281 | 80 |
fpTs: typ list}; |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
81 |
|
59314 | 82 |
fun morph_fp_rec_sugar phi ({transfers, fun_names, funs, fun_defs, fpTs} : fp_rec_sugar) = |
59275
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
83 |
{transfers = transfers, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
84 |
fun_names = fun_names, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
85 |
funs = map (Morphism.term phi) funs, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
86 |
fun_defs = map (Morphism.thm phi) fun_defs, |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
87 |
fpTs = map (Morphism.typ phi) fpTs}; |
77cd4992edcd
Add plugin to generate transfer theorem for primrec and primcorec
desharna
parents:
58337
diff
changeset
|
88 |
|
59281 | 89 |
val transfer_fp_rec_sugar = morph_fp_rec_sugar o Morphism.transfer_morphism; |
90 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
91 |
fun flat_rec_arg_args xss = |
59281 | 92 |
(* FIXME (once the old datatype package is completely phased out): The first line below gives the |
93 |
preferred order. The second line is for compatibility with the old datatype package. *) |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
94 |
(* flat xss *) |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
95 |
map hd xss @ maps tl xss; |
55571 | 96 |
|
54614 | 97 |
fun indexe _ h = (h, h + 1); |
98 |
fun indexed xs = fold_map indexe xs; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
99 |
fun indexedd xss = fold_map indexed xss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
100 |
fun indexeddd xsss = fold_map indexedd xsss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
101 |
fun indexedddd xssss = fold_map indexeddd xssss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
102 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
103 |
fun find_index_eq hs h = find_index (curry (op =) h) hs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
104 |
|
54246
8fdb4dc08ed1
split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents:
54243
diff
changeset
|
105 |
fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
106 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
107 |
fun find_indices eq xs ys = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
108 |
map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
109 |
|
62687 | 110 |
fun order_strong_conn eq make_graph topological_order deps sccs = |
111 |
let |
|
112 |
val normals = maps (fn x :: xs => map (fn y => (y, x)) xs) sccs; |
|
113 |
fun normal s = AList.lookup eq normals s |> the_default s; |
|
114 |
||
115 |
val normal_deps = deps |
|
116 |
|> map (fn (x, xs) => let val x' = normal x in |
|
117 |
(x', fold (insert eq o normal) xs [] |> remove eq x') |
|
118 |
end) |
|
119 |
|> AList.group eq |
|
120 |
|> map (apsnd (fn xss => fold (union eq) xss [])); |
|
121 |
||
122 |
val normal_G = make_graph (map (apfst (rpair ())) normal_deps); |
|
123 |
val ordered_normals = rev (topological_order normal_G); |
|
124 |
in |
|
125 |
map (fn x => the (find_first (fn (y :: _) => eq (y, x)) sccs)) ordered_normals |
|
126 |
end; |
|
127 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
128 |
val mk_common_name = space_implode "_"; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
129 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
130 |
fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
131 |
| num_binder_types _ = 0; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
132 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
133 |
val exists_subtype_in = Term.exists_subtype o member (op =); |
58337 | 134 |
fun exists_strict_subtype_in Ts T = exists_subtype_in (remove (op =) T Ts) T; |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
135 |
|
55571 | 136 |
fun tvar_subst thy Ts Us = |
137 |
Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; |
|
138 |
||
56651 | 139 |
fun retype_const_or_free T (Const (s, _)) = Const (s, T) |
140 |
| retype_const_or_free T (Free (s, _)) = Free (s, T) |
|
141 |
| retype_const_or_free _ t = raise TERM ("retype_const_or_free", [t]); |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
142 |
|
54979
d7593bfccf25
correctly extract code RHS, with loose bound variables
blanchet
parents:
54614
diff
changeset
|
143 |
fun drop_all t = |
56245 | 144 |
subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev, |
145 |
strip_qnt_body @{const_name Pure.all} t); |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
146 |
|
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
147 |
fun permute_args n t = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
148 |
list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
149 |
|
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
150 |
fun mk_partial_comp fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT)))); |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
151 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
152 |
fun mk_partial_compN 0 _ g = g |
55856
bddaada24074
got rid of automatically generated fold constant and theorems (to reduce overhead)
blanchet
parents:
55772
diff
changeset
|
153 |
| mk_partial_compN n fT g = mk_partial_comp fT (mk_partial_compN (n - 1) (range_type fT) g); |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
154 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
155 |
fun mk_compN n bound_Ts (g, f) = |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
156 |
let val typof = curry fastype_of1 bound_Ts in |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
157 |
mk_partial_compN n (typof f) g $ f |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
158 |
end; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
159 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
160 |
val mk_comp = mk_compN 1; |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
161 |
|
58211
c1f3fa32d322
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents:
56651
diff
changeset
|
162 |
fun mk_co_rec thy fp Cs fpT t = |
55571 | 163 |
let |
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
164 |
val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last; |
55966 | 165 |
val fpT0 = case_fp fp prebody body; |
166 |
val Cs0 = distinct (op =) (map (case_fp fp body_type domain_type) f_Cs); |
|
55571 | 167 |
val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); |
168 |
in |
|
169 |
Term.subst_TVars rho t |
|
170 |
end; |
|
171 |
||
55575
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
172 |
fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]} |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
173 |
| mk_conjunctN _ 1 = conjunct1 |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
174 |
| mk_conjunctN 2 2 = conjunct2 |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
175 |
| mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1)); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
176 |
|
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
177 |
fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n); |
a5e33e18fb5c
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents:
55573
diff
changeset
|
178 |
|
64674
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
179 |
fun print_def_consts int defs ctxt = |
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
180 |
Proof_Display.print_consts int (Position.thread_data ()) ctxt (K false) |
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
181 |
(map_filter (try (dest_Free o fst)) defs); |
ef0a5fd30f3b
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
blanchet
parents:
62687
diff
changeset
|
182 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
183 |
end; |