author | blanchet |
Mon, 04 Nov 2013 14:46:38 +0100 | |
changeset 54243 | a596292be9a8 |
parent 54241 | 357988ad95ec |
child 54246 | 8fdb4dc08ed1 |
permissions | -rw-r--r-- |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML |
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 |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
11 |
datatype rec_call = |
54200 | 12 |
No_Rec of int * typ | |
13 |
Mutual_Rec of (int * typ) (*before*) * (int * typ) (*after*) | |
|
14 |
Nested_Rec of int * typ |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
15 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
16 |
datatype corec_call = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
17 |
Dummy_No_Corec of int | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
18 |
No_Corec of int | |
54102 | 19 |
Mutual_Corec of int (*stop?*) * int (*end*) * int (*continue*) | |
20 |
Nested_Corec of int |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
21 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
22 |
type rec_ctr_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
23 |
{ctr: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
24 |
offset: int, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
25 |
calls: rec_call list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
26 |
rec_thm: thm} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
27 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
28 |
type basic_corec_ctr_spec = |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
29 |
{ctr: term, |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
30 |
disc: term, |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
31 |
sels: term list} |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
32 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
33 |
type corec_ctr_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
34 |
{ctr: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
35 |
disc: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
36 |
sels: term list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
37 |
pred: int option, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
38 |
calls: corec_call list, |
53705 | 39 |
discI: thm, |
40 |
sel_thms: thm list, |
|
53475 | 41 |
collapse: thm, |
42 |
corec_thm: thm, |
|
43 |
disc_corec: thm, |
|
44 |
sel_corecs: thm list} |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
45 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
46 |
type rec_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
47 |
{recx: term, |
53329 | 48 |
nested_map_idents: thm list, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
49 |
nested_map_comps: thm list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
50 |
ctr_specs: rec_ctr_spec list} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
51 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
52 |
type corec_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
53 |
{corec: term, |
53475 | 54 |
nested_maps: thm list, |
55 |
nested_map_idents: thm list, |
|
56 |
nested_map_comps: thm list, |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
57 |
ctr_specs: corec_ctr_spec list} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
58 |
|
54067 | 59 |
val s_not: term -> term |
60 |
val s_not_conj: term list -> term list |
|
54068 | 61 |
val s_conjs: term list -> term |
62 |
val s_disjs: term list -> term |
|
63 |
val s_dnf: term list list -> term list |
|
53878 | 64 |
|
54202
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
65 |
val mk_partial_compN: int -> typ -> typ -> term -> term |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
66 |
|
54102 | 67 |
val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
68 |
typ list -> term -> term -> term -> term |
54102 | 69 |
val massage_mutual_corec_call: Proof.context -> (term -> bool) -> (typ list -> term -> term) -> |
53890 | 70 |
typ list -> term -> term |
54102 | 71 |
val massage_nested_corec_call: Proof.context -> (term -> bool) -> |
53890 | 72 |
(typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term |
54243 | 73 |
val fold_rev_corec_call: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> term -> |
54188 | 74 |
'a -> string list * 'a |
53727
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
75 |
val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term |
53890 | 76 |
val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) -> |
77 |
typ list -> term -> term |
|
53871 | 78 |
val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) -> |
79 |
typ list -> term -> 'a -> 'a |
|
53909 | 80 |
val case_thms_of_term: Proof.context -> typ list -> term -> |
53925 | 81 |
thm list * thm list * thm list * thm list |
53878 | 82 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
83 |
val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) -> |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
84 |
((term * term list list) list) list -> local_theory -> |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
85 |
(bool * rec_spec list * typ list * thm * thm list) * local_theory |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
86 |
val basic_corec_specs_of: Proof.context -> typ -> basic_corec_ctr_spec list |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
87 |
val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) -> |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
88 |
((term * term list list) list) list -> local_theory -> |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
89 |
(bool * corec_spec list * typ list * thm * thm * thm list * thm list) * local_theory |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
90 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
91 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
92 |
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
|
93 |
struct |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
94 |
|
54006 | 95 |
open Ctr_Sugar |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
96 |
open BNF_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
97 |
open BNF_Def |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
98 |
open BNF_FP_Util |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
99 |
open BNF_FP_Def_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
100 |
open BNF_FP_N2M_Sugar |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
101 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
102 |
datatype rec_call = |
54200 | 103 |
No_Rec of int * typ | |
104 |
Mutual_Rec of (int * typ) * (int * typ) | |
|
105 |
Nested_Rec of int * typ; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
106 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
107 |
datatype corec_call = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
108 |
Dummy_No_Corec of int | |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
109 |
No_Corec of int | |
54102 | 110 |
Mutual_Corec of int * int * int | |
111 |
Nested_Corec of int; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
112 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
113 |
type rec_ctr_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
114 |
{ctr: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
115 |
offset: int, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
116 |
calls: rec_call list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
117 |
rec_thm: thm}; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
118 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
119 |
type basic_corec_ctr_spec = |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
120 |
{ctr: term, |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
121 |
disc: term, |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
122 |
sels: term list}; |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
123 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
124 |
type corec_ctr_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
125 |
{ctr: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
126 |
disc: term, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
127 |
sels: term list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
128 |
pred: int option, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
129 |
calls: corec_call list, |
53705 | 130 |
discI: thm, |
131 |
sel_thms: thm list, |
|
53475 | 132 |
collapse: thm, |
133 |
corec_thm: thm, |
|
134 |
disc_corec: thm, |
|
135 |
sel_corecs: thm list}; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
136 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
137 |
type rec_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
138 |
{recx: term, |
53329 | 139 |
nested_map_idents: thm list, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
140 |
nested_map_comps: thm list, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
141 |
ctr_specs: rec_ctr_spec list}; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
142 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
143 |
type corec_spec = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
144 |
{corec: term, |
53475 | 145 |
nested_maps: thm list, |
146 |
nested_map_idents: thm list, |
|
147 |
nested_map_comps: thm list, |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
148 |
ctr_specs: corec_ctr_spec list}; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
149 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
150 |
val id_def = @{thm id_def}; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
151 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
152 |
exception AINT_NO_MAP of term; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
153 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
154 |
fun not_codatatype ctxt T = |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
155 |
error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
156 |
fun ill_formed_rec_call ctxt t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
157 |
error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
158 |
fun ill_formed_corec_call ctxt t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
159 |
error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
160 |
fun invalid_map ctxt t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
161 |
error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
162 |
fun unexpected_rec_call ctxt t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
163 |
error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
164 |
fun unexpected_corec_call ctxt t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
165 |
error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
166 |
|
53878 | 167 |
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True}; |
168 |
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False}; |
|
169 |
||
54067 | 170 |
val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts; |
53878 | 171 |
|
54067 | 172 |
fun s_not @{const True} = @{const False} |
173 |
| s_not @{const False} = @{const True} |
|
174 |
| s_not (@{const Not} $ t) = t |
|
175 |
| s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u |
|
176 |
| s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u |
|
177 |
| s_not t = @{const Not} $ t; |
|
53878 | 178 |
|
54067 | 179 |
val s_not_conj = conjuncts_s o s_not o mk_conjs; |
53878 | 180 |
|
54068 | 181 |
fun s_conj c @{const True} = c |
182 |
| s_conj c d = HOLogic.mk_conj (c, d); |
|
183 |
||
184 |
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs; |
|
185 |
||
186 |
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs; |
|
187 |
||
188 |
fun propagate_units css = |
|
189 |
(case List.partition (can the_single) css of |
|
190 |
([], _) => css |
|
191 |
| ([u] :: uss, css') => |
|
192 |
[u] :: propagate_units (map (propagate_unit_neg (s_not u)) |
|
193 |
(map (propagate_unit_pos u) (uss @ css')))); |
|
194 |
||
195 |
fun s_conjs cs = |
|
196 |
if member (op aconv) cs @{const False} then @{const False} |
|
197 |
else mk_conjs (remove (op aconv) @{const True} cs); |
|
198 |
||
199 |
fun s_disjs ds = |
|
200 |
if member (op aconv) ds @{const True} then @{const True} |
|
201 |
else mk_disjs (remove (op aconv) @{const False} ds); |
|
202 |
||
203 |
fun s_dnf css0 = |
|
204 |
let val css = propagate_units css0 in |
|
205 |
if null css then |
|
206 |
[@{const False}] |
|
207 |
else if exists null css then |
|
208 |
[] |
|
209 |
else |
|
210 |
map (fn c :: cs => (c, cs)) css |
|
211 |
|> AList.coalesce (op =) |
|
212 |
|> map (fn (c, css) => c :: s_dnf css) |
|
213 |
|> (fn [cs] => cs | css => [s_disjs (map s_conjs css)]) |
|
214 |
end; |
|
215 |
||
54202
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
216 |
fun mk_partial_comp gT fT g = |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
217 |
let val T = domain_type fT --> range_type gT in |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
218 |
Const (@{const_name Fun.comp}, gT --> fT --> T) $ g |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
219 |
end; |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
220 |
|
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
221 |
fun mk_partial_compN 0 _ _ g = g |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
222 |
| mk_partial_compN n gT fT g = |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
223 |
let val g' = mk_partial_compN (n - 1) gT (range_type fT) g in |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
224 |
mk_partial_comp (fastype_of g') fT g' |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
225 |
end; |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
226 |
|
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
227 |
fun mk_compN n bound_Ts (g, f) = |
54202
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
228 |
let val typof = curry fastype_of1 bound_Ts in |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
229 |
mk_partial_compN n (typof g) (typof f) g $ f |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
230 |
end; |
0a06b51ffa56
handle applied ctor arguments gracefully when computing 'callssss' (for recursion through functions)
blanchet
parents:
54200
diff
changeset
|
231 |
|
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
232 |
val mk_comp = mk_compN 1; |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
233 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
234 |
fun factor_out_types ctxt massage destU U T = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
235 |
(case try destU U of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
236 |
SOME (U1, U2) => if U1 = T then massage T U2 else invalid_map ctxt |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
237 |
| NONE => invalid_map ctxt); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
238 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
239 |
fun map_flattened_map_args ctxt s map_args fs = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
240 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
241 |
val flat_fs = flatten_type_args_of_bnf (the (bnf_of ctxt s)) Term.dummy fs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
242 |
val flat_fs' = map_args flat_fs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
243 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
244 |
permute_like (op aconv) flat_fs fs flat_fs' |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
245 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
246 |
|
54102 | 247 |
fun massage_nested_rec_call ctxt has_call raw_massage_fun bound_Ts y y' = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
248 |
let |
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
249 |
fun check_no_call t = if has_call t then unexpected_rec_call ctxt t else (); |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
250 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
251 |
val typof = curry fastype_of1 bound_Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
252 |
val build_map_fst = build_map ctxt (fst_const o fst); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
253 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
254 |
val yT = typof y; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
255 |
val yU = typof y'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
256 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
257 |
fun y_of_y' () = build_map_fst (yU, yT) $ y'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
258 |
val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
259 |
|
54102 | 260 |
fun massage_mutual_fun U T t = |
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
261 |
(case t of |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
262 |
Const (@{const_name comp}, comp_T) $ t1 $ t2 => |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
263 |
mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2) |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
264 |
| _ => |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
265 |
if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t |
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
266 |
else mk_comp bound_Ts (t, build_map_fst (U, T))); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
267 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
268 |
fun massage_map (Type (_, Us)) (Type (s, Ts)) t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
269 |
(case try (dest_map ctxt s) t of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
270 |
SOME (map0, fs) => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
271 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
272 |
val Type (_, ran_Ts) = range_type (typof t); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
273 |
val map' = mk_map (length fs) Us ran_Ts map0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
274 |
val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
275 |
in |
53870 | 276 |
Term.list_comb (map', fs') |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
277 |
end |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
278 |
| NONE => raise AINT_NO_MAP t) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
279 |
| massage_map _ _ t = raise AINT_NO_MAP t |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
280 |
and massage_map_or_map_arg U T t = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
281 |
if T = U then |
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
282 |
tap check_no_call t |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
283 |
else |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
284 |
massage_map U T t |
54102 | 285 |
handle AINT_NO_MAP _ => massage_mutual_fun U T t; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
286 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
287 |
fun massage_call (t as t1 $ t2) = |
54170
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
288 |
if has_call t then |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
289 |
if t2 = y then |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
290 |
massage_map yU yT (elim_y t1) $ y' |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
291 |
handle AINT_NO_MAP t' => invalid_map ctxt t' |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
292 |
else |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
293 |
let val (g, xs) = Term.strip_comb t2 in |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
294 |
if g = y then |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
295 |
if exists has_call xs then unexpected_rec_call ctxt t2 |
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
296 |
else Term.list_comb (massage_call (mk_compN (length xs) bound_Ts (t1, y)), xs) |
54170
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
297 |
else |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
298 |
ill_formed_rec_call ctxt t |
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
299 |
end |
54162
faa9c35fe79b
handle composition for multiple arguments correctly
blanchet
parents:
54159
diff
changeset
|
300 |
else |
54170
402fcacb5c88
gracefully handle case where a nested recursive variable appears directly on the rhs of a primcorec equation
blanchet
parents:
54162
diff
changeset
|
301 |
elim_y t |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
302 |
| massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
303 |
in |
53724 | 304 |
massage_call |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
305 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
306 |
|
53909 | 307 |
fun fold_rev_let_if_case ctxt f bound_Ts t = |
53866 | 308 |
let |
53870 | 309 |
val thy = Proof_Context.theory_of ctxt; |
310 |
||
53871 | 311 |
fun fld conds t = |
53866 | 312 |
(case Term.strip_comb t of |
54135 | 313 |
(Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t) |
53871 | 314 |
| (Const (@{const_name If}, _), [cond, then_branch, else_branch]) => |
54199
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
315 |
fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch |
53896 | 316 |
| (Const (c, _), args as _ :: _ :: _) => |
317 |
let val n = num_binder_types (Sign.the_const_type thy c) - 1 in |
|
53924 | 318 |
if n >= 0 andalso n < length args then |
53896 | 319 |
(case fastype_of1 (bound_Ts, nth args n) of |
320 |
Type (s, Ts) => |
|
321 |
(case dest_case ctxt s Ts t of |
|
53909 | 322 |
NONE => apsnd (f conds t) |
53896 | 323 |
| SOME (conds', branches) => |
53909 | 324 |
apfst (cons s) o fold_rev (uncurry fld) |
54067 | 325 |
(map (append conds o conjuncts_s) conds' ~~ branches)) |
53909 | 326 |
| _ => apsnd (f conds t)) |
53896 | 327 |
else |
53909 | 328 |
apsnd (f conds t) |
53866 | 329 |
end |
53909 | 330 |
| _ => apsnd (f conds t)) |
53866 | 331 |
in |
53909 | 332 |
fld [] t o pair [] |
53866 | 333 |
end; |
334 |
||
53870 | 335 |
fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex); |
336 |
||
53890 | 337 |
fun massage_let_if_case ctxt has_call massage_leaf = |
53723 | 338 |
let |
53888 | 339 |
val thy = Proof_Context.theory_of ctxt; |
340 |
||
341 |
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); |
|
53835
687116951569
started adding support for "nat_case" as case study for all "case" constructs
blanchet
parents:
53833
diff
changeset
|
342 |
|
54105 | 343 |
fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t |
344 |
| massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t) |
|
345 |
| massage_abs bound_Ts m t = |
|
346 |
let val T = domain_type (fastype_of1 (bound_Ts, t)) in |
|
347 |
Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0)) |
|
348 |
end |
|
53893 | 349 |
and massage_rec bound_Ts t = |
53890 | 350 |
let val typof = curry fastype_of1 bound_Ts in |
351 |
(case Term.strip_comb t of |
|
54135 | 352 |
(Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t) |
53893 | 353 |
| (Const (@{const_name If}, _), obj :: (branches as [_, _])) => |
53890 | 354 |
let val branches' = map (massage_rec bound_Ts) branches in |
355 |
Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches') |
|
356 |
end |
|
54105 | 357 |
| (Const (c, _), args as _ :: _ :: _) => |
54199
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
358 |
(case try strip_fun_type (Sign.the_const_type thy c) of |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
359 |
SOME (gen_branch_Ts, gen_body_fun_T) => |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
360 |
let |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
361 |
val gen_branch_ms = map num_binder_types gen_branch_Ts; |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
362 |
val n = length gen_branch_ms; |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
363 |
in |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
364 |
if n < length args then |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
365 |
(case gen_body_fun_T of |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
366 |
Type (_, [Type (T_name, _), _]) => |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
367 |
if case_of ctxt T_name = SOME c then |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
368 |
let |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
369 |
val (branches, obj_leftovers) = chop n args; |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
370 |
val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches; |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
371 |
val branch_Ts' = map typof branches'; |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
372 |
val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts')); |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
373 |
val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T'); |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
374 |
in |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
375 |
Term.list_comb (casex', branches' @ tap (List.app check_no_call) obj_leftovers) |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
376 |
end |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
377 |
else |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
378 |
massage_leaf bound_Ts t |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
379 |
| _ => massage_leaf bound_Ts t) |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
380 |
else |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
381 |
massage_leaf bound_Ts t |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
382 |
end |
20a52b55f8ea
watch out for 'case' constant canditates whose general type is 'a (e.g. 'undefined')
blanchet
parents:
54188
diff
changeset
|
383 |
| NONE => massage_leaf bound_Ts t) |
53890 | 384 |
| _ => massage_leaf bound_Ts t) |
385 |
end |
|
53723 | 386 |
in |
387 |
massage_rec |
|
388 |
end; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
389 |
|
54102 | 390 |
val massage_mutual_corec_call = massage_let_if_case; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
391 |
|
54016
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
392 |
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T; |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
393 |
|
54102 | 394 |
fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
395 |
let |
54205
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
396 |
fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else (); |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
397 |
|
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
398 |
val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
399 |
|
54102 | 400 |
fun massage_mutual_call bound_Ts U T t = |
53890 | 401 |
if has_call t then factor_out_types ctxt (raw_massage_call bound_Ts) dest_sumT U T t |
53411 | 402 |
else build_map_Inl (T, U) $ t; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
403 |
|
54102 | 404 |
fun massage_mutual_fun bound_Ts U T t = |
54205
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
405 |
(case t of |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
406 |
Const (@{const_name comp}, comp_T) $ t1 $ t2 => |
54206
1c26d55b8d73
align 'primrec_new' on 'primcorec' (+ got rid of one more 'dummyT')
blanchet
parents:
54205
diff
changeset
|
407 |
mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2) |
54205
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
408 |
| _ => |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
409 |
let |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
410 |
val var = Var ((Name.uu, Term.maxidx_of_term t + 1), |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
411 |
domain_type (fastype_of1 (bound_Ts, t))); |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
412 |
in |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
413 |
Term.lambda var (massage_mutual_call bound_Ts U T (t $ var)) |
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
414 |
end); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
415 |
|
53890 | 416 |
fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
417 |
(case try (dest_map ctxt s) t of |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
418 |
SOME (map0, fs) => |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
419 |
let |
53890 | 420 |
val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t)); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
421 |
val map' = mk_map (length fs) dom_Ts Us map0; |
53890 | 422 |
val fs' = |
423 |
map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
424 |
in |
53870 | 425 |
Term.list_comb (map', fs') |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
426 |
end |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
427 |
| NONE => raise AINT_NO_MAP t) |
53890 | 428 |
| massage_map _ _ _ t = raise AINT_NO_MAP t |
429 |
and massage_map_or_map_arg bound_Ts U T t = |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
430 |
if T = U then |
54205
bdb83bc60780
convenience: handle composition gracefully in map in 'primcorec', analogously to 'primrec_new'
blanchet
parents:
54202
diff
changeset
|
431 |
tap check_no_call t |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
432 |
else |
53890 | 433 |
massage_map bound_Ts U T t |
54102 | 434 |
handle AINT_NO_MAP _ => massage_mutual_fun bound_Ts U T t; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
435 |
|
53890 | 436 |
fun massage_call bound_Ts U T = |
437 |
massage_let_if_case ctxt has_call (fn bound_Ts => fn t => |
|
53732
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
438 |
if has_call t then |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
439 |
(case U of |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
440 |
Type (s, Us) => |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
441 |
(case try (dest_ctr ctxt s) t of |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
442 |
SOME (f, args) => |
53890 | 443 |
let |
444 |
val typof = curry fastype_of1 bound_Ts; |
|
445 |
val f' = mk_ctr Us f |
|
446 |
val f'_T = typof f'; |
|
447 |
val arg_Ts = map typof args; |
|
448 |
in |
|
449 |
Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args) |
|
53732
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
450 |
end |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
451 |
| NONE => |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
452 |
(case t of |
54016
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
453 |
Const (@{const_name prod_case}, _) $ t' => |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
454 |
let |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
455 |
val U' = curried_type U; |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
456 |
val T' = curried_type T; |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
457 |
in |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
458 |
Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t' |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
459 |
end |
769fcbdf2918
allow uncurried lambda-abstractions on rhs of "primcorec"
blanchet
parents:
54009
diff
changeset
|
460 |
| t1 $ t2 => |
53732
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
461 |
(if has_call t2 then |
54102 | 462 |
massage_mutual_call bound_Ts U T t |
53732
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
463 |
else |
53890 | 464 |
massage_map bound_Ts U T t1 $ t2 |
54102 | 465 |
handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t) |
53890 | 466 |
| Abs (s, T', t') => |
467 |
Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t') |
|
54102 | 468 |
| _ => massage_mutual_call bound_Ts U T t)) |
53732
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
469 |
| _ => ill_formed_corec_call ctxt t) |
e2c0d0426d2b
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
blanchet
parents:
53731
diff
changeset
|
470 |
else |
53889 | 471 |
build_map_Inl (T, U) $ t) bound_Ts; |
53960 | 472 |
|
473 |
val T = fastype_of1 (bound_Ts, t); |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
474 |
in |
53960 | 475 |
if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
476 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
477 |
|
54188 | 478 |
val fold_rev_corec_call = fold_rev_let_if_case; |
479 |
||
54159
eb5d58c99049
set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents:
54137
diff
changeset
|
480 |
fun expand_to_ctr_term ctxt s Ts t = |
53867
8ad44ecc0d15
keep a database of free constructor type information
blanchet
parents:
53866
diff
changeset
|
481 |
(case ctr_sugar_of ctxt s of |
53870 | 482 |
SOME {ctrs, casex, ...} => |
483 |
Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t |
|
54159
eb5d58c99049
set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents:
54137
diff
changeset
|
484 |
| NONE => raise Fail "expand_to_ctr_term"); |
53726
d41a30db83d9
added massaging function for primcorec code equations
blanchet
parents:
53725
diff
changeset
|
485 |
|
53727
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
486 |
fun expand_corec_code_rhs ctxt has_call bound_Ts t = |
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
487 |
(case fastype_of1 (bound_Ts, t) of |
53889 | 488 |
Type (s, Ts) => |
53893 | 489 |
massage_let_if_case ctxt has_call (fn _ => fn t => |
54159
eb5d58c99049
set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents:
54137
diff
changeset
|
490 |
if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t |
53727
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
491 |
| _ => raise Fail "expand_corec_code_rhs"); |
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
492 |
|
1d88a7ee4e3e
split functionality into two functions to avoid redoing work over and over
blanchet
parents:
53726
diff
changeset
|
493 |
fun massage_corec_code_rhs ctxt massage_ctr = |
53890 | 494 |
massage_let_if_case ctxt (K false) |
495 |
(fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb); |
|
53865 | 496 |
|
53871 | 497 |
fun fold_rev_corec_code_rhs ctxt f = |
53909 | 498 |
snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb); |
499 |
||
500 |
fun case_thms_of_term ctxt bound_Ts t = |
|
501 |
let |
|
502 |
val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t (); |
|
503 |
val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names; |
|
504 |
in |
|
53925 | 505 |
(maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars, |
506 |
maps #sel_split_asms ctr_sugars) |
|
53909 | 507 |
end; |
53731 | 508 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
509 |
fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
510 |
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
|
511 |
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
|
512 |
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
|
513 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
514 |
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
|
515 |
|
54238 | 516 |
(*FIXME: remove special cases for product and sum once they are registered as datatypes*) |
53476
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
517 |
fun map_thms_of_typ ctxt (Type (s, _)) = |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
518 |
if s = @{type_name prod} then |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
519 |
@{thms map_pair_simp} |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
520 |
else if s = @{type_name sum} then |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
521 |
@{thms sum_map.simps} |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
522 |
else |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
523 |
(case fp_sugar_of ctxt s of |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
524 |
SOME {index, mapss, ...} => nth mapss index |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
525 |
| NONE => []) |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
526 |
| map_thms_of_typ _ _ = []; |
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
527 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
528 |
fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
529 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
530 |
val thy = Proof_Context.theory_of lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
531 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
532 |
val ((missing_arg_Ts, perm0_kks, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
533 |
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = ctor_iters1 :: _, ...}, |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
534 |
co_inducts = [induct_thm], ...} :: _, (lfp_sugar_thms, _)), lthy') = |
54009 | 535 |
nested_to_mutual_fps Least_FP bs arg_Ts get_indices callssss0 lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
536 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
537 |
val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
538 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
539 |
val indices = map #index fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
540 |
val perm_indices = map #index perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
541 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
542 |
val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
543 |
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
544 |
val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
545 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
546 |
val nn0 = length arg_Ts; |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
547 |
val nn = length perm_lfpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
548 |
val kks = 0 upto nn - 1; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
549 |
val perm_ns = map length perm_ctr_Tsss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
550 |
val perm_mss = map (map length) perm_ctr_Tsss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
551 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
552 |
val perm_Cs = map (body_type o fastype_of o co_rec_of o of_fp_sugar (#xtor_co_iterss o #fp_res)) |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
553 |
perm_fp_sugars; |
53592
5a7bf8c859f6
made non-co case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset
|
554 |
val perm_fun_arg_Tssss = |
5a7bf8c859f6
made non-co case more robust as well (cf. b6e2993fd0d3)
blanchet
parents:
53591
diff
changeset
|
555 |
mk_iter_fun_arg_types perm_ctr_Tsss perm_ns perm_mss (co_rec_of ctor_iters1); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
556 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
557 |
fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
558 |
fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
559 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
560 |
val induct_thms = unpermute0 (conj_dests nn induct_thm); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
561 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
562 |
val lfpTs = unpermute perm_lfpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
563 |
val Cs = unpermute perm_Cs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
564 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
565 |
val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
566 |
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
567 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
568 |
val substA = Term.subst_TVars As_rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
569 |
val substAT = Term.typ_subst_TVars As_rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
570 |
val substCT = Term.typ_subst_TVars Cs_rho; |
54200 | 571 |
val substACT = substAT o substCT; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
572 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
573 |
val perm_Cs' = map substCT perm_Cs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
574 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
575 |
fun offset_of_ctr 0 _ = 0 |
53974 | 576 |
| offset_of_ctr n (({ctrs, ...} : ctr_sugar) :: ctr_sugars) = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
577 |
length ctrs + offset_of_ctr (n - 1) ctr_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
578 |
|
54200 | 579 |
fun call_of [i] [T] = (if exists_subtype_in Cs T then Nested_Rec else No_Rec) (i, substACT T) |
580 |
| call_of [i, i'] [T, T'] = Mutual_Rec ((i, substACT T), (i', substACT T')); |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
581 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
582 |
fun mk_ctr_spec ctr offset fun_arg_Tss rec_thm = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
583 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
584 |
val (fun_arg_hss, _) = indexedd fun_arg_Tss 0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
585 |
val fun_arg_hs = flat_rec_arg_args fun_arg_hss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
586 |
val fun_arg_iss = map (map (find_index_eq fun_arg_hs)) fun_arg_hss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
587 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
588 |
{ctr = substA ctr, offset = offset, calls = map2 call_of fun_arg_iss fun_arg_Tss, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
589 |
rec_thm = rec_thm} |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
590 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
591 |
|
53974 | 592 |
fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) iter_thmsss = |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
593 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
594 |
val ctrs = #ctrs (nth ctr_sugars index); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
595 |
val rec_thmss = co_rec_of (nth iter_thmsss index); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
596 |
val k = offset_of_ctr index ctr_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
597 |
val n = length ctrs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
598 |
in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
599 |
map4 mk_ctr_spec ctrs (k upto k + n - 1) (nth perm_fun_arg_Tssss index) rec_thmss |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
600 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
601 |
|
53974 | 602 |
fun mk_spec ({T, index, ctr_sugars, co_iterss = iterss, co_iter_thmsss = iter_thmsss, ...} |
603 |
: fp_sugar) = |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
604 |
{recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' (co_rec_of (nth iterss index)), |
53329 | 605 |
nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
606 |
nested_map_comps = map map_comp_of_bnf nested_bnfs, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
607 |
ctr_specs = mk_ctr_specs index ctr_sugars iter_thmsss}; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
608 |
in |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
609 |
((is_some lfp_sugar_thms, map mk_spec fp_sugars, missing_arg_Ts, induct_thm, induct_thms), |
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
610 |
lthy') |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
611 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
612 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
613 |
fun basic_corec_specs_of ctxt res_T = |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
614 |
(case res_T of |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
615 |
Type (T_name, _) => |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
616 |
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
617 |
NONE => not_codatatype ctxt res_T |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
618 |
| SOME {ctrs, discs, selss, ...} => |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
619 |
let |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
620 |
val thy = Proof_Context.theory_of ctxt; |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
621 |
val gfpT = body_type (fastype_of (hd ctrs)); |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
622 |
val As_rho = tvar_subst thy [gfpT] [res_T]; |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
623 |
val substA = Term.subst_TVars As_rho; |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
624 |
|
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
625 |
fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels}; |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
626 |
in |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
627 |
map3 mk_spec ctrs discs selss |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
628 |
end) |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
629 |
| _ => not_codatatype ctxt res_T); |
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
630 |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
631 |
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
632 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
633 |
val thy = Proof_Context.theory_of lthy; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
634 |
|
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
635 |
val ((missing_res_Ts, perm0_kks, |
53475 | 636 |
fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
637 |
co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') = |
54009 | 638 |
nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
639 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
640 |
val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
641 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
642 |
val indices = map #index fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
643 |
val perm_indices = map #index perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
644 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
645 |
val perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
646 |
val perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss; |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
647 |
val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
648 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
649 |
val nn0 = length res_Ts; |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
650 |
val nn = length perm_gfpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
651 |
val kks = 0 upto nn - 1; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
652 |
val perm_ns = map length perm_ctr_Tsss; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
653 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
654 |
val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
655 |
of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
656 |
val (perm_p_Tss, (perm_q_Tssss, _, perm_f_Tssss, _)) = |
53591 | 657 |
mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
658 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
659 |
val (perm_p_hss, h) = indexedd perm_p_Tss 0; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
660 |
val (perm_q_hssss, h') = indexedddd perm_q_Tssss h; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
661 |
val (perm_f_hssss, _) = indexedddd perm_f_Tssss h'; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
662 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
663 |
val fun_arg_hs = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
664 |
flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
665 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
666 |
fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
667 |
fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
668 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
669 |
val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
670 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
671 |
val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
672 |
val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
673 |
val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
674 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
675 |
val f_Tssss = unpermute perm_f_Tssss; |
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
676 |
val gfpTs = unpermute perm_gfpTs; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
677 |
val Cs = unpermute perm_Cs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
678 |
|
54134
b26baa7f8262
added helper function (that solves chicken-and-egg problem w.r.t. "callssss")
blanchet
parents:
54105
diff
changeset
|
679 |
val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts; |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
680 |
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
681 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
682 |
val substA = Term.subst_TVars As_rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
683 |
val substAT = Term.typ_subst_TVars As_rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
684 |
val substCT = Term.typ_subst_TVars Cs_rho; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
685 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
686 |
val perm_Cs' = map substCT perm_Cs; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
687 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
688 |
fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] = |
54102 | 689 |
(if exists_subtype_in Cs T then Nested_Corec |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
690 |
else if nullary then Dummy_No_Corec |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
691 |
else No_Corec) g_i |
54102 | 692 |
| call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i'); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
693 |
|
53705 | 694 |
fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm |
695 |
disc_corec sel_corecs = |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
696 |
let val nullary = not (can dest_funT (fastype_of ctr)) in |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
697 |
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho, |
53705 | 698 |
calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, |
699 |
collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec, |
|
700 |
sel_corecs = sel_corecs} |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
701 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
702 |
|
54241 | 703 |
fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss |
704 |
disc_coitersss sel_coiterssss = |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
705 |
let |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
706 |
val ctrs = #ctrs (nth ctr_sugars index); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
707 |
val discs = #discs (nth ctr_sugars index); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
708 |
val selss = #selss (nth ctr_sugars index); |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
709 |
val p_ios = map SOME p_is @ [NONE]; |
53705 | 710 |
val discIs = #discIs (nth ctr_sugars index); |
711 |
val sel_thmss = #sel_thmss (nth ctr_sugars index); |
|
53475 | 712 |
val collapses = #collapses (nth ctr_sugars index); |
713 |
val corec_thms = co_rec_of (nth coiter_thmsss index); |
|
53741
c9068aade859
killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'
blanchet
parents:
53734
diff
changeset
|
714 |
val disc_corecs = co_rec_of (nth disc_coitersss index); |
53475 | 715 |
val sel_corecss = co_rec_of (nth sel_coiterssss index); |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
716 |
in |
53705 | 717 |
map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses |
718 |
corec_thms disc_corecs sel_corecss |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
719 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
720 |
|
53974 | 721 |
fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, |
722 |
disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar) |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
723 |
p_is q_isss f_isss f_Tsss = |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
724 |
{corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)), |
53476
eb3865c3ee58
include map theorems in datastructure for "primcorec"
blanchet
parents:
53475
diff
changeset
|
725 |
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, |
53475 | 726 |
nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs, |
727 |
nested_map_comps = map map_comp_of_bnf nested_bnfs, |
|
728 |
ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss |
|
729 |
disc_coitersss sel_coiterssss}; |
|
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
730 |
in |
53746
bd038e48526d
have "datatype_new_compat" register induction and recursion theorems in nested case
blanchet
parents:
53741
diff
changeset
|
731 |
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts, |
53303
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
732 |
co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss, |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
733 |
strong_co_induct_of coinduct_thmss), lthy') |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
734 |
end; |
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
735 |
|
ae49b835ca01
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff
changeset
|
736 |
end; |