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