author | wenzelm |
Mon, 05 Jan 2009 14:29:26 +0100 | |
changeset 29351 | 59250869ced5 |
parent 29329 | e02b3a32f34f |
child 29382 | 9f6e2658a868 |
permissions | -rw-r--r-- |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/fundef_datatype.ML |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
|
20344 | 4 |
A package for general recursive function definitions. |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
5 |
A tactic to prove completeness of datatype patterns. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
7 |
|
20344 | 8 |
signature FUNDEF_DATATYPE = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
sig |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
10 |
val pat_complete_tac: Proof.context -> int -> tactic |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
11 |
val prove_completeness : theory -> term list -> term -> term list list -> term list list -> thm |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
12 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
13 |
val pat_completeness : Proof.context -> method |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
14 |
val setup : theory -> theory |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
15 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
17 |
structure FundefDatatype : FUNDEF_DATATYPE = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
18 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
|
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20999
diff
changeset
|
20 |
open FundefLib |
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20999
diff
changeset
|
21 |
open FundefCommon |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
22 |
|
23189 | 23 |
|
24 |
fun check_pats ctxt geq = |
|
25 |
let |
|
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
26 |
fun err str = error (cat_lines ["Malformed definition:", |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
27 |
str ^ " not allowed in sequential mode.", |
24920 | 28 |
Syntax.string_of_term ctxt geq]) |
23189 | 29 |
val thy = ProofContext.theory_of ctxt |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
30 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
31 |
fun check_constr_pattern (Bound _) = () |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
32 |
| check_constr_pattern t = |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
33 |
let |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
34 |
val (hd, args) = strip_comb t |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
35 |
in |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
36 |
(((case DatatypePackage.datatype_of_constr thy (fst (dest_Const hd)) of |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
37 |
SOME _ => () |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
38 |
| NONE => err "Non-constructor pattern") |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
39 |
handle TERM ("dest_Const", _) => err "Non-constructor patterns"); |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
40 |
map check_constr_pattern args; |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
41 |
()) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
42 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
43 |
|
24170 | 44 |
val (fname, qs, gs, args, rhs) = split_def ctxt geq |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
45 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
46 |
val _ = if not (null gs) then err "Conditional equations" else () |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
47 |
val _ = map check_constr_pattern args |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
48 |
|
23189 | 49 |
(* just count occurrences to check linearity *) |
24170 | 50 |
val _ = if fold (fold_aterms (fn Bound _ => curry (op +) 1 | _ => I)) args 0 > length qs |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
51 |
then err "Nonlinear patterns" else () |
23189 | 52 |
in |
53 |
() |
|
54 |
end |
|
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
55 |
|
23189 | 56 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
57 |
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
58 |
fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
59 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
60 |
fun inst_free var inst thm = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
61 |
forall_elim inst (forall_intr var thm) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
62 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
63 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |
fun inst_case_thm thy x P thm = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
65 |
let |
29329 | 66 |
val [Pv, xv] = Term.add_vars (prop_of thm) [] |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
67 |
in |
29329 | 68 |
cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x), |
69 |
(cterm_of thy (Var Pv), cterm_of thy P)] thm |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
70 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
71 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
72 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
73 |
fun invent_vars constr i = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
74 |
let |
20344 | 75 |
val Ts = binder_types (fastype_of constr) |
76 |
val j = i + length Ts |
|
77 |
val is = i upto (j - 1) |
|
78 |
val avs = map2 mk_argvar is Ts |
|
79 |
val pvs = map2 mk_patvar is Ts |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
80 |
in |
20344 | 81 |
(avs, pvs, j) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
82 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
83 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
84 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
85 |
fun filter_pats thy cons pvars [] = [] |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
86 |
| filter_pats thy cons pvars (([], thm) :: pts) = raise Match |
20344 | 87 |
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
88 |
case pat of |
20344 | 89 |
Free _ => let val inst = list_comb (cons, pvars) |
90 |
in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm) |
|
91 |
:: (filter_pats thy cons pvars pts) end |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
92 |
| _ => if fst (strip_comb pat) = cons |
20344 | 93 |
then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) |
94 |
else filter_pats thy cons pvars pts |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
95 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
96 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
97 |
fun inst_constrs_of thy (T as Type (name, _)) = |
20344 | 98 |
map (fn (Cn,CT) => Envir.subst_TVars (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) |
99 |
(the (DatatypePackage.get_datatype_constrs thy name)) |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
100 |
| inst_constrs_of thy _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
101 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
102 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
103 |
fun transform_pat thy avars c_assum ([] , thm) = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
104 |
| transform_pat thy avars c_assum (pat :: pats, thm) = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
105 |
let |
20344 | 106 |
val (_, subps) = strip_comb pat |
107 |
val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) |
|
108 |
val a_eqs = map assume eqs |
|
109 |
val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
110 |
in |
20344 | 111 |
(subps @ pats, fold_rev implies_intr eqs |
112 |
(implies_elim thm c_eq_pat)) |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
113 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
114 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
115 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
116 |
exception COMPLETENESS |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
117 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
118 |
fun constr_case thy P idx (v :: vs) pats cons = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
119 |
let |
20344 | 120 |
val (avars, pvars, newidx) = invent_vars cons idx |
121 |
val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) |
|
122 |
val c_assum = assume c_hyp |
|
123 |
val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats) |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
124 |
in |
20344 | 125 |
o_alg thy P newidx (avars @ vs) newpats |
126 |
|> implies_intr c_hyp |
|
127 |
|> fold_rev (forall_intr o cterm_of thy) avars |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
128 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
129 |
| constr_case _ _ _ _ _ _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
130 |
and o_alg thy P idx [] (([], Pthm) :: _) = Pthm |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
131 |
| o_alg thy P idx (v :: vs) [] = raise COMPLETENESS |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
132 |
| o_alg thy P idx (v :: vs) pts = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
133 |
if forall (is_Free o hd o fst) pts (* Var case *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
134 |
then o_alg thy P idx vs (map (fn (pv :: pats, thm) => |
20344 | 135 |
(pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
136 |
else (* Cons case *) |
20344 | 137 |
let |
138 |
val T = fastype_of v |
|
139 |
val (tname, _) = dest_Type T |
|
140 |
val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname |
|
141 |
val constrs = inst_constrs_of thy T |
|
142 |
val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs |
|
143 |
in |
|
144 |
inst_case_thm thy v P case_thm |
|
145 |
|> fold (curry op COMP) c_cases |
|
146 |
end |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
147 |
| o_alg _ _ _ _ _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
148 |
|
20344 | 149 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
150 |
fun prove_completeness thy xs P qss patss = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
151 |
let |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
152 |
fun mk_assum qs pats = |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
153 |
HOLogic.mk_Trueprop P |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
154 |
|> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) |
27330 | 155 |
|> fold_rev Logic.all qs |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
156 |
|> cterm_of thy |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
157 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
158 |
val hyps = map2 mk_assum qss patss |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
159 |
|
20344 | 160 |
fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
161 |
|
20344 | 162 |
val assums = map2 inst_hyps hyps qss |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
163 |
in |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
164 |
o_alg thy P 2 xs (patss ~~ assums) |
20344 | 165 |
|> fold_rev implies_intr hyps |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
166 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
167 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
168 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
169 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
170 |
fun pat_complete_tac ctxt = SUBGOAL (fn (subgoal, i) => |
20344 | 171 |
let |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
172 |
val thy = ProofContext.theory_of ctxt |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
173 |
val (vs, subgf) = dest_all_all subgoal |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
174 |
val (cases, _ $ thesis) = Logic.strip_horn subgf |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
175 |
handle Bind => raise COMPLETENESS |
19922 | 176 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
177 |
fun pat_of assum = |
20344 | 178 |
let |
179 |
val (qs, imp) = dest_all_all assum |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
180 |
val prems = Logic.strip_imp_prems imp |
20344 | 181 |
in |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
182 |
(qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) |
20344 | 183 |
end |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
184 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
185 |
val (qss, x_pats) = split_list (map pat_of cases) |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
186 |
val xs = map fst (hd x_pats) |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
187 |
handle Empty => raise COMPLETENESS |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
188 |
|
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
189 |
val patss = map (map snd) x_pats |
20344 | 190 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
191 |
val complete_thm = prove_completeness thy xs thesis qss patss |
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
192 |
|> fold_rev (forall_intr o cterm_of thy) vs |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
193 |
in |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
194 |
PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st)) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
195 |
end |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
196 |
handle COMPLETENESS => no_tac) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
197 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
198 |
|
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
199 |
fun pat_completeness ctxt = Method.SIMPLE_METHOD' (pat_complete_tac ctxt) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
200 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
201 |
val by_pat_completeness_simp = |
29351
59250869ced5
parallelize some internal proofs via Proof.future_terminal_proof;
wenzelm
parents:
29329
diff
changeset
|
202 |
Proof.future_terminal_proof |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
203 |
(Method.Basic (pat_completeness, Position.none), |
22899
5ea718c68123
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
krauss
parents:
22733
diff
changeset
|
204 |
SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none)))) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
205 |
|
28287
c86fa4e0aedb
termination prover for "fun" can be configured using context data.
krauss
parents:
27330
diff
changeset
|
206 |
fun termination_by method = |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22498
diff
changeset
|
207 |
FundefPackage.setup_termination_proof NONE |
29351
59250869ced5
parallelize some internal proofs via Proof.future_terminal_proof;
wenzelm
parents:
29329
diff
changeset
|
208 |
#> Proof.future_terminal_proof |
28287
c86fa4e0aedb
termination prover for "fun" can be configured using context data.
krauss
parents:
27330
diff
changeset
|
209 |
(Method.Basic (method, Position.none), NONE) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
210 |
|
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
211 |
fun mk_catchall fixes arities = |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
212 |
let |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
213 |
fun mk_eqn ((fname, fT), _) = |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
214 |
let |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
215 |
val n = the (Symtab.lookup arities fname) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
216 |
val (argTs, rT) = chop n (binder_types fT) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
217 |
|> apsnd (fn Ts => Ts ---> body_type fT) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
218 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
219 |
val qs = map Free (Name.invent_list [] "a" n ~~ argTs) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
220 |
in |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
221 |
HOLogic.mk_eq(list_comb (Free (fname, fT), qs), |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
222 |
Const ("HOL.undefined", rT)) |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
223 |
|> HOLogic.mk_Trueprop |
27330 | 224 |
|> fold_rev Logic.all qs |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
225 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
226 |
in |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
227 |
map mk_eqn fixes |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
228 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
229 |
|
24170 | 230 |
fun add_catchall ctxt fixes spec = |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
231 |
let |
24170 | 232 |
val catchalls = mk_catchall fixes (mk_arities (map (split_def ctxt) (map snd spec))) |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
233 |
in |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
234 |
spec @ map (pair true) catchalls |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
235 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
236 |
|
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
237 |
fun warn_if_redundant ctxt origs tss = |
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
238 |
let |
24920 | 239 |
fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t) |
24466 | 240 |
|
241 |
val (tss', _) = chop (length origs) tss |
|
242 |
fun check ((_, t), []) = (Output.warning (msg t); []) |
|
243 |
| check ((_, t), s) = s |
|
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
244 |
in |
24466 | 245 |
(map check (origs ~~ tss'); tss) |
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
246 |
end |
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
247 |
|
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
248 |
|
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
249 |
fun sequential_preproc (config as FundefConfig {sequential, ...}) flags ctxt fixes spec = |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
250 |
let |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
251 |
val enabled = sequential orelse exists I flags |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
252 |
in |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
253 |
if enabled then |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
254 |
let |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
255 |
val flags' = if sequential then map (K true) flags else flags |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
256 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
257 |
val (nas, eqss) = split_list spec |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
258 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
259 |
val eqs = map the_single eqss |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
260 |
|
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
261 |
val feqs = eqs |
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
262 |
|> tap (check_defs ctxt fixes) (* Standard checks *) |
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
263 |
|> tap (map (check_pats ctxt)) (* More checks for sequential mode *) |
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
264 |
|> curry op ~~ flags' |
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
265 |
|
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
266 |
val compleqs = add_catchall ctxt fixes feqs (* Completion *) |
24356
65fd09a7243f
issue a warning, when encountering redundant equations (covered by prece3ding clauses)
krauss
parents:
24170
diff
changeset
|
267 |
|
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
268 |
val spliteqs = warn_if_redundant ctxt feqs |
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
269 |
(FundefSplit.split_some_equations ctxt compleqs) |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
270 |
|
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
271 |
fun restore_spec thms = |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
272 |
nas ~~ Library.take (length nas, Library.unflat spliteqs thms) |
23819 | 273 |
|
274 |
val spliteqs' = flat (Library.take (length nas, spliteqs)) |
|
275 |
val fnames = map (fst o fst) fixes |
|
276 |
val indices = map (fn eq => find_index (curry op = (fname_of eq)) fnames) spliteqs' |
|
277 |
||
278 |
fun sort xs = partition_list (fn i => fn (j,_) => i = j) 0 (length fnames - 1) (indices ~~ xs) |
|
279 |
|> map (map snd) |
|
280 |
||
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
281 |
|
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
282 |
val nas' = nas @ replicate (length spliteqs - length nas) ("",[]) |
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
283 |
|
25361
1aa441e48496
function package: using the names of the equations as case names turned out to be impractical => disabled
krauss
parents:
25289
diff
changeset
|
284 |
(* using theorem names for case name currently disabled *) |
1aa441e48496
function package: using the names of the equations as case names turned out to be impractical => disabled
krauss
parents:
25289
diff
changeset
|
285 |
val case_names = map_index (fn (i, ((n, _), es)) => mk_case_names i "" (length es)) |
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
286 |
(nas' ~~ spliteqs) |
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
287 |
|> flat |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
288 |
in |
25222
78943ac46f6d
fun/function: generate case names for induction rules
krauss
parents:
25169
diff
changeset
|
289 |
(flat spliteqs, restore_spec, sort, case_names) |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
290 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
291 |
else |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
292 |
FundefCommon.empty_preproc check_defs config flags ctxt fixes spec |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
293 |
end |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
294 |
|
20344 | 295 |
val setup = |
27271
ba2a00d35df1
generalized induct_scheme method to prove conditional induction schemes.
krauss
parents:
26989
diff
changeset
|
296 |
Method.add_methods [("pat_completeness", Method.ctxt_args pat_completeness, |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
297 |
"Completeness prover for datatype patterns")] |
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
298 |
#> Context.theory_map (FundefCommon.set_preproc sequential_preproc) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
299 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
300 |
|
28524 | 301 |
val fun_config = FundefConfig { sequential=true, default="%x. undefined" (*FIXME dynamic scoping*), |
26989 | 302 |
domintros=false, tailrec=false } |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
303 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
304 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
305 |
local structure P = OuterParse and K = OuterKeyword in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
306 |
|
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
307 |
fun fun_cmd config fixes statements flags lthy = |
26171
5426a823455c
more precise handling of "group" for termination;
wenzelm
parents:
26129
diff
changeset
|
308 |
let val group = serial_string () in |
21211
5370cfbf3070
Preparations for making "lexicographic_order" part of "fun"
krauss
parents:
21051
diff
changeset
|
309 |
lthy |
26171
5426a823455c
more precise handling of "group" for termination;
wenzelm
parents:
26129
diff
changeset
|
310 |
|> LocalTheory.set_group group |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
311 |
|> FundefPackage.add_fundef fixes statements config flags |
22733
0b14bb35be90
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
krauss
parents:
22498
diff
changeset
|
312 |
|> by_pat_completeness_simp |
26270 | 313 |
|> LocalTheory.restore |
26171
5426a823455c
more precise handling of "group" for termination;
wenzelm
parents:
26129
diff
changeset
|
314 |
|> LocalTheory.set_group group |
28287
c86fa4e0aedb
termination prover for "fun" can be configured using context data.
krauss
parents:
27330
diff
changeset
|
315 |
|> termination_by (FundefCommon.get_termination_prover (Context.Proof lthy)) |
26171
5426a823455c
more precise handling of "group" for termination;
wenzelm
parents:
26129
diff
changeset
|
316 |
end; |
21211
5370cfbf3070
Preparations for making "lexicographic_order" part of "fun"
krauss
parents:
21051
diff
changeset
|
317 |
|
24867 | 318 |
val _ = |
26989 | 319 |
OuterSyntax.local_theory "fun" "define general recursive functions (short version)" K.thy_decl |
23203
a5026e73cfcf
"function (sequential)" and "fun" now handle incomplete patterns silently by adding "undefined" cases.
krauss
parents:
23189
diff
changeset
|
320 |
(fundef_parser fun_config |
26989 | 321 |
>> (fn ((config, fixes), (flags, statements)) => fun_cmd config fixes statements flags)); |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
322 |
|
20344 | 323 |
end |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
324 |
|
20875 | 325 |
end |