src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 60752 b48830b670a1
child 61268 abe08fb15a12
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
wenzelm@33265
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
wenzelm@33265
     2
    Author:     Lukas Bulwahn, TU Muenchen
bulwahn@33250
     3
wenzelm@33265
     4
Preprocessing definitions of predicates to introduction rules.
bulwahn@33250
     5
*)
bulwahn@33250
     6
bulwahn@33250
     7
signature PREDICATE_COMPILE_PRED =
bulwahn@33250
     8
sig
bulwahn@33250
     9
  (* preprocesses an equation to a set of intro rules; defines new constants *)
bulwahn@35324
    10
  val preprocess : Predicate_Compile_Aux.options -> (string * thm list) -> theory
bulwahn@35324
    11
    -> ((string * thm list) list * theory) 
bulwahn@35324
    12
  val flat_higher_order_arguments : ((string * thm list) list * theory)
bulwahn@35324
    13
    -> ((string * thm list) list * ((string * thm list) list * theory))
bulwahn@33250
    14
end;
wenzelm@33265
    15
bulwahn@35324
    16
bulwahn@35324
    17
structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED =
bulwahn@33250
    18
struct
bulwahn@33250
    19
bulwahn@33250
    20
open Predicate_Compile_Aux
bulwahn@33250
    21
haftmann@50056
    22
fun is_compound ((Const (@{const_name Not}, _)) $ _) =
wenzelm@55437
    23
      error "is_compound: Negation should not occur; preprocessing is defect"
haftmann@38558
    24
  | is_compound ((Const (@{const_name Ex}, _)) $ _) = true
haftmann@38795
    25
  | is_compound ((Const (@{const_name HOL.disj}, _)) $ _ $ _) = true
haftmann@38795
    26
  | is_compound ((Const (@{const_name HOL.conj}, _)) $ _ $ _) =
wenzelm@55437
    27
      error "is_compound: Conjunction should not occur; preprocessing is defect"
bulwahn@33250
    28
  | is_compound _ = false
bulwahn@33250
    29
bulwahn@39723
    30
fun try_destruct_case thy names atom =
wenzelm@55437
    31
  (case find_split_thm thy (fst (strip_comb atom)) of
bulwahn@39723
    32
    NONE => NONE
bulwahn@39723
    33
  | SOME raw_split_thm =>
bulwahn@39723
    34
    let
wenzelm@42361
    35
      val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
bulwahn@39723
    36
      (* TODO: contextify things - this line is to unvarify the split_thm *)
bulwahn@39723
    37
      (*val ((_, [isplit_thm]), _) =
wenzelm@42361
    38
        Variable.import true [split_thm] (Proof_Context.init_global thy)*)
wenzelm@59582
    39
      val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm)
haftmann@50056
    40
      val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) 
bulwahn@39802
    41
      val atom' = case_betapply thy atom
bulwahn@39723
    42
      val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty)
bulwahn@39723
    43
      val names' = Term.add_free_names atom' names
bulwahn@39723
    44
      fun mk_subst_rhs assm =
bulwahn@39723
    45
        let
bulwahn@39723
    46
          val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
bulwahn@39723
    47
          val var_names = Name.variant_list names' (map fst vTs)
bulwahn@39723
    48
          val vars = map Free (var_names ~~ (map snd vTs))
bulwahn@39723
    49
          val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
bulwahn@39723
    50
          fun partition_prem_subst prem =
wenzelm@55437
    51
            (case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of
bulwahn@39723
    52
              (Free (x, T), r) => (NONE, SOME ((x, T), r))
wenzelm@55437
    53
            | _ => (SOME prem, NONE))
bulwahn@39723
    54
          fun partition f xs =
bulwahn@39723
    55
            let
bulwahn@39723
    56
              fun partition' acc1 acc2 [] = (rev acc1, rev acc2)
bulwahn@39723
    57
                | partition' acc1 acc2 (x :: xs) =
bulwahn@39723
    58
                  let
bulwahn@39723
    59
                    val (y, z) = f x
wenzelm@55437
    60
                    val acc1' = (case y of NONE => acc1 | SOME y' => y' :: acc1)
wenzelm@55437
    61
                    val acc2' = (case z of NONE => acc2 | SOME z' => z' :: acc2)
bulwahn@39723
    62
                  in partition' acc1' acc2' xs end
bulwahn@39723
    63
            in partition' [] [] xs end
bulwahn@39723
    64
          val (prems'', subst) = partition partition_prem_subst prems'
bulwahn@39723
    65
          val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
bulwahn@39723
    66
          val pre_rhs =
bulwahn@39723
    67
            fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
bulwahn@39723
    68
          val rhs = Envir.expand_term_frees subst pre_rhs
bulwahn@39723
    69
        in
wenzelm@55437
    70
          (case try_destruct_case thy (var_names @ names') rhs of
bulwahn@39723
    71
            NONE => [(subst, rhs)]
wenzelm@55437
    72
          | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs)
bulwahn@39723
    73
        end
wenzelm@55437
    74
     in SOME (atom', maps mk_subst_rhs assms) end)
bulwahn@39723
    75
     
bulwahn@33250
    76
fun flatten constname atom (defs, thy) =
bulwahn@33250
    77
  if is_compound atom then
bulwahn@33250
    78
    let
wenzelm@52131
    79
      val atom = Envir.beta_norm (Envir.eta_long [] atom)
wenzelm@55437
    80
      val constname =
wenzelm@55437
    81
        singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
wenzelm@55437
    82
          ((Long_Name.base_name constname) ^ "_aux")
bulwahn@33250
    83
      val full_constname = Sign.full_bname thy constname
bulwahn@33250
    84
      val (params, args) = List.partition (is_predT o fastype_of)
bulwahn@33250
    85
        (map Free (Term.add_frees atom []))
bulwahn@33250
    86
      val constT = map fastype_of (params @ args) ---> HOLogic.boolT
bulwahn@33250
    87
      val lhs = list_comb (Const (full_constname, constT), params @ args)
bulwahn@33250
    88
      val def = Logic.mk_equals (lhs, atom)
bulwahn@33250
    89
      val ([definition], thy') = thy
wenzelm@56239
    90
        |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
wenzelm@46909
    91
        |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
bulwahn@33250
    92
    in
bulwahn@33250
    93
      (lhs, ((full_constname, [definition]) :: defs, thy'))
bulwahn@33250
    94
    end
bulwahn@33250
    95
  else
wenzelm@55437
    96
    (case (fst (strip_comb atom)) of
bulwahn@37908
    97
      (Const (@{const_name If}, _)) =>
bulwahn@37908
    98
        let
bulwahn@35324
    99
          val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
wenzelm@41228
   100
          val atom' = Raw_Simplifier.rewrite_term thy
bulwahn@35324
   101
            (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
wenzelm@42816
   102
          val _ = @{assert} (not (atom = atom'))
bulwahn@35324
   103
        in
bulwahn@35324
   104
          flatten constname atom' (defs, thy)
bulwahn@35324
   105
        end
bulwahn@36029
   106
    | _ =>
wenzelm@55437
   107
        (case try_destruct_case thy [] atom of
wenzelm@55437
   108
          NONE => (atom, (defs, thy))
wenzelm@55437
   109
        | SOME (atom', srs) =>
wenzelm@55437
   110
            let      
wenzelm@55437
   111
              val frees = map Free (Term.add_frees atom' [])
wenzelm@55437
   112
              val constname =
wenzelm@55437
   113
                singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
wenzelm@55437
   114
                  ((Long_Name.base_name constname) ^ "_aux")
wenzelm@55437
   115
              val full_constname = Sign.full_bname thy constname
wenzelm@55437
   116
              val constT = map fastype_of frees ---> HOLogic.boolT
wenzelm@55437
   117
              val lhs = list_comb (Const (full_constname, constT), frees)
wenzelm@55437
   118
              fun mk_def (subst, rhs) =
wenzelm@55437
   119
                Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
wenzelm@55437
   120
              val new_defs = map mk_def srs
wenzelm@55437
   121
              val (definition, thy') = thy
wenzelm@56239
   122
              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
wenzelm@55437
   123
              |> fold_map Specification.axiom  (* FIXME !?!?!?! *)
wenzelm@55437
   124
                (map_index (fn (i, t) =>
wenzelm@55437
   125
                  ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs)
wenzelm@55437
   126
            in
wenzelm@55437
   127
              (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy'))
wenzelm@55437
   128
            end))
bulwahn@33250
   129
bulwahn@33250
   130
fun flatten_intros constname intros thy =
bulwahn@33250
   131
  let
wenzelm@51552
   132
    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
bulwahn@33250
   133
    val ((_, intros), ctxt') = Variable.import true intros ctxt
bulwahn@33250
   134
    val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
wenzelm@59582
   135
      (flatten constname) (map Thm.prop_of intros) ([], thy)
wenzelm@42361
   136
    val ctxt'' = Proof_Context.transfer thy' ctxt'
wenzelm@51552
   137
    val intros'' =
wenzelm@59498
   138
      map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt''))) intros'
bulwahn@37908
   139
      |> Variable.export ctxt'' ctxt
bulwahn@33250
   140
  in
bulwahn@33250
   141
    (intros'', (local_defs, thy'))
bulwahn@33250
   142
  end
bulwahn@33250
   143
wenzelm@60781
   144
fun introrulify ctxt ths = 
bulwahn@33250
   145
  let
bulwahn@33250
   146
    val ((_, ths'), ctxt') = Variable.import true ths ctxt
bulwahn@33250
   147
    fun introrulify' th =
bulwahn@33250
   148
      let
wenzelm@59582
   149
        val (lhs, rhs) = Logic.dest_equals (Thm.prop_of th)
bulwahn@33250
   150
        val frees = Term.add_free_names rhs []
bulwahn@33250
   151
        val disjuncts = HOLogic.dest_disj rhs
bulwahn@33250
   152
        val nctxt = Name.make_context frees
bulwahn@33250
   153
        fun mk_introrule t =
bulwahn@33250
   154
          let
haftmann@50056
   155
            val ((ps, t'), _) = focus_ex t nctxt
bulwahn@33250
   156
            val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t')
bulwahn@33250
   157
          in
bulwahn@33250
   158
            (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs))
bulwahn@33250
   159
          end
wenzelm@60781
   160
        val Var (x, _) =
wenzelm@60781
   161
          (the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o
wenzelm@59636
   162
            Logic.dest_implies o Thm.prop_of) @{thm exI}
bulwahn@33250
   163
        fun prove_introrule (index, (ps, introrule)) =
bulwahn@33250
   164
          let
wenzelm@51717
   165
            val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1
wenzelm@59532
   166
              THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1
bulwahn@33250
   167
              THEN (EVERY (map (fn y =>
wenzelm@60752
   168
                resolve_tac ctxt'
wenzelm@60781
   169
                  [infer_instantiate ctxt' [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps))
wenzelm@60752
   170
              THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1)
wenzelm@58963
   171
              THEN TRY (assume_tac ctxt' 1)
bulwahn@33250
   172
          in
wenzelm@33441
   173
            Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac)
bulwahn@33250
   174
          end
bulwahn@33250
   175
      in
bulwahn@33250
   176
        map_index prove_introrule (map mk_introrule disjuncts)
bulwahn@33250
   177
      end
bulwahn@33250
   178
  in maps introrulify' ths' |> Variable.export ctxt' ctxt end
bulwahn@33250
   179
wenzelm@51717
   180
fun rewrite ctxt =
wenzelm@51717
   181
  Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm Ball_def}, @{thm Bex_def}])
wenzelm@51717
   182
  #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}])
wenzelm@51717
   183
  #> Conv.fconv_rule (nnf_conv ctxt)
wenzelm@51717
   184
  #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}])
bulwahn@33250
   185
wenzelm@54895
   186
fun rewrite_intros ctxt =
wenzelm@54895
   187
  Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}])
bulwahn@38952
   188
  #> Simplifier.full_simplify
wenzelm@54895
   189
    (put_simpset HOL_basic_ss ctxt
wenzelm@51717
   190
      addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps})
wenzelm@54895
   191
  #> split_conjuncts_in_assms ctxt
bulwahn@35324
   192
bulwahn@35324
   193
fun print_specs options thy msg ths =
bulwahn@35324
   194
  if show_intermediate_results options then
bulwahn@35324
   195
    (tracing (msg); tracing (commas (map (Display.string_of_thm_global thy) ths)))
bulwahn@35324
   196
  else
bulwahn@35324
   197
    ()
bulwahn@39787
   198
bulwahn@35324
   199
fun preprocess options (constname, specs) thy =
bulwahn@35324
   200
(*  case Predicate_Compile_Data.processed_specs thy constname of
bulwahn@35324
   201
    SOME specss => (specss, thy)
bulwahn@35324
   202
  | NONE =>*)
bulwahn@35324
   203
    let
wenzelm@54742
   204
      val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
bulwahn@33250
   205
      val intros =
bulwahn@35324
   206
        if forall is_pred_equation specs then 
wenzelm@60781
   207
          map (split_conjuncts_in_assms ctxt) (introrulify ctxt (map (rewrite ctxt) specs))
bulwahn@35324
   208
        else if forall (is_intro constname) specs then
wenzelm@54895
   209
          map (rewrite_intros ctxt) specs
bulwahn@35324
   210
        else
bulwahn@35324
   211
          error ("unexpected specification for constant " ^ quote constname ^ ":\n"
bulwahn@35324
   212
            ^ commas (map (quote o Display.string_of_thm_global thy) specs))
bulwahn@37908
   213
      val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
wenzelm@54742
   214
      val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros
bulwahn@35324
   215
      val _ = print_specs options thy "normalized intros" intros
bulwahn@35324
   216
      (*val intros = maps (split_cases thy) intros*)
bulwahn@35324
   217
      val (intros', (local_defs, thy')) = flatten_intros constname intros thy
bulwahn@35324
   218
      val (intross, thy'') = fold_map (preprocess options) local_defs thy'
bulwahn@35324
   219
      val full_spec = (constname, intros') :: flat intross
bulwahn@35324
   220
      (*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*)
bulwahn@35324
   221
    in
bulwahn@35324
   222
      (full_spec, thy'')
bulwahn@35324
   223
    end;
bulwahn@33250
   224
bulwahn@33250
   225
fun flat_higher_order_arguments (intross, thy) =
bulwahn@33250
   226
  let
bulwahn@33250
   227
    fun process constname atom (new_defs, thy) =
bulwahn@33250
   228
      let
bulwahn@33250
   229
        val (pred, args) = strip_comb atom
bulwahn@33250
   230
        fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) =
bulwahn@33250
   231
          let
bulwahn@33250
   232
            val vars = map Var (Term.add_vars abs_arg [])
wenzelm@35845
   233
            val abs_arg' = Logic.unvarify_global abs_arg
bulwahn@33250
   234
            val frees = map Free (Term.add_frees abs_arg' [])
wenzelm@43324
   235
            val constname =
wenzelm@43324
   236
              singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs))
wenzelm@43324
   237
                ((Long_Name.base_name constname) ^ "_hoaux")
bulwahn@33250
   238
            val full_constname = Sign.full_bname thy constname
bulwahn@33250
   239
            val constT = map fastype_of frees ---> (fastype_of abs_arg')
bulwahn@33250
   240
            val const = Const (full_constname, constT)
bulwahn@33250
   241
            val lhs = list_comb (const, frees)
bulwahn@33250
   242
            val def = Logic.mk_equals (lhs, abs_arg')
bulwahn@33250
   243
            val ([definition], thy') = thy
wenzelm@56239
   244
              |> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
wenzelm@46909
   245
              |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])]
bulwahn@33250
   246
          in
wenzelm@35845
   247
            (list_comb (Logic.varify_global const, vars),
wenzelm@35845
   248
              ((full_constname, [definition])::new_defs, thy'))
bulwahn@33250
   249
          end
bulwahn@33403
   250
        | replace_abs_arg arg (new_defs, thy) =
bulwahn@39468
   251
          if is_some (try HOLogic.dest_prodT (fastype_of arg)) then
bulwahn@39468
   252
            (case try HOLogic.dest_prod arg of
bulwahn@39468
   253
              SOME (t1, t2) =>
bulwahn@39468
   254
                (new_defs, thy)
bulwahn@39468
   255
                |> process constname t1 
bulwahn@39468
   256
                ||>> process constname t2
bulwahn@39468
   257
                |>> HOLogic.mk_prod
wenzelm@55437
   258
            | NONE =>
wenzelm@55437
   259
              (warning ("Replacing higher order arguments " ^
wenzelm@55437
   260
                "is not applied in an undestructable product type"); (arg, (new_defs, thy))))
bulwahn@39468
   261
          else if (is_predT (fastype_of arg)) then
bulwahn@33403
   262
            process constname arg (new_defs, thy)
bulwahn@33403
   263
          else
bulwahn@33403
   264
            (arg, (new_defs, thy))
bulwahn@39468
   265
bulwahn@35324
   266
        val (args', (new_defs', thy')) = fold_map replace_abs_arg
bulwahn@35324
   267
          (map Envir.beta_eta_contract args) (new_defs, thy)
bulwahn@33250
   268
      in
bulwahn@33250
   269
        (list_comb (pred, args'), (new_defs', thy'))
bulwahn@33250
   270
      end
bulwahn@33250
   271
    fun flat_intro intro (new_defs, thy) =
bulwahn@33250
   272
      let
bulwahn@33250
   273
        val constname = fst (dest_Const (fst (strip_comb
wenzelm@59582
   274
          (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro))))))
wenzelm@55437
   275
        val (intro_ts, (new_defs, thy)) =
wenzelm@59582
   276
          fold_map_atoms (process constname) (Thm.prop_of intro) (new_defs, thy)
bulwahn@33250
   277
        val th = Skip_Proof.make_thm thy intro_ts
bulwahn@33250
   278
      in
bulwahn@33250
   279
        (th, (new_defs, thy))
bulwahn@33250
   280
      end
bulwahn@33250
   281
    fun fold_map_spec f [] s = ([], s)
bulwahn@33250
   282
      | fold_map_spec f ((c, ths) :: specs) s =
bulwahn@33250
   283
        let
bulwahn@33250
   284
          val (ths', s') = f ths s
bulwahn@33250
   285
          val (specs', s'') = fold_map_spec f specs s'
bulwahn@33250
   286
        in ((c, ths') :: specs', s'') end
bulwahn@33250
   287
    val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy)
bulwahn@33250
   288
  in
bulwahn@33250
   289
    (intross', (new_defs, thy'))
bulwahn@33250
   290
  end
bulwahn@33250
   291
wenzelm@55437
   292
end