author  wenzelm 
Thu, 12 Apr 2012 18:39:19 +0200  
changeset 47432  e1576d13e933 
parent 47060  e2741ec9ae36 
child 51717  9e7d1c139569 
permissions  rwrr 
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 

10 
val prove_completeness : theory > term list > term > term list list > 

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 

64 
fun transform_pat thy avars c_assum ([] , thm) = raise Match 

65 
 transform_pat thy avars c_assum (pat :: pats, thm) = 

66 
let 

67 
val (_, subps) = strip_comb pat 

68 
val eqs = map (cterm_of thy o HOLogic.mk_Trueprop o HOLogic.mk_eq) (avars ~~ subps) 

36945  69 
val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum 
33083  70 
in 
71 
(subps @ pats, 

36945  72 
fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat)) 
33083  73 
end 
74 

75 

76 
exception COMPLETENESS 

77 

78 
fun constr_case thy P idx (v :: vs) pats cons = 

79 
let 

80 
val (avars, pvars, newidx) = invent_vars cons idx 

81 
val c_hyp = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (v, list_comb (cons, avars)))) 

36945  82 
val c_assum = Thm.assume c_hyp 
33083  83 
val newpats = map (transform_pat thy avars c_assum) (filter_pats thy cons pvars pats) 
84 
in 

85 
o_alg thy P newidx (avars @ vs) newpats 

36945  86 
> Thm.implies_intr c_hyp 
87 
> fold_rev (Thm.forall_intr o cterm_of thy) avars 

33083  88 
end 
89 
 constr_case _ _ _ _ _ _ = raise Match 

90 
and o_alg thy P idx [] (([], Pthm) :: _) = Pthm 

91 
 o_alg thy P idx (v :: vs) [] = raise COMPLETENESS 

92 
 o_alg thy P idx (v :: vs) pts = 

93 
if forall (is_Free o hd o fst) pts (* Var case *) 

94 
then o_alg thy P idx vs 

95 
(map (fn (pv :: pats, thm) => 

96 
(pats, refl RS (inst_free (cterm_of thy pv) (cterm_of thy v) thm))) pts) 

97 
else (* Cons case *) 

98 
let 

99 
val T = fastype_of v 

100 
val (tname, _) = dest_Type T 

101 
val {exhaust=case_thm, ...} = Datatype.the_info thy tname 

102 
val constrs = inst_constrs_of thy T 

103 
val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs 

104 
in 

105 
inst_case_thm thy v P case_thm 

106 
> fold (curry op COMP) c_cases 

107 
end 

108 
 o_alg _ _ _ _ _ = raise Match 

109 

110 
fun prove_completeness thy xs P qss patss = 

111 
let 

112 
fun mk_assum qs pats = 

113 
HOLogic.mk_Trueprop P 

114 
> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats) 

115 
> fold_rev Logic.all qs 

116 
> cterm_of thy 

117 

118 
val hyps = map2 mk_assum qss patss 

36945  119 
fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp) 
33083  120 
val assums = map2 inst_hyps hyps qss 
121 
in 

122 
o_alg thy P 2 xs (patss ~~ assums) 

36945  123 
> fold_rev Thm.implies_intr hyps 
33083  124 
end 
125 

126 
fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) => 

127 
let 

42361  128 
val thy = Proof_Context.theory_of ctxt 
33083  129 
val (vs, subgf) = dest_all_all subgoal 
130 
val (cases, _ $ thesis) = Logic.strip_horn subgf 

131 
handle Bind => raise COMPLETENESS 

132 

133 
fun pat_of assum = 

134 
let 

135 
val (qs, imp) = dest_all_all assum 

136 
val prems = Logic.strip_imp_prems imp 

137 
in 

138 
(qs, map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems) 

139 
end 

140 

141 
val (qss, x_pats) = split_list (map pat_of cases) 

142 
val xs = map fst (hd x_pats) 

47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
42361
diff
changeset

143 
handle List.Empty => raise COMPLETENESS 
33083  144 

145 
val patss = map (map snd) x_pats 

146 
val complete_thm = prove_completeness thy xs thesis qss patss 

36945  147 
> fold_rev (Thm.forall_intr o cterm_of thy) vs 
33083  148 
in 
149 
PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st)) 

150 
end 

151 
handle COMPLETENESS => no_tac) 

152 

153 
end 