src/HOL/Tools/Function/pat_completeness.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 59627 bb1e4a35d506
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
     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: Proof.context -> 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 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 
    32 fun 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 
    43 fun 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 
    56 fun 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 
    69 exception COMPLETENESS
    70 
    71 fun 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
    85 and 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 
   106 fun 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 
   122 fun 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 
   148 end