src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
author bulwahn
Tue Oct 27 09:03:56 2009 +0100 (2009-10-27)
changeset 33251 4b13ab778b78
parent 33250 5c2af18a3237
child 33265 01c9c6dbd890
permissions -rw-r--r--
added option show_modes to predicate compiler
bulwahn@33250
     1
(* Author: Lukas Bulwahn, TU Muenchen
bulwahn@33250
     2
bulwahn@33250
     3
Auxilary functions for predicate compiler
bulwahn@33250
     4
*)
bulwahn@33250
     5
bulwahn@33250
     6
structure Predicate_Compile_Aux =
bulwahn@33250
     7
struct
bulwahn@33250
     8
bulwahn@33250
     9
(* general syntactic functions *)
bulwahn@33250
    10
bulwahn@33250
    11
(*Like dest_conj, but flattens conjunctions however nested*)
bulwahn@33250
    12
fun conjuncts_aux (Const ("op &", _) $ t $ t') conjs = conjuncts_aux t (conjuncts_aux t' conjs)
bulwahn@33250
    13
  | conjuncts_aux t conjs = t::conjs;
bulwahn@33250
    14
bulwahn@33250
    15
fun conjuncts t = conjuncts_aux t [];
bulwahn@33250
    16
bulwahn@33250
    17
(* syntactic functions *)
bulwahn@33250
    18
bulwahn@33250
    19
fun is_equationlike_term (Const ("==", _) $ _ $ _) = true
bulwahn@33250
    20
  | is_equationlike_term (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ _)) = true
bulwahn@33250
    21
  | is_equationlike_term _ = false
bulwahn@33250
    22
  
bulwahn@33250
    23
val is_equationlike = is_equationlike_term o prop_of 
bulwahn@33250
    24
bulwahn@33250
    25
fun is_pred_equation_term (Const ("==", _) $ u $ v) =
bulwahn@33250
    26
  (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
bulwahn@33250
    27
  | is_pred_equation_term _ = false
bulwahn@33250
    28
  
bulwahn@33250
    29
val is_pred_equation = is_pred_equation_term o prop_of 
bulwahn@33250
    30
bulwahn@33250
    31
fun is_intro_term constname t =
bulwahn@33250
    32
  case fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl t))) of
bulwahn@33250
    33
    Const (c, _) => c = constname
bulwahn@33250
    34
  | _ => false
bulwahn@33250
    35
  
bulwahn@33250
    36
fun is_intro constname t = is_intro_term constname (prop_of t)
bulwahn@33250
    37
bulwahn@33250
    38
fun is_pred thy constname =
bulwahn@33250
    39
  let
bulwahn@33250
    40
    val T = (Sign.the_const_type thy constname)
bulwahn@33250
    41
  in body_type T = @{typ "bool"} end;
bulwahn@33250
    42
  
bulwahn@33250
    43
bulwahn@33250
    44
fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = HOLogic.boolT)
bulwahn@33250
    45
  | is_predT _ = false
bulwahn@33250
    46
bulwahn@33250
    47
  
bulwahn@33250
    48
(*** check if a term contains only constructor functions ***)
bulwahn@33250
    49
fun is_constrt thy =
bulwahn@33250
    50
  let
bulwahn@33250
    51
    val cnstrs = flat (maps
bulwahn@33250
    52
      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
bulwahn@33250
    53
      (Symtab.dest (Datatype.get_all thy)));
bulwahn@33250
    54
    fun check t = (case strip_comb t of
bulwahn@33250
    55
        (Free _, []) => true
bulwahn@33250
    56
      | (Const (s, T), ts) => (case (AList.lookup (op =) cnstrs s, body_type T) of
bulwahn@33250
    57
            (SOME (i, Tname), Type (Tname', _)) => length ts = i andalso Tname = Tname' andalso forall check ts
bulwahn@33250
    58
          | _ => false)
bulwahn@33250
    59
      | _ => false)
bulwahn@33250
    60
  in check end;  
bulwahn@33250
    61
  
bulwahn@33250
    62
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
bulwahn@33250
    63
  let
bulwahn@33250
    64
    val (xTs, t') = strip_ex t
bulwahn@33250
    65
  in
bulwahn@33250
    66
    ((x, T) :: xTs, t')
bulwahn@33250
    67
  end
bulwahn@33250
    68
  | strip_ex t = ([], t)
bulwahn@33250
    69
bulwahn@33250
    70
fun focus_ex t nctxt =
bulwahn@33250
    71
  let
bulwahn@33250
    72
    val ((xs, Ts), t') = apfst split_list (strip_ex t) 
bulwahn@33250
    73
    val (xs', nctxt') = Name.variants xs nctxt;
bulwahn@33250
    74
    val ps' = xs' ~~ Ts;
bulwahn@33250
    75
    val vs = map Free ps';
bulwahn@33250
    76
    val t'' = Term.subst_bounds (rev vs, t');
bulwahn@33250
    77
  in ((ps', t''), nctxt') end;
bulwahn@33250
    78
bulwahn@33250
    79
bulwahn@33250
    80
(* introduction rule combinators *)
bulwahn@33250
    81
bulwahn@33250
    82
(* combinators to apply a function to all literals of an introduction rules *)
bulwahn@33250
    83
bulwahn@33250
    84
fun map_atoms f intro = 
bulwahn@33250
    85
  let
bulwahn@33250
    86
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
    87
    fun appl t = (case t of
bulwahn@33250
    88
        (@{term "Not"} $ t') => HOLogic.mk_not (f t')
bulwahn@33250
    89
      | _ => f t)
bulwahn@33250
    90
  in
bulwahn@33250
    91
    Logic.list_implies
bulwahn@33250
    92
      (map (HOLogic.mk_Trueprop o appl o HOLogic.dest_Trueprop) literals, head)
bulwahn@33250
    93
  end
bulwahn@33250
    94
bulwahn@33250
    95
fun fold_atoms f intro s =
bulwahn@33250
    96
  let
bulwahn@33250
    97
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
    98
    fun appl t s = (case t of
bulwahn@33250
    99
      (@{term "Not"} $ t') => f t' s
bulwahn@33250
   100
      | _ => f t s)
bulwahn@33250
   101
  in fold appl (map HOLogic.dest_Trueprop literals) s end
bulwahn@33250
   102
bulwahn@33250
   103
fun fold_map_atoms f intro s =
bulwahn@33250
   104
  let
bulwahn@33250
   105
    val (literals, head) = Logic.strip_horn intro
bulwahn@33250
   106
    fun appl t s = (case t of
bulwahn@33250
   107
      (@{term "Not"} $ t') => apfst HOLogic.mk_not (f t' s)
bulwahn@33250
   108
      | _ => f t s)
bulwahn@33250
   109
    val (literals', s') = fold_map appl (map HOLogic.dest_Trueprop literals) s
bulwahn@33250
   110
  in
bulwahn@33250
   111
    (Logic.list_implies (map HOLogic.mk_Trueprop literals', head), s')
bulwahn@33250
   112
  end;
bulwahn@33250
   113
bulwahn@33250
   114
fun maps_premises f intro =
bulwahn@33250
   115
  let
bulwahn@33250
   116
    val (premises, head) = Logic.strip_horn intro
bulwahn@33250
   117
  in
bulwahn@33250
   118
    Logic.list_implies (maps f premises, head)
bulwahn@33250
   119
  end
bulwahn@33250
   120
  
bulwahn@33250
   121
(* lifting term operations to theorems *)
bulwahn@33250
   122
bulwahn@33250
   123
fun map_term thy f th =
bulwahn@33250
   124
  Skip_Proof.make_thm thy (f (prop_of th))
bulwahn@33250
   125
bulwahn@33250
   126
(*
bulwahn@33250
   127
fun equals_conv lhs_cv rhs_cv ct =
bulwahn@33250
   128
  case Thm.term_of ct of
bulwahn@33250
   129
    Const ("==", _) $ _ $ _ => Conv.arg_conv cv ct  
bulwahn@33250
   130
  | _ => error "equals_conv"  
bulwahn@33250
   131
*)
bulwahn@33250
   132
bulwahn@33250
   133
(* Different options for compiler *)
bulwahn@33250
   134
bulwahn@33250
   135
datatype options = Options of {  
bulwahn@33250
   136
  expected_modes : (string * int list list) option,
bulwahn@33250
   137
  show_steps : bool,
bulwahn@33250
   138
  show_proof_trace : bool,
bulwahn@33250
   139
  show_intermediate_results : bool,
bulwahn@33251
   140
  show_mode_inference : bool,
bulwahn@33251
   141
  show_modes : bool,
bulwahn@33250
   142
  show_compilation : bool,
bulwahn@33250
   143
  skip_proof : bool,
bulwahn@33250
   144
bulwahn@33250
   145
  inductify : bool,
bulwahn@33250
   146
  rpred : bool,
bulwahn@33250
   147
  depth_limited : bool
bulwahn@33250
   148
};
bulwahn@33250
   149
bulwahn@33250
   150
fun expected_modes (Options opt) = #expected_modes opt
bulwahn@33250
   151
fun show_steps (Options opt) = #show_steps opt
bulwahn@33250
   152
fun show_intermediate_results (Options opt) = #show_intermediate_results opt
bulwahn@33250
   153
fun show_proof_trace (Options opt) = #show_proof_trace opt
bulwahn@33251
   154
fun show_modes (Options opt) = #show_modes opt
bulwahn@33251
   155
fun show_mode_inference (Options opt) = #show_mode_inference opt
bulwahn@33250
   156
fun show_compilation (Options opt) = #show_compilation opt
bulwahn@33250
   157
fun skip_proof (Options opt) = #skip_proof opt
bulwahn@33250
   158
bulwahn@33250
   159
fun is_inductify (Options opt) = #inductify opt
bulwahn@33250
   160
fun is_rpred (Options opt) = #rpred opt
bulwahn@33250
   161
fun is_depth_limited (Options opt) = #depth_limited opt
bulwahn@33250
   162
bulwahn@33250
   163
val default_options = Options {
bulwahn@33250
   164
  expected_modes = NONE,
bulwahn@33250
   165
  show_steps = false,
bulwahn@33250
   166
  show_intermediate_results = false,
bulwahn@33250
   167
  show_proof_trace = false,
bulwahn@33251
   168
  show_modes = false,
bulwahn@33250
   169
  show_mode_inference = false,
bulwahn@33250
   170
  show_compilation = false,
bulwahn@33250
   171
  skip_proof = false,
bulwahn@33250
   172
  
bulwahn@33250
   173
  inductify = false,
bulwahn@33250
   174
  rpred = false,
bulwahn@33250
   175
  depth_limited = false
bulwahn@33250
   176
}
bulwahn@33250
   177
bulwahn@33250
   178
bulwahn@33250
   179
fun print_step options s =
bulwahn@33250
   180
  if show_steps options then tracing s else ()
bulwahn@33250
   181
bulwahn@33250
   182
(* tuple processing *)
bulwahn@33250
   183
bulwahn@33250
   184
fun expand_tuples thy intro =
bulwahn@33250
   185
  let
bulwahn@33250
   186
    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
bulwahn@33250
   187
      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
bulwahn@33250
   188
      (case HOLogic.strip_tupleT (fastype_of arg) of
bulwahn@33250
   189
        (Ts as _ :: _ :: _) =>
bulwahn@33250
   190
        let
bulwahn@33250
   191
          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
bulwahn@33250
   192
            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
bulwahn@33250
   193
            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
bulwahn@33250
   194
              let
bulwahn@33250
   195
                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
bulwahn@33250
   196
                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
bulwahn@33250
   197
                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
bulwahn@33250
   198
                val args' = map (Pattern.rewrite_term thy [pat] []) args
bulwahn@33250
   199
              in
bulwahn@33250
   200
                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
bulwahn@33250
   201
              end
bulwahn@33250
   202
            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
bulwahn@33250
   203
          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
bulwahn@33250
   204
            (args, (pats, intro_t, ctxt))
bulwahn@33250
   205
        in
bulwahn@33250
   206
          rewrite_args args' (pats, intro_t', ctxt')
bulwahn@33250
   207
        end
bulwahn@33250
   208
      | _ => rewrite_args args (pats, intro_t, ctxt))
bulwahn@33250
   209
    fun rewrite_prem atom =
bulwahn@33250
   210
      let
bulwahn@33250
   211
        val (_, args) = strip_comb atom
bulwahn@33250
   212
      in rewrite_args args end
bulwahn@33250
   213
    val ctxt = ProofContext.init thy
bulwahn@33250
   214
    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
bulwahn@33250
   215
    val intro_t = prop_of intro'
bulwahn@33250
   216
    val concl = Logic.strip_imp_concl intro_t
bulwahn@33250
   217
    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
bulwahn@33250
   218
    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
bulwahn@33250
   219
    val (pats', intro_t', ctxt3) = 
bulwahn@33250
   220
      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
bulwahn@33250
   221
    fun rewrite_pat (ct1, ct2) =
bulwahn@33250
   222
      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
bulwahn@33250
   223
    val t_insts' = map rewrite_pat t_insts
bulwahn@33250
   224
    val intro'' = Thm.instantiate (T_insts, t_insts') intro
bulwahn@33250
   225
    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
bulwahn@33250
   226
    val intro'''' = Simplifier.full_simplify
bulwahn@33250
   227
      (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
bulwahn@33250
   228
      intro'''
bulwahn@33250
   229
    (* splitting conjunctions introduced by Pair_eq*)
bulwahn@33250
   230
    fun split_conj prem =
bulwahn@33250
   231
      map HOLogic.mk_Trueprop (conjuncts (HOLogic.dest_Trueprop prem))
bulwahn@33250
   232
    val intro''''' = map_term thy (maps_premises split_conj) intro''''
bulwahn@33250
   233
  in
bulwahn@33250
   234
    intro'''''
bulwahn@33250
   235
  end
bulwahn@33250
   236
bulwahn@33250
   237
bulwahn@33250
   238
bulwahn@33250
   239
end;