author | wenzelm |
Thu, 27 Jun 2013 17:06:22 +0200 | |
changeset 52467 | 24c6ddb48cb8 |
parent 51717 | 9e7d1c139569 |
child 54406 | a2d18fea844a |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: HOL/Tools/Function/pat_completeness.ML |
33083 | 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 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
10 |
val prove_completeness : Proof.context -> term list -> term -> term list list -> |
33083 | 11 |
term list list -> thm |
12 |
end |
|
13 |
||
14 |
structure Pat_Completeness : PAT_COMPLETENESS = |
|
15 |
struct |
|
16 |
||
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33083
diff
changeset
|
17 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33083
diff
changeset
|
18 |
open Function_Common |
33083 | 19 |
|
20 |
||
21 |
fun mk_argvar i T = Free ("_av" ^ (string_of_int i), T) |
|
22 |
fun mk_patvar i T = Free ("_pv" ^ (string_of_int i), T) |
|
23 |
||
36945 | 24 |
fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var |
33083 | 25 |
|
26 |
fun inst_case_thm thy x P thm = |
|
27 |
let val [Pv, xv] = Term.add_vars (prop_of thm) [] |
|
28 |
in |
|
29 |
thm |> cterm_instantiate (map (pairself (cterm_of thy)) |
|
30 |
[(Var xv, x), (Var Pv, P)]) |
|
31 |
end |
|
32 |
||
33 |
fun invent_vars constr i = |
|
34 |
let |
|
35 |
val Ts = binder_types (fastype_of constr) |
|
36 |
val j = i + length Ts |
|
37 |
val is = i upto (j - 1) |
|
38 |
val avs = map2 mk_argvar is Ts |
|
39 |
val pvs = map2 mk_patvar is Ts |
|
40 |
in |
|
41 |
(avs, pvs, j) |
|
42 |
end |
|
43 |
||
44 |
fun filter_pats thy cons pvars [] = [] |
|
45 |
| filter_pats thy cons pvars (([], thm) :: pts) = raise Match |
|
46 |
| filter_pats thy cons pvars (((pat as Free _) :: pats, thm) :: pts) = |
|
47 |
let val inst = list_comb (cons, pvars) |
|
48 |
in (inst :: pats, inst_free (cterm_of thy pat) (cterm_of thy inst) thm) |
|
49 |
:: (filter_pats thy cons pvars pts) |
|
50 |
end |
|
51 |
| filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = |
|
52 |
if fst (strip_comb pat) = cons |
|
53 |
then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) |
|
54 |
else filter_pats thy cons pvars pts |
|
55 |
||
56 |
||
57 |
fun inst_constrs_of thy (T as Type (name, _)) = |
|
58 |
map (fn (Cn,CT) => |
|
59 |
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) |
|
60 |
(the (Datatype.get_constrs thy name)) |
|
61 |
| inst_constrs_of thy _ = raise Match |
|
62 |
||
63 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
64 |
fun transform_pat _ avars c_assum ([] , thm) = raise Match |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
65 |
| transform_pat ctxt avars c_assum (pat :: pats, thm) = |
33083 | 66 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
67 |
val thy = Proof_Context.theory_of ctxt |
33083 | 68 |
val (_, subps) = strip_comb pat |
69 |
val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
70 |
val c_eq_pat = simplify (put_simpset HOL_basic_ss ctxt addsimps (map Thm.assume eqs)) c_assum |
33083 | 71 |
in |
72 |
(subps @ pats, |
|
36945 | 73 |
fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat)) |
33083 | 74 |
end |
75 |
||
76 |
||
77 |
exception COMPLETENESS |
|
78 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
79 |
fun constr_case ctxt P idx (v :: vs) pats cons = |
33083 | 80 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
81 |
val thy = Proof_Context.theory_of ctxt |
33083 | 82 |
val (avars, pvars, newidx) = invent_vars cons idx |
83 |
val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) |
|
36945 | 84 |
val c_assum = Thm.assume c_hyp |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
85 |
val newpats = map (transform_pat ctxt avars c_assum) (filter_pats thy cons pvars pats) |
33083 | 86 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
87 |
o_alg ctxt P newidx (avars @ vs) newpats |
36945 | 88 |
|> Thm.implies_intr c_hyp |
89 |
|> fold_rev (Thm.forall_intr o cterm_of thy) avars |
|
33083 | 90 |
end |
91 |
| constr_case _ _ _ _ _ _ = raise Match |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
92 |
and o_alg _ P idx [] (([], Pthm) :: _) = Pthm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
93 |
| o_alg _ P idx (v :: vs) [] = raise COMPLETENESS |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
94 |
| o_alg ctxt P idx (v :: vs) pts = |
33083 | 95 |
if forall (is_Free o hd o fst) pts (* Var case *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
96 |
then o_alg ctxt P idx vs |
33083 | 97 |
(map (fn (pv :: pats, thm) => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
98 |
(pats, refl RS |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
99 |
(inst_free (cterm_of (Proof_Context.theory_of ctxt) pv) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
100 |
(cterm_of (Proof_Context.theory_of ctxt) v) thm))) pts) |
33083 | 101 |
else (* Cons case *) |
102 |
let |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
103 |
val thy = Proof_Context.theory_of ctxt |
33083 | 104 |
val T = fastype_of v |
105 |
val (tname, _) = dest_Type T |
|
106 |
val {exhaust=case_thm, ...} = Datatype.the_info thy tname |
|
107 |
val constrs = inst_constrs_of thy T |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
108 |
val c_cases = map (constr_case ctxt P idx (v :: vs) pts) constrs |
33083 | 109 |
in |
110 |
inst_case_thm thy v P case_thm |
|
111 |
|> fold (curry op COMP) c_cases |
|
112 |
end |
|
113 |
| o_alg _ _ _ _ _ = raise Match |
|
114 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
115 |
fun prove_completeness ctxt xs P qss patss = |
33083 | 116 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
117 |
val thy = Proof_Context.theory_of ctxt |
33083 | 118 |
fun mk_assum qs pats = |
119 |
HOLogic.mk_Trueprop P |
|
120 |
|> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) |
|
121 |
|> fold_rev Logic.all qs |
|
122 |
|> cterm_of thy |
|
123 |
||
124 |
val hyps = map2 mk_assum qss patss |
|
36945 | 125 |
fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp) |
33083 | 126 |
val assums = map2 inst_hyps hyps qss |
127 |
in |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
128 |
o_alg ctxt P 2 xs (patss ~~ assums) |
36945 | 129 |
|> fold_rev Thm.implies_intr hyps |
33083 | 130 |
end |
131 |
||
132 |
fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => |
|
133 |
let |
|
42361 | 134 |
val thy = Proof_Context.theory_of ctxt |
33083 | 135 |
val (vs, subgf) = dest_all_all subgoal |
136 |
val (cases, _ $ thesis) = Logic.strip_horn subgf |
|
137 |
handle Bind => raise COMPLETENESS |
|
138 |
||
139 |
fun pat_of assum = |
|
140 |
let |
|
141 |
val (qs, imp) = dest_all_all assum |
|
142 |
val prems = Logic.strip_imp_prems imp |
|
143 |
in |
|
144 |
(qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) |
|
145 |
end |
|
146 |
||
147 |
val (qss, x_pats) = split_list (map pat_of cases) |
|
148 |
val xs = map fst (hd x_pats) |
|
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
42361
diff
changeset
|
149 |
handle List.Empty => raise COMPLETENESS |
33083 | 150 |
|
151 |
val patss = map (map snd) x_pats |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
47432
diff
changeset
|
152 |
val complete_thm = prove_completeness ctxt xs thesis qss patss |
36945 | 153 |
|> fold_rev (Thm.forall_intr o cterm_of thy) vs |
33083 | 154 |
in |
52467 | 155 |
PRIMITIVE (fn st => Drule.compose (complete_thm, i, st)) |
33083 | 156 |
end |
157 |
handle COMPLETENESS => no_tac) |
|
158 |
||
159 |
end |