src/HOL/Tools/Function/pat_completeness.ML
author wenzelm
Wed Mar 21 11:00:34 2012 +0100 (2012-03-21)
changeset 47060 e2741ec9ae36
parent 42361 23f352990944
child 47432 e1576d13e933
permissions -rw-r--r--
prefer explicitly qualified exception List.Empty;
     1 (*  Title:      HOL/Tools/Function/pat_completeness.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 Function_Lib
    21 open Function_Common
    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 = Thm.forall_elim inst o Thm.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 Thm.assume eqs)) c_assum
    73   in
    74     (subps @ pats,
    75      fold_rev Thm.implies_intr eqs (Thm.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 = Thm.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     |> Thm.implies_intr c_hyp
    90     |> fold_rev (Thm.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 (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
   123     val assums = map2 inst_hyps hyps qss
   124     in
   125       o_alg thy P 2 xs (patss ~~ assums)
   126       |> fold_rev Thm.implies_intr hyps
   127     end
   128 
   129 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   130   let
   131     val thy = Proof_Context.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 List.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 (Thm.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