author | wenzelm |
Wed, 07 Aug 2019 10:42:34 +0200 | |
changeset 70479 | 02d08d0ba896 |
parent 67149 | e61557884799 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/mutual.ML |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
3 |
|
41114 | 4 |
Mutual recursive function definitions. |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
5 |
*) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
6 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
7 |
signature FUNCTION_MUTUAL = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
8 |
sig |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
9 |
val prepare_function_mutual : Function_Common.function_config |
63004 | 10 |
-> binding (* defname *) |
63011 | 11 |
-> ((binding * typ) * mixfix) list |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
12 |
-> term list |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
13 |
-> local_theory |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
14 |
-> ((thm (* goalstate *) |
60643 | 15 |
* (Proof.context -> thm -> Function_Common.function_result) (* proof continuation *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
16 |
) * local_theory) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
17 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
18 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
19 |
structure Function_Mutual: FUNCTION_MUTUAL = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
20 |
struct |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
21 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
22 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
23 |
open Function_Common |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
24 |
|
22166 | 25 |
type qgar = string * (string * typ) list * term list * term list * term |
26 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
27 |
datatype mutual_part = MutualPart of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
28 |
{i : int, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
29 |
i' : int, |
63011 | 30 |
fname : binding, |
31 |
fT : typ, |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
32 |
cargTs: typ list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
33 |
f_def: term, |
22166 | 34 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
35 |
f: term option, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
36 |
f_defthm : thm option} |
22166 | 37 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
38 |
datatype mutual_info = Mutual of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
39 |
{n : int, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
40 |
n' : int, |
63012 | 41 |
fsum_name : binding, |
42 |
fsum_type: typ, |
|
22166 | 43 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
44 |
ST: typ, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
45 |
RST: typ, |
22166 | 46 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
47 |
parts: mutual_part list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
48 |
fqgars: qgar list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
49 |
qglrs: ((string * typ) list * term list * term * term) list, |
22166 | 50 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
51 |
fsum : term option} |
22166 | 52 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
53 |
fun mutual_induct_Pnames n = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
54 |
if n < 5 then fst (chop n ["P","Q","R","S"]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
55 |
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
|
56 |
|
63011 | 57 |
fun get_part f = |
58 |
the o find_first (fn (MutualPart {fname, ...}) => Binding.name_of fname = f) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
59 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
60 |
(* FIXME *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
61 |
fun mk_prod_abs e (t1, t2) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
62 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
val bTs = rev (map snd e) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
64 |
val T1 = fastype_of1 (bTs, t1) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
65 |
val T2 = fastype_of1 (bTs, t2) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
67 |
HOLogic.pair_const T1 T2 $ t1 $ t2 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
68 |
end |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
69 |
|
22166 | 70 |
fun analyze_eqs ctxt defname fs eqs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
71 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
72 |
val num = length fs |
39276
2ad95934521f
improved error message for common mistake (fun f where "g x = ...")
krauss
parents:
36945
diff
changeset
|
73 |
val fqgars = map (split_def ctxt (K true)) eqs |
63011 | 74 |
fun arity_of fname = |
75 |
the (get_first (fn (f, _, _, args, _) => |
|
76 |
if f = Binding.name_of fname then SOME (length args) else NONE) fqgars) |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
77 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
78 |
fun curried_types (fname, fT) = |
63011 | 79 |
let val (caTs, uaTs) = chop (arity_of fname) (binder_types fT) |
80 |
in (caTs, uaTs ---> body_type fT) end |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
81 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
82 |
val (caTss, resultTs) = split_list (map curried_types fs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
83 |
val argTs = map (foldr1 HOLogic.mk_prodT) caTss |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
84 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
85 |
val dresultTs = distinct (op =) resultTs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
86 |
val n' = length dresultTs |
23494 | 87 |
|
55968 | 88 |
val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs |
89 |
val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
90 |
|
63012 | 91 |
val fsum_name = derived_name_suffix defname "_sum" |
92 |
val ([fsum_var_name], _) = Variable.add_fixes_binding [fsum_name] ctxt |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
93 |
val fsum_type = ST --> RST |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
94 |
val fsum_var = (fsum_var_name, fsum_type) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
95 |
|
63011 | 96 |
fun define (fname, fT) caTs resultT i = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
97 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
98 |
val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
99 |
val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1 |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
100 |
|
55968 | 101 |
val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
102 |
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
|
103 |
|
63011 | 104 |
val rew = (Binding.name_of fname, fold_rev lambda vars f_exp) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
105 |
in |
63011 | 106 |
(MutualPart |
107 |
{i = i, i' = i', fname = fname, fT = fT, cargTs = caTs, |
|
108 |
f_def = def, f = NONE, f_defthm = NONE}, rew) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
109 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
110 |
|
58634
9f10d82e8188
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents:
55968
diff
changeset
|
111 |
val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num)) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
112 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
113 |
fun convert_eqs (f, qs, gs, args, rhs) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
114 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
115 |
val MutualPart {i, i', ...} = get_part f parts |
42497
89acb654d8eb
inlined Function_Lib.replace_frees, which is used only once
krauss
parents:
42361
diff
changeset
|
116 |
val rhs' = rhs |
89acb654d8eb
inlined Function_Lib.replace_frees, which is used only once
krauss
parents:
42361
diff
changeset
|
117 |
|> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
118 |
in |
55968 | 119 |
(qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args), |
120 |
Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs')) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
121 |
end |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
122 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
123 |
val qglrs = map convert_eqs fqgars |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
124 |
in |
63012 | 125 |
Mutual {n = num, n' = n', fsum_name = fsum_name, fsum_type = fsum_type, |
126 |
ST = ST, RST = RST, parts = parts, fqgars = fqgars, qglrs = qglrs, fsum = NONE} |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
127 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
128 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
129 |
fun define_projections fixes mutual fsum lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
130 |
let |
63011 | 131 |
fun def ((MutualPart {i=i, i'=i', fname, fT, cargTs, f_def, ...}), (_, mixfix)) lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
132 |
let |
63011 | 133 |
val def_binding = Thm.make_def_binding (Config.get lthy function_internals) fname |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
134 |
val ((f, (_, f_defthm)), lthy') = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
135 |
Local_Theory.define |
63011 | 136 |
((fname, mixfix), ((def_binding, []), Term.subst_bound (fsum, f_def))) lthy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
137 |
in |
63011 | 138 |
(MutualPart {i = i, i' = i', fname = fname, fT = fT, cargTs = cargTs, |
139 |
f_def = f_def, f = SOME f, f_defthm = SOME f_defthm}, lthy') |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
140 |
end |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
141 |
|
63012 | 142 |
val Mutual {n, n', fsum_name, fsum_type, ST, RST, parts, fqgars, qglrs, ...} = mutual |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
143 |
val (parts', lthy') = fold_map def (parts ~~ fixes) lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
144 |
in |
63012 | 145 |
(Mutual {n = n, n' = n', fsum_name = fsum_name, fsum_type = fsum_type, ST = ST, |
146 |
RST = RST, parts = parts', fqgars = fqgars, qglrs = qglrs, fsum = SOME fsum}, lthy') |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
147 |
end |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
148 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
149 |
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
150 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
151 |
val oqnames = map fst pre_qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
152 |
val (qs, _) = Variable.variant_fixes oqnames ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
153 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
154 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
155 |
fun inst t = subst_bounds (rev qs, t) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
156 |
val gs = map inst pre_gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
157 |
val args = map inst pre_args |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
158 |
val rhs = inst pre_rhs |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
159 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
160 |
val cqs = map (Thm.cterm_of ctxt) qs |
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
161 |
val ags = map (Thm.assume o Thm.cterm_of ctxt) gs |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
162 |
|
36945 | 163 |
val import = fold Thm.forall_elim cqs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
164 |
#> fold Thm.elim_implies ags |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
19922
diff
changeset
|
165 |
|
59582 | 166 |
val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
167 |
#> fold_rev forall_intr_rename (oqnames ~~ cqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
168 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
169 |
F ctxt (f, qs, gs, args, rhs) import export |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
170 |
end |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
171 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
172 |
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs) |
45403 | 173 |
import (export : thm -> thm) sum_psimp_eq = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
174 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
175 |
val (MutualPart {f=SOME f, ...}) = get_part fname parts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
176 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
177 |
val psimp = import sum_psimp_eq |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
178 |
val (simp, restore_cond) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
179 |
case cprems_of psimp of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
180 |
[] => (psimp, I) |
36945 | 181 |
| [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
40317
1eac228c52b3
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents:
40076
diff
changeset
|
182 |
| _ => raise General.Fail "Too many conditions" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
183 |
|
60949 | 184 |
val simp_ctxt = fold Thm.declare_hyps (Thm.chyps_of simp) ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
185 |
in |
54566 | 186 |
Goal.prove simp_ctxt [] [] |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
187 |
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) |
45403 | 188 |
(fn _ => |
63170 | 189 |
Local_Defs.unfold0_tac ctxt all_orig_fdefs |
45403 | 190 |
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
191 |
THEN (simp_tac ctxt) 1) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
192 |
|> restore_cond |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
193 |
|> export |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
194 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
195 |
|
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
196 |
fun mk_applied_form ctxt caTs thm = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
197 |
let |
59582 | 198 |
val xs = |
199 |
map_index (fn (i, T) => |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
200 |
Thm.cterm_of ctxt |
59618 | 201 |
(Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
202 |
in |
36945 | 203 |
fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
204 |
|> Conv.fconv_rule (Thm.beta_conversion true) |
36945 | 205 |
|> fold_rev Thm.forall_intr xs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
206 |
|> Thm.forall_elim_vars 0 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
207 |
end |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
208 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
209 |
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
210 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
211 |
val newPs = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
212 |
map2 (fn Pname => fn MutualPart {cargTs, ...} => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
213 |
Free (Pname, cargTs ---> HOLogic.boolT)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
214 |
(mutual_induct_Pnames (length parts)) parts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
215 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
216 |
fun mk_P (MutualPart {cargTs, ...}) P = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
217 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
218 |
val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
219 |
val atup = foldr1 HOLogic.mk_prod avars |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
220 |
in |
39756
6c8e83d94536
consolidated tupled_lambda; moved to structure HOLogic
krauss
parents:
39276
diff
changeset
|
221 |
HOLogic.tupled_lambda atup (list_comb (P, avars)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
222 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
223 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
224 |
val Ps = map2 mk_P parts newPs |
55968 | 225 |
val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
226 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
227 |
val induct_inst = |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
228 |
Thm.forall_elim (Thm.cterm_of ctxt case_exp) induct |
55968 | 229 |
|> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
230 |
|> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
231 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
232 |
fun project rule (MutualPart {cargTs, i, ...}) k = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
233 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
234 |
val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *) |
55968 | 235 |
val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
236 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
237 |
(rule |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
238 |
|> Thm.forall_elim (Thm.cterm_of ctxt inj) |
55968 | 239 |
|> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt) |
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
240 |
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) (afs @ newPs), |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
241 |
k + length cargTs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
242 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
243 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
244 |
fst (fold_map (project induct_inst) parts 0) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
245 |
end |
20878
384c5bb713b2
mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents:
20851
diff
changeset
|
246 |
|
59651 | 247 |
fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) = |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
248 |
let |
59651 | 249 |
val [P, x] = |
67149 | 250 |
Variable.variant_frees ctxt [] [("P", \<^typ>\<open>bool\<close>), ("x", HOLogic.mk_tupleT Ts)] |
59651 | 251 |
|> map (Thm.cterm_of ctxt o Free); |
60321 | 252 |
val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x)); |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
253 |
|
59651 | 254 |
fun prep_subgoal_tac i = |
255 |
REPEAT (eresolve_tac ctxt |
|
256 |
@{thms Pair_inject Inl_inject [elim_format] Inr_inject [elim_format]} i) |
|
257 |
THEN REPEAT (eresolve_tac ctxt |
|
258 |
@{thms HOL.notE [OF Sum_Type.sum.distinct(1)] HOL.notE [OF Sum_Type.sum.distinct(2)]} i); |
|
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
259 |
in |
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
260 |
cases_rule |
59454 | 261 |
|> Thm.forall_elim P |
59651 | 262 |
|> Thm.forall_elim sumtree_inj |
263 |
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac) |
|
264 |
|> Thm.forall_intr x |
|
59454 | 265 |
|> Thm.forall_intr P |
70479 | 266 |
|> Thm.solve_constraints |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
267 |
end |
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
268 |
|
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
269 |
|
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
270 |
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, n, ST, ...}) proof = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
271 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
272 |
val result = inner_cont proof |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
273 |
val FunctionResult {G, R, cases=[cases_rule], psimps, simple_pinducts=[simple_pinduct], |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
274 |
termination, domintros, dom, pelims, ...} = result |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
275 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
276 |
val (all_f_defs, fs) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
277 |
map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
36945 | 278 |
(mk_applied_form lthy cargTs (Thm.symmetric f_def), f)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
279 |
parts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
280 |
|> split_list |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
281 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
282 |
val all_orig_fdefs = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
283 |
map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
284 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
285 |
fun mk_mpsimp fqgar sum_psimp = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
286 |
in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp |
22497
1fe951654cee
fixed problem with the construction of mutual simp rules
krauss
parents:
22323
diff
changeset
|
287 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
288 |
val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
289 |
val mpsimps = map2 mk_mpsimp fqgars psimps |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
290 |
val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
291 |
val mcases = map (mutual_cases_rule lthy cases_rule n ST) parts |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
292 |
val mtermination = full_simplify rew_simpset termination |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46909
diff
changeset
|
293 |
val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
294 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
295 |
in |
52384 | 296 |
FunctionResult { fs=fs, G=G, R=R, dom=dom, |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
297 |
psimps=mpsimps, simple_pinducts=minducts, |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
298 |
cases=mcases, pelims=pelims, termination=mtermination, |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41114
diff
changeset
|
299 |
domintros=mdomintros} |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
300 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
301 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
52384
diff
changeset
|
302 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
32765
diff
changeset
|
303 |
fun prepare_function_mutual config defname fixes eqss lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
304 |
let |
63012 | 305 |
val mutual as Mutual {fsum_name, fsum_type, qglrs, ...} = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
306 |
analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
307 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
308 |
val ((fsum, goalstate, cont), lthy') = |
63012 | 309 |
Function_Core.prepare_function config defname [((fsum_name, fsum_type), NoSyn)] qglrs lthy |
22166 | 310 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
311 |
val (mutual', lthy'') = define_projections fixes mutual fsum lthy' |
22166 | 312 |
|
60643 | 313 |
fun cont' ctxt = mk_partial_rules_mutual lthy'' (cont ctxt) mutual' |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
314 |
in |
53608
53bd62921c54
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents:
53607
diff
changeset
|
315 |
((goalstate, cont'), lthy'') |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
316 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
317 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff
changeset
|
318 |
end |