author | krauss |
Wed, 02 Aug 2006 18:33:46 +0200 | |
changeset 20285 | 23f5cd23c1e1 |
parent 19922 | 984ae977f7aa |
child 20344 | d02b43ea722e |
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 |
ID: $Id$ |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
4 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
5 |
A package for general recursive function definitions. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
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
|
7 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
signature FUNDEF_DATATYPE = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
sig |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
11 |
val pat_complete_tac: int -> tactic |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
12 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
13 |
val setup : theory -> theory |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
14 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
15 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
16 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
17 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
18 |
structure FundefDatatype : FUNDEF_DATATYPE = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
20 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19564
diff
changeset
|
21 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
22 |
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
|
23 |
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
|
24 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
25 |
fun inst_free var inst thm = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
26 |
forall_elim inst (forall_intr var thm) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
27 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
28 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
29 |
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
|
30 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
31 |
val [Pv, xv] = term_vars (prop_of thm) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
32 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
33 |
cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
34 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
35 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
36 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
37 |
fun invent_vars constr i = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
39 |
val Ts = binder_types (fastype_of constr) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
40 |
val j = i + length Ts |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
41 |
val is = i upto (j - 1) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
42 |
val avs = map2 mk_argvar is Ts |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
43 |
val pvs = map2 mk_patvar is Ts |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
44 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
45 |
(avs, pvs, j) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
46 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
47 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
48 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
49 |
fun filter_pats thy cons pvars [] = [] |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
50 |
| filter_pats thy cons pvars (([], thm) :: pts) = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
51 |
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
52 |
case pat of |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
53 |
Free _ => let val inst = list_comb (cons, pvars) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
54 |
in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
55 |
:: (filter_pats thy cons pvars pts) end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
56 |
| _ => if fst (strip_comb pat) = cons |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
57 |
then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
58 |
else filter_pats thy cons pvars pts |
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 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
61 |
fun inst_constrs_of thy (T as Type (name, _)) = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
62 |
map (fn (Cn,CT) => Envir.subst_TVars (Type.typ_match (Sign.tsig_of thy) (body_type CT, T) Vartab.empty) (Const (Cn, CT))) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
63 |
(the (DatatypePackage.get_datatype_constrs thy name)) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |
| inst_constrs_of thy _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
65 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
66 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
67 |
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
|
68 |
| 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
|
69 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
70 |
val (_, subps) = strip_comb pat |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
71 |
val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
72 |
val a_eqs = map assume eqs |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
73 |
val c_eq_pat = simplify (HOL_basic_ss addsimps a_eqs) c_assum |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
74 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
75 |
(subps @ pats, fold_rev implies_intr eqs |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
76 |
(implies_elim thm c_eq_pat)) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
77 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
78 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
79 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
80 |
exception COMPLETENESS |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
81 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
82 |
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
|
83 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
84 |
val (avars, pvars, newidx) = invent_vars cons idx |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
85 |
val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
86 |
val c_assum = assume c_hyp |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
87 |
val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
88 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
89 |
o_alg thy P newidx (avars @ vs) newpats |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
90 |
|> implies_intr c_hyp |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
91 |
|> fold_rev (forall_intr o cterm_of thy) avars |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
92 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
93 |
| constr_case _ _ _ _ _ _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
94 |
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
|
95 |
| 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
|
96 |
| 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
|
97 |
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
|
98 |
then o_alg thy P idx vs (map (fn (pv :: pats, thm) => |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
99 |
(pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
100 |
else (* Cons case *) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
101 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
102 |
val T = fastype_of v |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
103 |
val (tname, _) = dest_Type T |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
104 |
val {exhaustion=case_thm, ...} = DatatypePackage.the_datatype thy tname |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
105 |
val constrs = inst_constrs_of thy T |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
106 |
val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
107 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
108 |
inst_case_thm thy v P case_thm |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
109 |
|> fold (curry op COMP) c_cases |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
110 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
111 |
| o_alg _ _ _ _ _ = raise Match |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
112 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
113 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
114 |
fun prove_completeness thy x P qss pats = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
115 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
116 |
fun mk_assum qs pat = Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x,pat)), |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
117 |
HOLogic.mk_Trueprop P) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
118 |
|> fold_rev mk_forall qs |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
119 |
|> cterm_of thy |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
120 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
121 |
val hyps = map2 mk_assum qss pats |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
122 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
123 |
fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
124 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
125 |
val assums = map2 inst_hyps hyps qss |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
126 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
127 |
o_alg thy P 2 [x] (map2 (pair o single) pats assums) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
128 |
|> fold_rev implies_intr hyps |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
129 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
130 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
131 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
132 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
133 |
fun pat_complete_tac i thm = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
134 |
let |
19922 | 135 |
val thy = theory_of_thm thm |
136 |
||
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
137 |
val subgoal = nth (prems_of thm) (i - 1) |
19922 | 138 |
|
139 |
val ([P, x], subgf) = dest_all_all subgoal |
|
140 |
||
141 |
val assums = Logic.strip_imp_prems subgf |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
142 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
143 |
fun pat_of assum = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
144 |
let |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
145 |
val (qs, imp) = dest_all_all assum |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
146 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
147 |
case Logic.dest_implies imp of |
19922 | 148 |
(_ $ (_ $ _ $ pat), _) => (qs, pat) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
149 |
| _ => raise COMPLETENESS |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
150 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
151 |
|
19922 | 152 |
val (qss, pats) = split_list (map pat_of assums) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
153 |
|
19922 | 154 |
val complete_thm = prove_completeness thy x P qss pats |
155 |
|> forall_intr (cterm_of thy x) |
|
156 |
|> forall_intr (cterm_of thy P) |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
157 |
in |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
158 |
Seq.single (Drule.compose_single(complete_thm, i, thm)) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
159 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
160 |
handle COMPLETENESS => Seq.empty |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
161 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
162 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
163 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
164 |
val setup = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
165 |
Method.add_methods [("pat_completeness", Method.no_args (Method.SIMPLE_METHOD (pat_complete_tac 1)), "Completeness prover for datatype patterns")] |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
166 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
167 |
end |