src/HOL/Tools/Function/function_elims.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59618 e6939796717e
child 59627 bb1e4a35d506
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
Manuel@53603
     1
(*  Title:      HOL/Tools/Function/function_elims.ML
krauss@53609
     2
    Author:     Manuel Eberl, TU Muenchen
Manuel@53603
     3
wenzelm@53666
     4
Generate the pelims rules for a function. These are of the shape
wenzelm@53664
     5
[|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P
Manuel@53603
     6
and are derived from the cases rule. There is at least one pelim rule for
Manuel@53603
     7
each function (cf. mutually recursive functions)
Manuel@53603
     8
There may be more than one pelim rule for a function in case of functions
Manuel@53603
     9
that return a boolean. For such a function, e.g. P x, not only the normal
Manuel@53603
    10
elim rule with the premise P x = z is generated, but also two additional
wenzelm@53664
    11
elim rules with P x resp. \<not>P x as premises.
Manuel@53603
    12
*)
Manuel@53603
    13
Manuel@53603
    14
signature FUNCTION_ELIMS =
Manuel@53603
    15
sig
Manuel@53603
    16
  val dest_funprop : term -> (term * term list) * term
wenzelm@53667
    17
  val mk_partial_elim_rules : Proof.context ->
wenzelm@53666
    18
    Function_Common.function_result -> thm list list
Manuel@53603
    19
end;
Manuel@53603
    20
Manuel@53603
    21
structure Function_Elims : FUNCTION_ELIMS =
Manuel@53603
    22
struct
Manuel@53603
    23
Manuel@53603
    24
open Function_Lib
Manuel@53603
    25
open Function_Common
Manuel@53603
    26
wenzelm@53669
    27
(* Extract a function and its arguments from a proposition that is
Manuel@53603
    28
   either of the form "f x y z = ..." or, in case of function that
Manuel@53603
    29
   returns a boolean, "f x y z" *)
wenzelm@53669
    30
fun dest_funprop (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (strip_comb lhs, rhs)
wenzelm@53669
    31
  | dest_funprop (Const (@{const_name Not}, _) $ trm) = (strip_comb trm, @{term "False"})
Manuel@53603
    32
  | dest_funprop trm = (strip_comb trm, @{term "True"});
Manuel@53603
    33
Manuel@53603
    34
local
wenzelm@53666
    35
wenzelm@54738
    36
fun propagate_tac ctxt i =
wenzelm@54736
    37
  let
wenzelm@54736
    38
    fun inspect eq =
wenzelm@54736
    39
      (case eq of
wenzelm@54736
    40
        Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) =>
wenzelm@54736
    41
          if Logic.occs (Free x, t) then raise Match else true
wenzelm@54736
    42
      | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) =>
wenzelm@54736
    43
          if Logic.occs (Free x, t) then raise Match else false
wenzelm@54736
    44
      | _ => raise Match);
wenzelm@54736
    45
    fun mk_eq thm =
wenzelm@59582
    46
      (if inspect (Thm.prop_of thm) then [thm RS eq_reflection]
wenzelm@54736
    47
       else [Thm.symmetric (thm RS eq_reflection)])
wenzelm@54736
    48
      handle Match => [];
wenzelm@54738
    49
    val simpset =
wenzelm@54738
    50
      empty_simpset ctxt
wenzelm@54736
    51
      |> Simplifier.set_mksimps (K mk_eq);
wenzelm@53666
    52
  in
wenzelm@54738
    53
    asm_lr_simp_tac simpset i
wenzelm@53666
    54
  end;
Manuel@53603
    55
wenzelm@54737
    56
val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+};
wenzelm@54736
    57
val boolE = @{thms HOL.TrueE HOL.FalseE};
wenzelm@54736
    58
val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+};
wenzelm@54737
    59
val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False};
Manuel@53603
    60
wenzelm@53666
    61
fun bool_subst_tac ctxt i =
wenzelm@54737
    62
  REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i)
wenzelm@59498
    63
  THEN REPEAT (dresolve_tac ctxt boolD i)
wenzelm@59498
    64
  THEN REPEAT (eresolve_tac ctxt boolE i)
Manuel@53603
    65
wenzelm@53666
    66
fun mk_bool_elims ctxt elim =
wenzelm@54736
    67
  let
wenzelm@54736
    68
    val tac = ALLGOALS (bool_subst_tac ctxt);
wenzelm@54736
    69
    fun mk_bool_elim b =
wenzelm@54736
    70
      elim
wenzelm@54736
    71
      |> Thm.forall_elim b
wenzelm@59498
    72
      |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac ctxt eq_boolI 1))
wenzelm@54736
    73
      |> Tactic.rule_by_tactic ctxt tac;
wenzelm@53666
    74
  in
wenzelm@54736
    75
    map mk_bool_elim [@{cterm True}, @{cterm False}]
wenzelm@53666
    76
  end;
Manuel@53603
    77
Manuel@53603
    78
in
Manuel@53603
    79
wenzelm@53667
    80
fun mk_partial_elim_rules ctxt result =
wenzelm@53667
    81
  let
wenzelm@54736
    82
    val thy = Proof_Context.theory_of ctxt;
wenzelm@53667
    83
wenzelm@54737
    84
    val FunctionResult {fs, R, dom, psimps, cases, ...} = result;
wenzelm@54736
    85
    val n_fs = length fs;
Manuel@53603
    86
wenzelm@54736
    87
    fun mk_partial_elim_rule (idx, f) =
wenzelm@54736
    88
      let
eberlm@59454
    89
        fun mk_var x T ctxt = case Name.variant x ctxt of (x, ctxt) => (Free (x, T), ctxt)
eberlm@59454
    90
        fun mk_funeq 0 T ctxt (acc_vars, acc_lhs) =
eberlm@59454
    91
              let val (y, ctxt) = mk_var "y" T ctxt
eberlm@59454
    92
              in  (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T, ctxt) end
eberlm@59454
    93
          | mk_funeq n (Type (@{type_name "fun"}, [S, T])) ctxt (acc_vars, acc_lhs) =
eberlm@59454
    94
              let val (xn, ctxt) = mk_var "x" S ctxt
eberlm@59454
    95
              in  mk_funeq (n - 1) T ctxt (xn :: acc_vars, acc_lhs $ xn) end
eberlm@59454
    96
          | mk_funeq _ _ _ _ = raise TERM ("Not a function.", [f]);
Manuel@53603
    97
wenzelm@54736
    98
        val f_simps =
wenzelm@54736
    99
          filter (fn r =>
wenzelm@59582
   100
            (Thm.prop_of r |> Logic.strip_assums_concl
wenzelm@54736
   101
              |> HOLogic.dest_Trueprop
wenzelm@54736
   102
              |> dest_funprop |> fst |> fst) = f)
wenzelm@54736
   103
            psimps;
Manuel@53603
   104
wenzelm@54736
   105
        val arity =
wenzelm@54736
   106
          hd f_simps
wenzelm@59582
   107
          |> Thm.prop_of
wenzelm@54736
   108
          |> Logic.strip_assums_concl
wenzelm@54736
   109
          |> HOLogic.dest_Trueprop
wenzelm@54736
   110
          |> snd o fst o dest_funprop
wenzelm@54736
   111
          |> length;
eberlm@59454
   112
        val name_ctxt = Variable.names_of ctxt
eberlm@59454
   113
        val (free_vars, prop, ranT, name_ctxt) = mk_funeq arity (fastype_of f) name_ctxt ([], f);
wenzelm@54736
   114
        val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs));
wenzelm@54736
   115
        val args = HOLogic.mk_tuple arg_vars;
wenzelm@54736
   116
        val domT = R |> dest_Free |> snd |> hd o snd o dest_Type;
Manuel@53603
   117
wenzelm@59621
   118
        val P = mk_var "P" @{typ "bool"} name_ctxt |> fst |> Thm.cterm_of ctxt
blanchet@55968
   119
        val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx+1) args;
wenzelm@54736
   120
wenzelm@59621
   121
        val cprop = Thm.cterm_of ctxt prop;
wenzelm@54736
   122
wenzelm@59621
   123
        val asms = [cprop, Thm.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))];
wenzelm@54736
   124
        val asms_thms = map Thm.assume asms;
Manuel@53603
   125
wenzelm@54737
   126
        fun prep_subgoal_tac i =
wenzelm@59498
   127
          REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
wenzelm@54736
   128
          THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
wenzelm@54738
   129
          THEN propagate_tac ctxt i
wenzelm@58963
   130
          THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
wenzelm@54736
   131
          THEN bool_subst_tac ctxt i;
Manuel@53603
   132
eberlm@59454
   133
        val elim_stripped =
eberlm@59454
   134
          nth cases idx
eberlm@59454
   135
          |> Thm.forall_elim P
wenzelm@59621
   136
          |> Thm.forall_elim (Thm.cterm_of ctxt args)
eberlm@59454
   137
          |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
eberlm@59454
   138
          |> fold_rev Thm.implies_intr asms
wenzelm@59621
   139
          |> Thm.forall_intr (Thm.cterm_of ctxt rhs_var);
Manuel@53603
   140
eberlm@59454
   141
        val bool_elims =
eberlm@59454
   142
          (case ranT of
eberlm@59454
   143
            Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped
eberlm@59454
   144
          | _ => []);
Manuel@53603
   145
eberlm@59454
   146
        fun unstrip rl =
eberlm@59454
   147
          rl
wenzelm@59621
   148
          |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars
eberlm@59454
   149
          |> Thm.forall_intr P
eberlm@59454
   150
      in
eberlm@59454
   151
        map unstrip (elim_stripped :: bool_elims)
eberlm@59454
   152
      end;
wenzelm@53666
   153
  in
wenzelm@53666
   154
    map_index mk_partial_elim_rule fs
Manuel@53603
   155
  end;
wenzelm@53666
   156
Manuel@53603
   157
end;
Manuel@53603
   158
wenzelm@53666
   159
end;