src/HOL/Tools/Function/pat_completeness.ML
author wenzelm
Thu Apr 12 18:39:19 2012 +0200 (2012-04-12)
changeset 47432 e1576d13e933
parent 47060 e2741ec9ae36
child 51717 9e7d1c139569
permissions -rw-r--r--
more standard method setup;
     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 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 
    17 open Function_Lib
    18 open Function_Common
    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 
    24 fun inst_free var inst = Thm.forall_elim inst o Thm.forall_intr var
    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)
    69     val c_eq_pat = simplify (HOL_basic_ss addsimps (map Thm.assume eqs)) c_assum
    70   in
    71     (subps @ pats,
    72      fold_rev Thm.implies_intr eqs (Thm.implies_elim thm c_eq_pat))
    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))))
    82     val c_assum = Thm.assume c_hyp
    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
    86     |> Thm.implies_intr c_hyp
    87     |> fold_rev (Thm.forall_intr o cterm_of thy) avars
    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
   119     fun inst_hyps hyp qs = fold (Thm.forall_elim o cterm_of thy) qs (Thm.assume hyp)
   120     val assums = map2 inst_hyps hyps qss
   121     in
   122       o_alg thy P 2 xs (patss ~~ assums)
   123       |> fold_rev Thm.implies_intr hyps
   124     end
   125 
   126 fun pat_completeness_tac ctxt = SUBGOAL (fn (subgoal, i) =>
   127   let
   128     val thy = Proof_Context.theory_of ctxt
   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)
   143       handle List.Empty => raise COMPLETENESS
   144 
   145     val patss = map (map snd) x_pats
   146     val complete_thm = prove_completeness thy xs thesis qss patss
   147       |> fold_rev (Thm.forall_intr o cterm_of thy) vs
   148     in
   149       PRIMITIVE (fn st => Drule.compose_single(complete_thm, i, st))
   150   end
   151   handle COMPLETENESS => no_tac)
   152 
   153 end