author | krauss |
Mon, 25 Jun 2007 12:16:27 +0200 | |
changeset 23494 | f985f9239e0d |
parent 23217 | 8eac3bda1063 |
child 23528 | 55597852285a |
permissions | -rw-r--r-- |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/mutual.ML |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
4 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
5 |
A package for general recursive function definitions. |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
6 |
Tools for mutual recursive definitions. |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
7 |
*) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
8 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
9 |
signature FUNDEF_MUTUAL = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
10 |
sig |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
11 |
|
22166 | 12 |
val prepare_fundef_mutual : FundefCommon.fundef_config |
13 |
-> string (* defname *) |
|
14 |
-> ((string * typ) * mixfix) list |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
15 |
-> term list |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
16 |
-> local_theory |
22166 | 17 |
-> ((thm (* goalstate *) |
18 |
* (thm -> FundefCommon.fundef_result) (* proof continuation *) |
|
19 |
* (thm list -> thm list list) (* sorting continuation *) |
|
20 |
) * local_theory) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
21 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
22 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
23 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
24 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
25 |
structure FundefMutual: FUNDEF_MUTUAL = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
26 |
struct |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
27 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20949
diff
changeset
|
28 |
open FundefLib |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
29 |
open FundefCommon |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
30 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
31 |
(* Theory dependencies *) |
22622
25693088396b
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
krauss
parents:
22620
diff
changeset
|
32 |
val sum_case_rules = thms "Sum_Type.sum_cases" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
33 |
val split_apply = thm "Product_Type.split" |
23494 | 34 |
val projl_inl = thm "Sum_Type.Projl_Inl" |
35 |
val projr_inr = thm "Sum_Type.Projr_Inr" |
|
36 |
||
37 |
||
38 |
(* Sum types *) |
|
39 |
fun mk_sumT LT RT = Type ("+", [LT, RT]) |
|
40 |
fun mk_sumcase TL TR T l r = Const (@{const_name "Sum_Type.sum_case"}, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
|
41 |
||
42 |
val App = curry op $ |
|
43 |
||
44 |
fun mk_inj ST n i = |
|
45 |
BalancedTree.access |
|
46 |
{ init = (ST, I : term -> term), |
|
47 |
left = (fn (T as Type ("+", [LT, RT]), inj) => (LT, App (Const (@{const_name "Inl"}, LT --> T)) o inj)), |
|
48 |
right =(fn (T as Type ("+", [LT, RT]), inj) => (RT, App (Const (@{const_name "Inr"}, RT --> T)) o inj))} n i |
|
49 |
|> snd |
|
50 |
||
51 |
fun mk_proj ST n i = |
|
52 |
BalancedTree.access |
|
53 |
{ init = (ST, I : term -> term), |
|
54 |
left = (fn (T as Type ("+", [LT, RT]), proj) => (LT, proj o App (Const (@{const_name "Projl"}, T --> LT)))), |
|
55 |
right =(fn (T as Type ("+", [LT, RT]), proj) => (RT, proj o App (Const (@{const_name "Projr"}, T --> RT))))} n i |
|
56 |
|> snd |
|
57 |
||
58 |
fun mk_sumcases T fs = |
|
59 |
BalancedTree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) |
|
60 |
(map (fn f => (f, domain_type (fastype_of f))) fs) |
|
61 |
|> fst |
|
62 |
||
63 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
64 |
|
22166 | 65 |
type qgar = string * (string * typ) list * term list * term list * term |
66 |
||
23217 | 67 |
fun name_of_fqgar ((f, _, _, _, _): qgar) = f |
22166 | 68 |
|
69 |
datatype mutual_part = |
|
70 |
MutualPart of |
|
71 |
{ |
|
23494 | 72 |
i : int, |
73 |
i' : int, |
|
22166 | 74 |
fvar : string * typ, |
75 |
cargTs: typ list, |
|
76 |
f_def: term, |
|
77 |
||
78 |
f: term option, |
|
79 |
f_defthm : thm option |
|
80 |
} |
|
81 |
||
82 |
||
83 |
datatype mutual_info = |
|
84 |
Mutual of |
|
85 |
{ |
|
23494 | 86 |
n : int, |
87 |
n' : int, |
|
22166 | 88 |
fsum_var : string * typ, |
89 |
||
90 |
ST: typ, |
|
91 |
RST: typ, |
|
92 |
||
93 |
parts: mutual_part list, |
|
94 |
fqgars: qgar list, |
|
95 |
qglrs: ((string * typ) list * term list * term * term) list, |
|
96 |
||
97 |
fsum : term option |
|
98 |
} |
|
99 |
||
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
100 |
fun mutual_induct_Pnames n = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
101 |
if n < 5 then fst (chop n ["P","Q","R","S"]) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
102 |
else map (fn i => "P" ^ string_of_int i) (1 upto n) |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
103 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
104 |
fun get_part fname = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
105 |
the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname) |
21237 | 106 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
107 |
(* FIXME *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
108 |
fun mk_prod_abs e (t1, t2) = |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
109 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
110 |
val bTs = rev (map snd e) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
111 |
val T1 = fastype_of1 (bTs, t1) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
112 |
val T2 = fastype_of1 (bTs, t2) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
113 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
114 |
HOLogic.pair_const T1 T2 $ t1 $ t2 |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
115 |
end; |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
116 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
117 |
|
22166 | 118 |
fun analyze_eqs ctxt defname fs eqs = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
119 |
let |
23494 | 120 |
val num = length fs |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
121 |
val fnames = map fst fs |
23189 | 122 |
val fqgars = map split_def eqs |
123 |
val arities = mk_arities fqgars |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
124 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
125 |
fun curried_types (fname, fT) = |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
126 |
let |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20534
diff
changeset
|
127 |
val k = the_default 1 (Symtab.lookup arities fname) |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
128 |
val (caTs, uaTs) = chop k (binder_types fT) |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
129 |
in |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
130 |
(caTs, uaTs ---> body_type fT) |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
131 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
132 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
133 |
val (caTss, resultTs) = split_list (map curried_types fs) |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
134 |
val argTs = map (foldr1 HOLogic.mk_prodT) caTss |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
135 |
|
23494 | 136 |
val dresultTs = distinct (Type.eq_type Vartab.empty) resultTs |
137 |
val n' = length dresultTs |
|
138 |
||
139 |
val RST = BalancedTree.make (uncurry mk_sumT) dresultTs |
|
140 |
val ST = BalancedTree.make (uncurry mk_sumT) argTs |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
141 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
142 |
val fsum_type = ST --> RST |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
143 |
|
22166 | 144 |
val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
145 |
val fsum_var = (fsum_var_name, fsum_type) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
146 |
|
23494 | 147 |
fun define (fvar as (n, T)) caTs resultT i = |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
148 |
let |
23494 | 149 |
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) |
150 |
val i' = find_index (fn Ta => Type.eq_type Vartab.empty (Ta, resultT)) dresultTs + 1 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
151 |
|
23494 | 152 |
val f_exp = mk_proj RST n' i' (Free fsum_var $ mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
153 |
val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
154 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
155 |
val rew = (n, fold_rev lambda vars f_exp) |
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
156 |
in |
23494 | 157 |
(MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew) |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
158 |
end |
21237 | 159 |
|
23494 | 160 |
val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num)) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
161 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
162 |
fun convert_eqs (f, qs, gs, args, rhs) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
163 |
let |
23494 | 164 |
val MutualPart {i, i', ...} = get_part f parts |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
165 |
in |
23494 | 166 |
(qs, gs, mk_inj ST num i (foldr1 (mk_prod_abs qs) args), |
167 |
mk_inj RST n' i' (replace_frees rews rhs) |
|
168 |
|> Envir.beta_norm) |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
169 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
170 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
171 |
val qglrs = map convert_eqs fqgars |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
172 |
in |
23494 | 173 |
Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
174 |
parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE} |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
175 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
176 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
177 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
178 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
179 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
180 |
fun define_projections fixes mutual fsum lthy = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
181 |
let |
23494 | 182 |
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
183 |
let |
21436 | 184 |
val ((f, (_, f_defthm)), lthy') = |
185 |
LocalTheory.def Thm.internalK ((fname, mixfix), |
|
186 |
((fname ^ "_def", []), Term.subst_bound (fsum, f_def))) |
|
187 |
lthy |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
188 |
in |
23494 | 189 |
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
21237 | 190 |
f=SOME f, f_defthm=SOME f_defthm }, |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
191 |
lthy') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
192 |
end |
21237 | 193 |
|
23494 | 194 |
val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
195 |
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
196 |
in |
23494 | 197 |
(Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts', |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
198 |
fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum }, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
199 |
lthy') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
200 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
201 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
202 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
203 |
fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm |
21237 | 204 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
205 |
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
206 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
207 |
val thy = ProofContext.theory_of ctxt |
21237 | 208 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
209 |
val oqnames = map fst pre_qs |
20797
c1f0bc7e7d80
renamed Variable.invent_fixes to Variable.variant_fixes;
wenzelm
parents:
20654
diff
changeset
|
210 |
val (qs, ctxt') = Variable.variant_fixes oqnames ctxt |
21237 | 211 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
212 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
213 |
fun inst t = subst_bounds (rev qs, t) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
214 |
val gs = map inst pre_gs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
215 |
val args = map inst pre_args |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
216 |
val rhs = inst pre_rhs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
217 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
218 |
val cqs = map (cterm_of thy) qs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
219 |
val ags = map (assume o cterm_of thy) gs |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
220 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
221 |
val import = fold forall_elim cqs |
23494 | 222 |
#> fold (flip implies_elim) ags |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
223 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
224 |
val export = fold_rev (implies_intr o cprop_of) ags |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
225 |
#> fold_rev forall_intr_rename (oqnames ~~ cqs) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
226 |
in |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
227 |
F ctxt (f, qs, gs, args, rhs) import export |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
228 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
229 |
|
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
230 |
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) import (export : thm -> thm) sum_psimp_eq = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
231 |
let |
23494 | 232 |
val (MutualPart {f=SOME f, f_defthm=SOME f_def, ...}) = get_part fname parts |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
233 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
234 |
val psimp = import sum_psimp_eq |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
235 |
val (simp, restore_cond) = case cprems_of psimp of |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
236 |
[] => (psimp, I) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
237 |
| [cond] => (implies_elim psimp (assume cond), implies_intr cond) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
238 |
| _ => sys_error "Too many conditions" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
239 |
in |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
240 |
Goal.prove ctxt [] [] |
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
241 |
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
242 |
(fn _ => SIMPSET (unfold_tac all_orig_fdefs) |
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
243 |
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
23494 | 244 |
THEN SIMPSET' (fn ss => simp_tac (ss addsimps [projl_inl, projr_inr])) 1) |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
245 |
|> restore_cond |
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
246 |
|> export |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
247 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
248 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
249 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
250 |
(* FIXME HACK *) |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
251 |
fun mk_applied_form ctxt caTs thm = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
252 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
253 |
val thy = ProofContext.theory_of ctxt |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
254 |
val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
255 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
256 |
fold (fn x => fn thm => combination thm (reflexive x)) xs thm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
257 |
|> beta_reduce |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
258 |
|> fold_rev forall_intr xs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
259 |
|> forall_elim_vars 0 |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
260 |
end |
23494 | 261 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
262 |
|
23494 | 263 |
fun mutual_induct_rules lthy induct all_f_defs (Mutual {n, ST, RST, parts, ...}) = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
264 |
let |
22623 | 265 |
val cert = cterm_of (ProofContext.theory_of lthy) |
20949 | 266 |
val newPs = map2 (fn Pname => fn MutualPart {cargTs, ...} => |
21237 | 267 |
Free (Pname, cargTs ---> HOLogic.boolT)) |
20949 | 268 |
(mutual_induct_Pnames (length parts)) |
269 |
parts |
|
21237 | 270 |
|
271 |
fun mk_P (MutualPart {cargTs, ...}) P = |
|
272 |
let |
|
273 |
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs |
|
274 |
val atup = foldr1 HOLogic.mk_prod avars |
|
275 |
in |
|
276 |
tupled_lambda atup (list_comb (P, avars)) |
|
277 |
end |
|
278 |
||
279 |
val Ps = map2 mk_P parts newPs |
|
23494 | 280 |
val case_exp = mk_sumcases HOLogic.boolT Ps |
21237 | 281 |
|
282 |
val induct_inst = |
|
22623 | 283 |
forall_elim (cert case_exp) induct |
21237 | 284 |
|> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
285 |
|> full_simplify (HOL_basic_ss addsimps all_f_defs) |
|
286 |
||
23494 | 287 |
fun project rule (MutualPart {cargTs, i, ...}) = |
21237 | 288 |
let |
23494 | 289 |
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int j, T)) cargTs |
290 |
val inj = mk_inj ST n i (foldr1 HOLogic.mk_prod afs) |
|
21237 | 291 |
in |
292 |
rule |
|
22623 | 293 |
|> forall_elim (cert inj) |
21237 | 294 |
|> full_simplify (HOL_basic_ss addsimps (split_apply :: sum_case_rules)) |
22623 | 295 |
|> fold_rev (forall_intr o cert) (afs @ newPs) |
21237 | 296 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
297 |
in |
23494 | 298 |
map (project induct_inst) parts |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
299 |
end |
21237 | 300 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
301 |
|
22623 | 302 |
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
303 |
let |
22166 | 304 |
val result = inner_cont proof |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
305 |
val FundefResult {fs=[f], G, R, cases, psimps, trsimps, subset_pinducts=[subset_pinduct],simple_pinducts=[simple_pinduct], |
22166 | 306 |
termination,domintros} = result |
21237 | 307 |
|
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
308 |
val (all_f_defs, fs) = map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
309 |
(mk_applied_form lthy cargTs (symmetric f_def), f)) |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
310 |
parts |
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
311 |
|> split_list |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
312 |
|
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
313 |
val all_orig_fdefs = map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts |
21237 | 314 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
315 |
fun mk_mpsimp fqgar sum_psimp = |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
316 |
in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
21237 | 317 |
|
23189 | 318 |
val rew_ss = HOL_basic_ss addsimps all_f_defs |
22166 | 319 |
val mpsimps = map2 mk_mpsimp fqgars psimps |
320 |
val mtrsimps = map_option (map2 mk_mpsimp fqgars) trsimps |
|
22623 | 321 |
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
23189 | 322 |
val mtermination = full_simplify rew_ss termination |
323 |
val mdomintros = map_option (map (full_simplify rew_ss)) domintros |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
324 |
in |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22623
diff
changeset
|
325 |
FundefResult { fs=fs, G=G, R=R, |
22623 | 326 |
psimps=mpsimps, subset_pinducts=[subset_pinduct], simple_pinducts=minducts, |
327 |
cases=cases, termination=mtermination, |
|
23189 | 328 |
domintros=mdomintros, |
22623 | 329 |
trsimps=mtrsimps} |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
330 |
end |
21237 | 331 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
332 |
(* puts an object in the "right bucket" *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
333 |
fun store_grouped P x [] = [] |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
334 |
| store_grouped P x ((l, xs)::bs) = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
335 |
if P (x, l) then ((l, x::xs)::bs) else ((l, xs)::store_grouped P x bs) |
21237 | 336 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
337 |
fun sort_by_function (Mutual {fqgars, ...}) names xs = |
23217 | 338 |
fold_rev (store_grouped (op = o apfst fst)) (* fill *) |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
339 |
(map name_of_fqgar (Library.take (length xs, fqgars)) ~~ xs) (* the name-thm pairs *) |
21237 | 340 |
(map (rpair []) names) (* in the empty buckets labeled with names *) |
341 |
||
342 |
|> map (snd #> map snd) (* and remove the labels afterwards *) |
|
22166 | 343 |
|
344 |
||
23189 | 345 |
fun prepare_fundef_mutual config defname fixes eqss lthy = |
22166 | 346 |
let |
22323
b8c227d8ca91
beta_eta_contract specification befor processing. These normal forms avoid unpleasant surprises later on.
krauss
parents:
22244
diff
changeset
|
347 |
val mutual = analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) |
22166 | 348 |
val Mutual {fsum_var=(n, T), qglrs, ...} = mutual |
349 |
||
350 |
val ((fsum, goalstate, cont), lthy') = |
|
23189 | 351 |
FundefCore.prepare_fundef config defname [((n, T), NoSyn)] qglrs lthy |
22166 | 352 |
|
353 |
val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
|
354 |
||
355 |
val mutual_cont = mk_partial_rules_mutual lthy'' cont mutual' |
|
356 |
val sort_cont = sort_by_function mutual' (map (fst o fst) fixes) |
|
357 |
in |
|
358 |
((goalstate, mutual_cont, sort_cont), lthy'') |
|
359 |
end |
|
360 |
||
21237 | 361 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
362 |
end |