33083
|
1 |
(* Title: HOL/Tools/Function/fundef_datatype.ML
|
|
2 |
Author: Alexander Krauss, TU Muenchen
|
|
3 |
|
|
4 |
Method "pat_completeness" to prove completeness of datatype patterns.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature PAT_COMPLETENESS =
|
|
8 |
sig
|
|
9 |
val pat_completeness_tac: Proof.context -> int -> tactic
|
|
10 |
val pat_completeness: Proof.context -> Proof.method
|
|
11 |
val prove_completeness : theory -> term list -> term -> term list list ->
|
|
12 |
term list list -> thm
|
|
13 |
|
|
14 |
val setup : theory -> theory
|
|
15 |
end
|
|
16 |
|
|
17 |
structure Pat_Completeness : PAT_COMPLETENESS =
|
|
18 |
struct
|
|
19 |
|
|
20 |
open FundefLib
|
|
21 |
open FundefCommon
|
|
22 |
|
|
23 |
|
|
24 |
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T)
|
|
25 |
fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T)
|
|
26 |
|
|
27 |
fun inst_free var inst = forall_elim inst o forall_intr var
|
|
28 |
|
|
29 |
fun inst_case_thm thy x P thm =
|
|
30 |
let val [Pv, xv] = Term.add_vars (prop_of thm) []
|
|
31 |
in
|
|
32 |
thm |> cterm_instantiate (map (pairself (cterm_of thy))
|
|
33 |
[(Var xv, x), (Var Pv, P)])
|
|
34 |
end
|
|
35 |
|
|
36 |
fun invent_vars constr i =
|
|
37 |
let
|
|
38 |
val Ts = binder_types (fastype_of constr)
|
|
39 |
val j = i + length Ts
|
|
40 |
val is = i upto (j - 1)
|
|
41 |
val avs = map2 mk_argvar is Ts
|
|
42 |
val pvs = map2 mk_patvar is Ts
|
|
43 |
in
|
|
44 |
(avs, pvs, j)
|
|
45 |
end
|
|
46 |
|
|
47 |
fun filter_pats thy cons pvars [] = []
|
|
48 |
| filter_pats thy cons pvars (([], thm) :: pts) = raise Match
|
|
49 |
| filter_pats thy cons pvars (((pat as Free _) :: pats, thm) :: pts) =
|
|
50 |
let val inst = list_comb (cons, pvars)
|
|
51 |
in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm)
|
|
52 |
:: (filter_pats thy cons pvars pts)
|
|
53 |
end
|
|
54 |
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) =
|
|
55 |
if fst (strip_comb pat) = cons
|
|
56 |
then (pat :: pats, thm) :: (filter_pats thy cons pvars pts)
|
|
57 |
else filter_pats thy cons pvars pts
|
|
58 |
|
|
59 |
|
|
60 |
fun inst_constrs_of thy (T as Type (name, _)) =
|
|
61 |
map (fn (Cn,CT) =>
|
|
62 |
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT)))
|
|
63 |
(the (Datatype.get_constrs thy name))
|
|
64 |
| inst_constrs_of thy _ = raise Match
|
|
65 |
|
|
66 |
|
|
67 |
fun transform_pat thy avars c_assum ([] , thm) = raise Match
|
|
68 |
| transform_pat thy avars c_assum (pat :: pats, thm) =
|
|
69 |
let
|
|
70 |
val (_, subps) = strip_comb pat
|
|
71 |
val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps)
|
|
72 |
val c_eq_pat = simplify (HOL_basic_ss addsimps (map assume eqs)) c_assum
|
|
73 |
in
|
|
74 |
(subps @ pats,
|
|
75 |
fold_rev implies_intr eqs (implies_elim thm c_eq_pat))
|
|
76 |
end
|
|
77 |
|
|
78 |
|
|
79 |
exception COMPLETENESS
|
|
80 |
|
|
81 |
fun constr_case thy P idx (v :: vs) pats cons =
|
|
82 |
let
|
|
83 |
val (avars, pvars, newidx) = invent_vars cons idx
|
|
84 |
val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars))))
|
|
85 |
val c_assum = assume c_hyp
|
|
86 |
val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats)
|
|
87 |
in
|
|
88 |
o_alg thy P newidx (avars @ vs) newpats
|
|
89 |
|> implies_intr c_hyp
|
|
90 |
|> fold_rev (forall_intr o cterm_of thy) avars
|
|
91 |
end
|
|
92 |
| constr_case _ _ _ _ _ _ = raise Match
|
|
93 |
and o_alg thy P idx [] (([], Pthm) :: _) = Pthm
|
|
94 |
| o_alg thy P idx (v :: vs) [] = raise COMPLETENESS
|
|
95 |
| o_alg thy P idx (v :: vs) pts =
|
|
96 |
if forall (is_Free o hd o fst) pts (* Var case *)
|
|
97 |
then o_alg thy P idx vs
|
|
98 |
(map (fn (pv :: pats, thm) =>
|
|
99 |
(pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts)
|
|
100 |
else (* Cons case *)
|
|
101 |
let
|
|
102 |
val T = fastype_of v
|
|
103 |
val (tname, _) = dest_Type T
|
|
104 |
val {exhaust=case_thm, ...} = Datatype.the_info thy tname
|
|
105 |
val constrs = inst_constrs_of thy T
|
|
106 |
val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs
|
|
107 |
in
|
|
108 |
inst_case_thm thy v P case_thm
|
|
109 |
|> fold (curry op COMP) c_cases
|
|
110 |
end
|
|
111 |
| o_alg _ _ _ _ _ = raise Match
|
|
112 |
|
|
113 |
fun prove_completeness thy xs P qss patss =
|
|
114 |
let
|
|
115 |
fun mk_assum qs pats =
|
|
116 |
HOLogic.mk_Trueprop P
|
|
117 |
|> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
|
|
118 |
|> fold_rev Logic.all qs
|
|
119 |
|> cterm_of thy
|
|
120 |
|
|
121 |
val hyps = map2 mk_assum qss patss
|
|
122 |
fun inst_hyps hyp qs = fold (forall_elim o cterm_of thy) qs (assume hyp)
|
|
123 |
val assums = map2 inst_hyps hyps qss
|
|
124 |
in
|
|
125 |
o_alg thy P 2 xs (patss ~~ assums)
|
|
126 |
|> fold_rev implies_intr hyps
|
|
127 |
end
|
|
128 |
|
|
129 |
fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
|
|
130 |
let
|
|
131 |
val thy = ProofContext.theory_of ctxt
|
|
132 |
val (vs, subgf) = dest_all_all subgoal
|
|
133 |
val (cases, _ $ thesis) = Logic.strip_horn subgf
|
|
134 |
handle Bind => raise COMPLETENESS
|
|
135 |
|
|
136 |
fun pat_of assum =
|
|
137 |
let
|
|
138 |
val (qs, imp) = dest_all_all assum
|
|
139 |
val prems = Logic.strip_imp_prems imp
|
|
140 |
in
|
|
141 |
(qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems)
|
|
142 |
end
|
|
143 |
|
|
144 |
val (qss, x_pats) = split_list (map pat_of cases)
|
|
145 |
val xs = map fst (hd x_pats)
|
|
146 |
handle Empty => raise COMPLETENESS
|
|
147 |
|
|
148 |
val patss = map (map snd) x_pats
|
|
149 |
val complete_thm = prove_completeness thy xs thesis qss patss
|
|
150 |
|> fold_rev (forall_intr o cterm_of thy) vs
|
|
151 |
in
|
|
152 |
PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
|
|
153 |
end
|
|
154 |
handle COMPLETENESS => no_tac)
|
|
155 |
|
|
156 |
|
|
157 |
val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
|
|
158 |
|
|
159 |
val setup =
|
|
160 |
Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
|
|
161 |
"Completeness prover for datatype patterns"
|
|
162 |
|
|
163 |
end
|