src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
author wenzelm
Wed Jul 08 21:33:00 2015 +0200 (2015-07-08)
changeset 60696 8304fb4fb823
parent 59582 0fbed69ff081
child 60752 b48830b670a1
permissions -rw-r--r--
clarified context;
bulwahn@40052
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
bulwahn@40052
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@40052
     3
bulwahn@40052
     4
Proof procedure for the compiler from predicates specified by intro/elim rules to equations.
bulwahn@40052
     5
*)
bulwahn@40052
     6
bulwahn@40052
     7
signature PREDICATE_COMPILE_PROOF =
bulwahn@40052
     8
sig
bulwahn@40052
     9
  type indprem = Predicate_Compile_Aux.indprem;
bulwahn@40052
    10
  type mode = Predicate_Compile_Aux.mode
bulwahn@40052
    11
  val prove_pred : Predicate_Compile_Aux.options -> theory
bulwahn@40052
    12
    -> (string * (term list * indprem list) list) list
bulwahn@40052
    13
    -> (string * typ) list -> string -> bool * mode
bulwahn@40052
    14
    -> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term
bulwahn@40052
    15
    -> Thm.thm
bulwahn@40052
    16
end;
bulwahn@40052
    17
bulwahn@40052
    18
structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF =
bulwahn@40052
    19
struct
bulwahn@40052
    20
bulwahn@40052
    21
open Predicate_Compile_Aux;
bulwahn@40052
    22
open Core_Data;
bulwahn@40052
    23
open Mode_Inference;
bulwahn@40052
    24
wenzelm@55437
    25
bulwahn@40052
    26
(* debug stuff *)
bulwahn@40052
    27
wenzelm@56491
    28
fun trace_tac ctxt options s =
wenzelm@56491
    29
  if show_proof_trace options then print_tac ctxt s else Seq.single;
bulwahn@40052
    30
wenzelm@56491
    31
fun assert_tac ctxt pos pred =
wenzelm@56491
    32
  COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac);
bulwahn@40052
    33
bulwahn@40052
    34
bulwahn@40052
    35
(** special setup for simpset **)
wenzelm@55437
    36
wenzelm@51717
    37
val HOL_basic_ss' =
wenzelm@51717
    38
  simpset_of (put_simpset HOL_basic_ss @{context}
wenzelm@51717
    39
    addsimps @{thms simp_thms Pair_eq}
wenzelm@51717
    40
    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
wenzelm@51717
    41
    setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI})))
bulwahn@40052
    42
wenzelm@55437
    43
bulwahn@40052
    44
(* auxillary functions *)
bulwahn@40052
    45
blanchet@55399
    46
(* returns true if t is an application of a datatype constructor *)
bulwahn@40052
    47
(* which then consequently would be splitted *)
blanchet@55399
    48
fun is_constructor ctxt t =
blanchet@55399
    49
  (case fastype_of t of
blanchet@55399
    50
    Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t
wenzelm@55440
    51
  | _ => false)
bulwahn@40052
    52
bulwahn@40052
    53
(* MAJOR FIXME:  prove_params should be simple
bulwahn@40052
    54
 - different form of introrule for parameters ? *)
bulwahn@40052
    55
bulwahn@40052
    56
fun prove_param options ctxt nargs t deriv =
bulwahn@40052
    57
  let
blanchet@55399
    58
    val (f, args) = strip_comb (Envir.eta_contract t)
bulwahn@40052
    59
    val mode = head_mode_of deriv
bulwahn@40052
    60
    val param_derivations = param_derivations_of deriv
bulwahn@40052
    61
    val ho_args = ho_args_of mode args
wenzelm@55437
    62
    val f_tac =
wenzelm@55437
    63
      (case f of
wenzelm@55437
    64
        Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
wenzelm@55437
    65
           [@{thm eval_pred}, predfun_definition_of ctxt name mode,
wenzelm@55437
    66
           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
wenzelm@55437
    67
           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
wenzelm@55437
    68
      | Free _ =>
wenzelm@56490
    69
        Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
wenzelm@55437
    70
          let
wenzelm@55437
    71
            val prems' = maps dest_conjunct_prem (take nargs prems)
wenzelm@55437
    72
          in
wenzelm@55437
    73
            rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
wenzelm@55437
    74
          end) ctxt 1
wenzelm@55437
    75
      | Abs _ => raise Fail "prove_param: No valid parameter term")
bulwahn@40052
    76
  in
bulwahn@40052
    77
    REPEAT_DETERM (rtac @{thm ext} 1)
wenzelm@56491
    78
    THEN trace_tac ctxt options "prove_param"
wenzelm@56490
    79
    THEN f_tac
wenzelm@56491
    80
    THEN trace_tac ctxt options "after prove_param"
wenzelm@58963
    81
    THEN (REPEAT_DETERM (assume_tac ctxt 1))
bulwahn@40052
    82
    THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
bulwahn@40052
    83
    THEN REPEAT_DETERM (rtac @{thm refl} 1)
bulwahn@40052
    84
  end
bulwahn@40052
    85
bulwahn@40052
    86
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) =
wenzelm@55437
    87
  (case strip_comb t of
haftmann@50056
    88
    (Const (name, _), args) =>
bulwahn@40052
    89
      let
bulwahn@40052
    90
        val mode = head_mode_of deriv
bulwahn@40052
    91
        val introrule = predfun_intro_of ctxt name mode
bulwahn@40052
    92
        val param_derivations = param_derivations_of deriv
bulwahn@40052
    93
        val ho_args = ho_args_of mode args
bulwahn@40052
    94
      in
wenzelm@56491
    95
        trace_tac ctxt options "before intro rule:"
bulwahn@40052
    96
        THEN rtac introrule 1
wenzelm@56491
    97
        THEN trace_tac ctxt options "after intro rule"
bulwahn@40052
    98
        (* for the right assumption in first position *)
bulwahn@40052
    99
        THEN rotate_tac premposition 1
wenzelm@58963
   100
        THEN assume_tac ctxt 1
wenzelm@56491
   101
        THEN trace_tac ctxt options "parameter goal"
bulwahn@40052
   102
        (* work with parameter arguments *)
bulwahn@40052
   103
        THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations))
wenzelm@58963
   104
        THEN (REPEAT_DETERM (assume_tac ctxt 1))
bulwahn@40052
   105
      end
bulwahn@40052
   106
  | (Free _, _) =>
wenzelm@56491
   107
      trace_tac ctxt options "proving parameter call.."
wenzelm@56490
   108
      THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} =>
wenzelm@55437
   109
          let
wenzelm@55437
   110
            val param_prem = nth prems premposition
wenzelm@59582
   111
            val (param, _) = strip_comb (HOLogic.dest_Trueprop (Thm.prop_of param_prem))
wenzelm@55437
   112
            val prems' = maps dest_conjunct_prem (take nargs prems)
wenzelm@55437
   113
            fun param_rewrite prem =
wenzelm@59582
   114
              param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of prem)))
wenzelm@55437
   115
            val SOME rew_eq = find_first param_rewrite prems'
wenzelm@55437
   116
            val param_prem' = rewrite_rule ctxt'
wenzelm@55437
   117
              (map (fn th => th RS @{thm eq_reflection})
wenzelm@55437
   118
                [rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}])
wenzelm@55437
   119
              param_prem
wenzelm@55437
   120
          in
wenzelm@55437
   121
            rtac param_prem' 1
wenzelm@55437
   122
          end) ctxt 1
wenzelm@56491
   123
      THEN trace_tac ctxt options "after prove parameter call")
bulwahn@40052
   124
wenzelm@59582
   125
fun SOLVED tac st = FILTER (fn st' => Thm.nprems_of st' = Thm.nprems_of st - 1) tac st
bulwahn@40052
   126
bulwahn@40052
   127
fun prove_match options ctxt nargs out_ts =
bulwahn@40052
   128
  let
bulwahn@40052
   129
    val eval_if_P =
wenzelm@56490
   130
      @{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp}
bulwahn@40052
   131
    fun get_case_rewrite t =
blanchet@55399
   132
      if is_constructor ctxt t then
wenzelm@45701
   133
        let
blanchet@55399
   134
          val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
wenzelm@45701
   135
        in
blanchet@55399
   136
          fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) []
wenzelm@45701
   137
        end
bulwahn@40052
   138
      else []
blanchet@55642
   139
    val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"}
bulwahn@40052
   140
      (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
bulwahn@40052
   141
  (* replace TRY by determining if it necessary - are there equations when calling compile match? *)
bulwahn@40052
   142
  in
wenzelm@55437
   143
    (* make this simpset better! *)
wenzelm@51717
   144
    asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1
wenzelm@56491
   145
    THEN trace_tac ctxt options "after prove_match:"
wenzelm@56490
   146
    THEN (DETERM (TRY
bulwahn@40052
   147
           (rtac eval_if_P 1
wenzelm@60696
   148
           THEN (SUBPROOF (fn {prems, context = ctxt', ...} =>
bulwahn@40052
   149
             (REPEAT_DETERM (rtac @{thm conjI} 1
wenzelm@60696
   150
             THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1))))
wenzelm@60696
   151
             THEN trace_tac ctxt' options "if condition to be solved:"
wenzelm@60696
   152
             THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1
bulwahn@40052
   153
             THEN TRY (
bulwahn@40052
   154
                let
bulwahn@40052
   155
                  val prems' = maps dest_conjunct_prem (take nargs prems)
bulwahn@40052
   156
                in
wenzelm@60696
   157
                  rewrite_goal_tac ctxt'
bulwahn@40052
   158
                    (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
bulwahn@40052
   159
                end
bulwahn@40052
   160
             THEN REPEAT_DETERM (rtac @{thm refl} 1))
wenzelm@60696
   161
             THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1))))
wenzelm@56491
   162
    THEN trace_tac ctxt options "after if simplification"
bulwahn@40052
   163
  end;
bulwahn@40052
   164
wenzelm@55437
   165
bulwahn@40052
   166
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
bulwahn@40052
   167
bulwahn@40052
   168
fun prove_sidecond ctxt t =
bulwahn@40052
   169
  let
wenzelm@55437
   170
    fun preds_of t nameTs =
wenzelm@55437
   171
      (case strip_comb t of
wenzelm@55437
   172
        (Const (name, T), args) =>
wenzelm@55437
   173
          if is_registered ctxt name then (name, T) :: nameTs
wenzelm@55437
   174
            else fold preds_of args nameTs
wenzelm@55437
   175
      | _ => nameTs)
bulwahn@40052
   176
    val preds = preds_of t []
bulwahn@40052
   177
    val defs = map
bulwahn@40052
   178
      (fn (pred, T) => predfun_definition_of ctxt pred
bulwahn@40052
   179
        (all_input_of T))
bulwahn@40052
   180
        preds
wenzelm@56490
   181
  in
wenzelm@51717
   182
    simp_tac (put_simpset HOL_basic_ss ctxt
wenzelm@51717
   183
      addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1
bulwahn@40052
   184
    (* need better control here! *)
bulwahn@40052
   185
  end
bulwahn@40052
   186
bulwahn@40052
   187
fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) =
bulwahn@40052
   188
  let
bulwahn@40052
   189
    val (in_ts, clause_out_ts) = split_mode mode ts;
bulwahn@40052
   190
    fun prove_prems out_ts [] =
wenzelm@55437
   191
        (prove_match options ctxt nargs out_ts)
wenzelm@56491
   192
        THEN trace_tac ctxt options "before simplifying assumptions"
wenzelm@55437
   193
        THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1
wenzelm@56491
   194
        THEN trace_tac ctxt options "before single intro rule"
wenzelm@55437
   195
        THEN Subgoal.FOCUS_PREMS
wenzelm@56490
   196
           (fn {context = ctxt', prems, ...} =>
bulwahn@40052
   197
            let
wenzelm@55437
   198
              val prems' = maps dest_conjunct_prem (take nargs prems)
bulwahn@40052
   199
            in
wenzelm@55437
   200
              rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1
wenzelm@55437
   201
            end) ctxt 1
wenzelm@55437
   202
        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
wenzelm@55437
   203
    | prove_prems out_ts ((p, deriv) :: ps) =
wenzelm@55437
   204
        let
wenzelm@55437
   205
          val premposition = (find_index (equal p) clauses) + nargs
wenzelm@55437
   206
          val mode = head_mode_of deriv
wenzelm@55437
   207
          val rest_tac =
wenzelm@55437
   208
            rtac @{thm bindI} 1
wenzelm@55437
   209
            THEN (case p of Prem t =>
wenzelm@55437
   210
              let
wenzelm@55437
   211
                val (_, us) = strip_comb t
wenzelm@55437
   212
                val (_, out_ts''') = split_mode mode us
wenzelm@55437
   213
                val rec_tac = prove_prems out_ts''' ps
wenzelm@55437
   214
              in
wenzelm@56491
   215
                trace_tac ctxt options "before clause:"
wenzelm@55437
   216
                (*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*)
wenzelm@56491
   217
                THEN trace_tac ctxt options "before prove_expr:"
wenzelm@55437
   218
                THEN prove_expr options ctxt nargs premposition (t, deriv)
wenzelm@56491
   219
                THEN trace_tac ctxt options "after prove_expr:"
wenzelm@55437
   220
                THEN rec_tac
wenzelm@55437
   221
              end
wenzelm@55437
   222
            | Negprem t =>
wenzelm@55437
   223
              let
wenzelm@55437
   224
                val (t, args) = strip_comb t
wenzelm@55437
   225
                val (_, out_ts''') = split_mode mode args
wenzelm@55437
   226
                val rec_tac = prove_prems out_ts''' ps
wenzelm@55437
   227
                val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
wenzelm@55437
   228
                val neg_intro_rule =
wenzelm@55437
   229
                  Option.map (fn name =>
wenzelm@55437
   230
                    the (predfun_neg_intro_of ctxt name mode)) name
wenzelm@55437
   231
                val param_derivations = param_derivations_of deriv
wenzelm@55437
   232
                val params = ho_args_of mode args
wenzelm@55437
   233
              in
wenzelm@56491
   234
                trace_tac ctxt options "before prove_neg_expr:"
wenzelm@55437
   235
                THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
wenzelm@55437
   236
                  [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
wenzelm@55437
   237
                   @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
wenzelm@55437
   238
                THEN (if (is_some name) then
wenzelm@56491
   239
                    trace_tac ctxt options "before applying not introduction rule"
wenzelm@56490
   240
                    THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
wenzelm@56490
   241
                      rtac (the neg_intro_rule) 1
wenzelm@56490
   242
                      THEN rtac (nth prems premposition) 1) ctxt 1
wenzelm@56491
   243
                    THEN trace_tac ctxt options "after applying not introduction rule"
wenzelm@55437
   244
                    THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations))
wenzelm@58963
   245
                    THEN (REPEAT_DETERM (assume_tac ctxt 1))
wenzelm@55437
   246
                  else
wenzelm@55437
   247
                    rtac @{thm not_predI'} 1
wenzelm@55437
   248
                    (* test: *)
wenzelm@55437
   249
                    THEN dtac @{thm sym} 1
wenzelm@55437
   250
                    THEN asm_full_simp_tac
wenzelm@55437
   251
                      (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1)
wenzelm@55437
   252
                    THEN simp_tac
wenzelm@55437
   253
                      (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
wenzelm@55437
   254
                THEN rec_tac
wenzelm@55437
   255
              end
wenzelm@55437
   256
            | Sidecond t =>
wenzelm@55437
   257
             rtac @{thm if_predI} 1
wenzelm@56491
   258
             THEN trace_tac ctxt options "before sidecond:"
wenzelm@55437
   259
             THEN prove_sidecond ctxt t
wenzelm@56491
   260
             THEN trace_tac ctxt options "after sidecond:"
wenzelm@55437
   261
             THEN prove_prems [] ps)
wenzelm@55437
   262
        in (prove_match options ctxt nargs out_ts)
wenzelm@55437
   263
            THEN rest_tac
wenzelm@55437
   264
        end
bulwahn@40052
   265
    val prems_tac = prove_prems in_ts moded_ps
bulwahn@40052
   266
  in
wenzelm@56491
   267
    trace_tac ctxt options "Proving clause..."
bulwahn@40052
   268
    THEN rtac @{thm bindI} 1
bulwahn@40052
   269
    THEN rtac @{thm singleI} 1
bulwahn@40052
   270
    THEN prems_tac
wenzelm@55437
   271
  end
bulwahn@40052
   272
bulwahn@40052
   273
fun select_sup 1 1 = []
bulwahn@40052
   274
  | select_sup _ 1 = [rtac @{thm supI1}]
bulwahn@40052
   275
  | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1));
bulwahn@40052
   276
bulwahn@40052
   277
fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
bulwahn@40052
   278
  let
bulwahn@40052
   279
    val T = the (AList.lookup (op =) preds pred)
bulwahn@40052
   280
    val nargs = length (binder_types T)
bulwahn@40052
   281
    val pred_case_rule = the_elim_of ctxt pred
bulwahn@40052
   282
  in
wenzelm@54742
   283
    REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))
wenzelm@56491
   284
    THEN trace_tac ctxt options "before applying elim rule"
bulwahn@40052
   285
    THEN etac (predfun_elim_of ctxt pred mode) 1
bulwahn@40052
   286
    THEN etac pred_case_rule 1
wenzelm@56491
   287
    THEN trace_tac ctxt options "after applying elim rule"
bulwahn@40052
   288
    THEN (EVERY (map
wenzelm@56490
   289
           (fn i => EVERY' (select_sup (length moded_clauses) i) i)
bulwahn@40052
   290
             (1 upto (length moded_clauses))))
bulwahn@40052
   291
    THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses))
wenzelm@56491
   292
    THEN trace_tac ctxt options "proved one direction"
wenzelm@55437
   293
  end
wenzelm@55437
   294
bulwahn@40052
   295
bulwahn@40052
   296
(** Proof in the other direction **)
bulwahn@40052
   297
bulwahn@40052
   298
fun prove_match2 options ctxt out_ts =
bulwahn@40052
   299
  let
bulwahn@40052
   300
    fun split_term_tac (Free _) = all_tac
bulwahn@40052
   301
      | split_term_tac t =
blanchet@55399
   302
        if is_constructor ctxt t then
bulwahn@40052
   303
          let
blanchet@55399
   304
            val SOME {case_thms, split_asm, ...} =
blanchet@55399
   305
              Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t)))
blanchet@55399
   306
            val num_of_constrs = length case_thms
bulwahn@40052
   307
            val (_, ts) = strip_comb t
bulwahn@40052
   308
          in
wenzelm@56491
   309
            trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
blanchet@55420
   310
              " splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
wenzelm@58956
   311
            THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
wenzelm@56491
   312
              THEN (trace_tac ctxt options "after splitting with split_asm rules")
wenzelm@51717
   313
            (* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
bulwahn@40052
   314
              THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
bulwahn@40052
   315
              THEN (REPEAT_DETERM_N (num_of_constrs - 1)
bulwahn@40052
   316
                (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)))
wenzelm@56491
   317
            THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2)
bulwahn@40052
   318
            THEN (EVERY (map split_term_tac ts))
bulwahn@40052
   319
          end
bulwahn@40052
   320
      else all_tac
bulwahn@40052
   321
  in
bulwahn@40052
   322
    split_term_tac (HOLogic.mk_tuple out_ts)
wenzelm@58956
   323
    THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
bulwahn@40052
   324
    THEN (etac @{thm botE} 2))))
bulwahn@40052
   325
  end
bulwahn@40052
   326
wenzelm@56490
   327
(* VERY LARGE SIMILIRATIY to function prove_param
bulwahn@40052
   328
-- join both functions
bulwahn@40052
   329
*)
bulwahn@40052
   330
(* TODO: remove function *)
bulwahn@40052
   331
bulwahn@40052
   332
fun prove_param2 options ctxt t deriv =
bulwahn@40052
   333
  let
bulwahn@40052
   334
    val (f, args) = strip_comb (Envir.eta_contract t)
bulwahn@40052
   335
    val mode = head_mode_of deriv
bulwahn@40052
   336
    val param_derivations = param_derivations_of deriv
bulwahn@40052
   337
    val ho_args = ho_args_of mode args
wenzelm@55437
   338
    val f_tac =
wenzelm@55437
   339
      (case f of
wenzelm@56490
   340
        Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
bulwahn@40052
   341
           (@{thm eval_pred}::(predfun_definition_of ctxt name mode)
bulwahn@40052
   342
           :: @{thm "Product_Type.split_conv"}::[])) 1
bulwahn@40052
   343
      | Free _ => all_tac
wenzelm@55437
   344
      | _ => error "prove_param2: illegal parameter term")
bulwahn@40052
   345
  in
wenzelm@56491
   346
    trace_tac ctxt options "before simplification in prove_args:"
bulwahn@40052
   347
    THEN f_tac
wenzelm@56491
   348
    THEN trace_tac ctxt options "after simplification in prove_args"
bulwahn@40052
   349
    THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)
bulwahn@40052
   350
  end
bulwahn@40052
   351
wenzelm@56490
   352
fun prove_expr2 options ctxt (t, deriv) =
bulwahn@40052
   353
  (case strip_comb t of
haftmann@50056
   354
      (Const (name, _), args) =>
bulwahn@40052
   355
        let
bulwahn@40052
   356
          val mode = head_mode_of deriv
bulwahn@40052
   357
          val param_derivations = param_derivations_of deriv
bulwahn@40052
   358
          val ho_args = ho_args_of mode args
bulwahn@40052
   359
        in
bulwahn@40052
   360
          etac @{thm bindE} 1
wenzelm@54742
   361
          THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
wenzelm@56491
   362
          THEN trace_tac ctxt options "prove_expr2-before"
bulwahn@40052
   363
          THEN etac (predfun_elim_of ctxt name mode) 1
wenzelm@56491
   364
          THEN trace_tac ctxt options "prove_expr2"
bulwahn@40052
   365
          THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
wenzelm@56491
   366
          THEN trace_tac ctxt options "finished prove_expr2"
bulwahn@40052
   367
        end
bulwahn@40052
   368
      | _ => etac @{thm bindE} 1)
bulwahn@40052
   369
wenzelm@55437
   370
fun prove_sidecond2 options ctxt t =
wenzelm@55437
   371
  let
wenzelm@55437
   372
    fun preds_of t nameTs =
wenzelm@55437
   373
      (case strip_comb t of
wenzelm@55437
   374
        (Const (name, T), args) =>
wenzelm@55437
   375
          if is_registered ctxt name then (name, T) :: nameTs
wenzelm@55437
   376
            else fold preds_of args nameTs
wenzelm@55437
   377
      | _ => nameTs)
wenzelm@55437
   378
    val preds = preds_of t []
wenzelm@55437
   379
    val defs = map
wenzelm@56490
   380
      (fn (pred, T) => predfun_definition_of ctxt pred
wenzelm@55437
   381
        (all_input_of T))
wenzelm@55437
   382
        preds
bulwahn@40052
   383
  in
wenzelm@55437
   384
    (* only simplify the one assumption *)
wenzelm@56490
   385
    full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1
wenzelm@55437
   386
    (* need better control here! *)
wenzelm@56491
   387
    THEN trace_tac ctxt options "after sidecond2 simplification"
wenzelm@55437
   388
  end
wenzelm@56490
   389
bulwahn@40052
   390
fun prove_clause2 options ctxt pred mode (ts, ps) i =
bulwahn@40052
   391
  let
bulwahn@40052
   392
    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
haftmann@50056
   393
    val (in_ts, _) = split_mode mode ts;
wenzelm@51717
   394
    val split_simpset =
wenzelm@51717
   395
      put_simpset HOL_basic_ss' ctxt
wenzelm@51717
   396
      addsimps [@{thm split_eta}, @{thm split_beta},
wenzelm@51717
   397
        @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
bulwahn@40052
   398
    fun prove_prems2 out_ts [] =
wenzelm@56491
   399
      trace_tac ctxt options "before prove_match2 - last call:"
bulwahn@40052
   400
      THEN prove_match2 options ctxt out_ts
wenzelm@56491
   401
      THEN trace_tac ctxt options "after prove_match2 - last call:"
bulwahn@40052
   402
      THEN (etac @{thm singleE} 1)
bulwahn@40052
   403
      THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
wenzelm@51717
   404
      THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
bulwahn@40052
   405
      THEN TRY (
bulwahn@40052
   406
        (REPEAT_DETERM (etac @{thm Pair_inject} 1))
wenzelm@51717
   407
        THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1)
wenzelm@56490
   408
wenzelm@56491
   409
        THEN SOLVED (trace_tac ctxt options "state before applying intro rule:"
bulwahn@40052
   410
        THEN (rtac pred_intro_rule
bulwahn@40052
   411
        (* How to handle equality correctly? *)
wenzelm@56491
   412
        THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching")
wenzelm@58963
   413
        THEN' (assume_tac ctxt ORELSE'
wenzelm@58963
   414
          ((CHANGED o asm_full_simp_tac split_simpset) THEN'
wenzelm@58963
   415
            (TRY o assume_tac ctxt))) THEN'
wenzelm@58963
   416
          (K (trace_tac ctxt options "state after pre-simplification:"))
wenzelm@56491
   417
        THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1))
bulwahn@40052
   418
    | prove_prems2 out_ts ((p, deriv) :: ps) =
bulwahn@40052
   419
      let
bulwahn@40052
   420
        val mode = head_mode_of deriv
wenzelm@55437
   421
        val rest_tac =
wenzelm@55437
   422
          (case p of
wenzelm@55437
   423
            Prem t =>
wenzelm@55437
   424
              let
wenzelm@55437
   425
                val (_, us) = strip_comb t
wenzelm@55437
   426
                val (_, out_ts''') = split_mode mode us
wenzelm@55437
   427
                val rec_tac = prove_prems2 out_ts''' ps
wenzelm@55437
   428
              in
wenzelm@55437
   429
                (prove_expr2 options ctxt (t, deriv)) THEN rec_tac
wenzelm@55437
   430
              end
wenzelm@55437
   431
          | Negprem t =>
wenzelm@55437
   432
              let
wenzelm@55437
   433
                val (_, args) = strip_comb t
wenzelm@55437
   434
                val (_, out_ts''') = split_mode mode args
wenzelm@55437
   435
                val rec_tac = prove_prems2 out_ts''' ps
wenzelm@55437
   436
                val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE)
wenzelm@55437
   437
                val param_derivations = param_derivations_of deriv
wenzelm@55437
   438
                val ho_args = ho_args_of mode args
wenzelm@55437
   439
              in
wenzelm@56491
   440
                trace_tac ctxt options "before neg prem 2"
wenzelm@55437
   441
                THEN etac @{thm bindE} 1
wenzelm@55437
   442
                THEN (if is_some name then
wenzelm@55437
   443
                    full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
wenzelm@55437
   444
                      [predfun_definition_of ctxt (the name) mode]) 1
wenzelm@55437
   445
                    THEN etac @{thm not_predE} 1
wenzelm@55437
   446
                    THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1
wenzelm@55437
   447
                    THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations))
wenzelm@55437
   448
                  else
wenzelm@55437
   449
                    etac @{thm not_predE'} 1)
wenzelm@55437
   450
                THEN rec_tac
wenzelm@56490
   451
              end
wenzelm@55437
   452
          | Sidecond t =>
wenzelm@55437
   453
              etac @{thm bindE} 1
wenzelm@55437
   454
              THEN etac @{thm if_predE} 1
wenzelm@55437
   455
              THEN prove_sidecond2 options ctxt t
wenzelm@55437
   456
              THEN prove_prems2 [] ps)
wenzelm@55437
   457
      in
wenzelm@56491
   458
        trace_tac ctxt options "before prove_match2:"
wenzelm@55437
   459
        THEN prove_match2 options ctxt out_ts
wenzelm@56491
   460
        THEN trace_tac ctxt options "after prove_match2:"
wenzelm@55437
   461
        THEN rest_tac
wenzelm@55437
   462
      end
wenzelm@56490
   463
    val prems_tac = prove_prems2 in_ts ps
bulwahn@40052
   464
  in
wenzelm@56491
   465
    trace_tac ctxt options "starting prove_clause2"
bulwahn@40052
   466
    THEN etac @{thm bindE} 1
bulwahn@40052
   467
    THEN (etac @{thm singleE'} 1)
bulwahn@40052
   468
    THEN (TRY (etac @{thm Pair_inject} 1))
wenzelm@56491
   469
    THEN trace_tac ctxt options "after singleE':"
bulwahn@40052
   470
    THEN prems_tac
bulwahn@40052
   471
  end;
wenzelm@56490
   472
bulwahn@40052
   473
fun prove_other_direction options ctxt pred mode moded_clauses =
bulwahn@40052
   474
  let
bulwahn@40052
   475
    fun prove_clause clause i =
bulwahn@40052
   476
      (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
bulwahn@40052
   477
      THEN (prove_clause2 options ctxt pred mode clause i)
bulwahn@40052
   478
  in
bulwahn@40052
   479
    (DETERM (TRY (rtac @{thm unit.induct} 1)))
wenzelm@54742
   480
     THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})))
bulwahn@40052
   481
     THEN (rtac (predfun_intro_of ctxt pred mode) 1)
bulwahn@40052
   482
     THEN (REPEAT_DETERM (rtac @{thm refl} 2))
wenzelm@54742
   483
     THEN (
wenzelm@54742
   484
       if null moded_clauses then etac @{thm botE} 1
bulwahn@40052
   485
       else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses))))
wenzelm@55437
   486
  end
wenzelm@55437
   487
bulwahn@40052
   488
bulwahn@40052
   489
(** proof procedure **)
bulwahn@40052
   490
haftmann@50056
   491
fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
bulwahn@40052
   492
  let
wenzelm@51552
   493
    val ctxt = Proof_Context.init_global thy   (* FIXME proper context!? *)
wenzelm@55437
   494
    val clauses = (case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [])
bulwahn@40052
   495
  in
bulwahn@40052
   496
    Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
bulwahn@40052
   497
      (if not (skip_proof options) then
bulwahn@40052
   498
        (fn _ =>
bulwahn@40052
   499
        rtac @{thm pred_iffI} 1
wenzelm@56491
   500
        THEN trace_tac ctxt options "after pred_iffI"
bulwahn@40052
   501
        THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses
wenzelm@56491
   502
        THEN trace_tac ctxt options "proved one direction"
bulwahn@40052
   503
        THEN prove_other_direction options ctxt pred mode moded_clauses
wenzelm@56491
   504
        THEN trace_tac ctxt options "proved other direction")
wenzelm@59498
   505
      else (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt)))
wenzelm@55437
   506
  end
bulwahn@40052
   507
wenzelm@55437
   508
end