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