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