src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
author blanchet
Mon, 04 Nov 2013 17:25:36 +0100
changeset 54247 81ee85f56e2d
parent 54229 ca638d713ff8
child 55379 9701dbc35f86
permissions -rw-r--r--
careful with lists of different lengths
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     1
(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     3
33265
01c9c6dbd890 proper headers;
wenzelm
parents: 33250
diff changeset
     4
Preprocessing functions to predicates.
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     5
*)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     6
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     7
signature PREDICATE_COMPILE_FUN =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
     8
sig
33630
68e058d061f5 removed unnecessary oracle in the predicate compiler
bulwahn
parents: 33522
diff changeset
     9
  val define_predicates : (string * thm list) list -> theory -> (string * thm list) list * theory
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    10
  val rewrite_intro : theory -> thm -> thm list
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    11
  val pred_of_function : theory -> string -> string option
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    12
  val add_function_predicate_translation : (term * term) -> theory -> theory
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    13
end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    14
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    15
structure Predicate_Compile_Fun : PREDICATE_COMPILE_FUN =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    16
struct
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    17
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 33752
diff changeset
    18
open Predicate_Compile_Aux;
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    19
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    20
(* Table from function to inductive predicate *)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    21
structure Fun_Pred = Theory_Data
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    22
(
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    23
  type T = (term * term) Item_Net.T;
38760
wenzelm
parents: 38553
diff changeset
    24
  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    25
  val extend = I;
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    26
  val merge = Item_Net.merge;
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    27
)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    28
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    29
fun lookup thy net t =
36051
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    30
  let
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    31
    val poss_preds = map_filter (fn (f, p) =>
36039
bulwahn
parents: 36035
diff changeset
    32
    SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p)
36051
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    33
    handle Pattern.MATCH => NONE) (Item_Net.retrieve net t)
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    34
  in
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    35
    case poss_preds of
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    36
      [p] => SOME p
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    37
    | _ => NONE
810357220388 improving lookup function to handle overloaded constants more correctly in the function flattening of the predicate compiler
bulwahn
parents: 36039
diff changeset
    38
  end
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    39
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    40
fun pred_of_function thy name =
49323
6dff6b1f5417 standardized ML aliases;
wenzelm
parents: 46219
diff changeset
    41
  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    42
    [] => NONE
50056
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
    43
  | [(_, p)] => SOME (fst (dest_Const p))
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    44
  | _ => error ("Multiple matches possible for lookup of constant " ^ name)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    45
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    46
fun defined_const thy name = is_some (pred_of_function thy name)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    47
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    48
fun add_function_predicate_translation (f, p) =
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    49
  Fun_Pred.map (Item_Net.update (f, p))
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    50
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    51
fun transform_ho_typ (T as Type ("fun", _)) =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    52
  let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    53
    val (Ts, T') = strip_type T
38553
56965d8e4e11 use HOLogic.boolT and @{typ bool} more pervasively
haftmann
parents: 37591
diff changeset
    54
  in if T' = HOLogic.boolT then T else (Ts @ [T']) ---> HOLogic.boolT end
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    55
| transform_ho_typ t = t
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    56
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    57
fun transform_ho_arg arg = 
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    58
  case (fastype_of arg) of
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    59
    (T as Type ("fun", _)) =>
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    60
      (case arg of
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    61
        Free (name, _) => Free (name, transform_ho_typ T)
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
    62
      | _ => raise Fail "A non-variable term at a higher-order position")
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
    63
  | _ => arg
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    64
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    65
fun pred_type T =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    66
  let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    67
    val (Ts, T') = strip_type T
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    68
    val Ts' = map transform_ho_typ Ts
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    69
  in
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    70
    (Ts' @ [T']) ---> HOLogic.boolT
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    71
  end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    72
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    73
(* creates the list of premises for every intro rule *)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    74
(* theory -> term -> (string list, term list list) *)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    75
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    76
fun dest_code_eqn eqn = let
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35411
diff changeset
    77
  val (lhs, rhs) = Logic.dest_equals (Logic.unvarify_global (Thm.prop_of eqn))
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    78
  val (func, args) = strip_comb lhs
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    79
in ((func, args), rhs) end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    80
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    81
fun folds_map f xs y =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    82
  let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    83
    fun folds_map' acc [] y = [(rev acc, y)]
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    84
      | folds_map' acc (x :: xs) y =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    85
        maps (fn (x, y) => folds_map' (x :: acc) xs y) (f x y)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    86
    in
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    87
      folds_map' [] xs y
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    88
    end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
    89
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    90
fun keep_functions thy t =
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    91
  case try dest_Const (fst (strip_comb t)) of
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    92
    SOME (c, _) => Predicate_Compile_Data.keep_function thy c
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    93
  | _ => false
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
    94
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
    95
fun flatten thy lookup_pred t (names, prems) =
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
    96
  let
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
    97
    fun lift t (names, prems) =
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
    98
      case lookup_pred (Envir.eta_contract t) of
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
    99
        SOME pred => [(pred, (names, prems))]
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   100
      | NONE =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   101
        let
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   102
          val (vars, body) = strip_abs t
42816
ba14eafef077 eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents: 42361
diff changeset
   103
          val _ = @{assert} (fastype_of body = body_type (fastype_of body))
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   104
          val absnames = Name.variant_list names (map fst vars)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   105
          val frees = map2 (curry Free) absnames (map snd vars)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   106
          val body' = subst_bounds (rev frees, body)
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42816
diff changeset
   107
          val resname = singleton (Name.variant_list (absnames @ names)) "res"
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   108
          val resvar = Free (resname, fastype_of body)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   109
          val t = flatten' body' ([], [])
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   110
            |> map (fn (res, (inner_names, inner_prems)) =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   111
              let
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   112
                fun mk_exists (x, T) t = HOLogic.mk_exists (x, T, t)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   113
                val vTs = 
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   114
                  fold Term.add_frees inner_prems []
50056
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
   115
                  |> filter (fn (x, _) => member (op =) inner_names x)
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   116
                val t = 
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   117
                  fold mk_exists vTs
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   118
                  (foldr1 HOLogic.mk_conj (HOLogic.mk_eq (res, resvar) ::
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   119
                    map HOLogic.dest_Trueprop inner_prems))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   120
              in
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   121
                t
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   122
              end)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   123
              |> foldr1 HOLogic.mk_disj
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   124
              |> fold lambda (resvar :: rev frees)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   125
        in
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   126
          [(t, (names, prems))]
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   127
        end
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   128
    and flatten_or_lift (t, T) (names, prems) =
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   129
      if fastype_of t = T then
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   130
        flatten' t (names, prems)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   131
      else
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   132
        (* note pred_type might be to general! *)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   133
        if (pred_type (fastype_of t) = T) then
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   134
          lift t (names, prems)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   135
        else
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   136
          error ("unexpected input for flatten or lift" ^ Syntax.string_of_term_global thy t ^
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   137
          ", " ^  Syntax.string_of_typ_global thy T)
50056
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
   138
    and flatten' (t as Const _) (names, prems) = [(t, (names, prems))]
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
   139
      | flatten' (t as Free _) (names, prems) = [(t, (names, prems))]
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   140
      | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))]
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   141
      | flatten' (t as _ $ _) (names, prems) =
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   142
      if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   143
        [(t, (names, prems))]
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   144
      else
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   145
        case (fst (strip_comb t)) of
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   146
          Const (@{const_name "If"}, _) =>
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   147
            (let
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   148
              val (_, [B, x, y]) = strip_comb t
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   149
            in
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   150
              flatten' B (names, prems)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   151
              |> maps (fn (B', (names, prems)) =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   152
                (flatten' x (names, prems)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   153
                |> map (fn (res, (names, prems)) => (res, (names, (HOLogic.mk_Trueprop B') :: prems))))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   154
                @ (flatten' y (names, prems)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   155
                |> map (fn (res, (names, prems)) =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   156
                  (* in general unsound! *)
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   157
                  (res, (names, (HOLogic.mk_Trueprop (HOLogic.mk_not B')) :: prems)))))
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   158
            end)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   159
        | Const (@{const_name "Let"}, _) => 
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   160
            (let
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   161
              val (_, [f, g]) = strip_comb t
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   162
            in
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   163
              flatten' f (names, prems)
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   164
              |> maps (fn (res, (names, prems)) =>
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   165
                flatten' (betapply (g, res)) (names, prems))
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   166
            end)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   167
        | _ =>
36029
a790b94e090c removing fishing for split thm in the predicate compiler
bulwahn
parents: 35878
diff changeset
   168
        case find_split_thm thy (fst (strip_comb t)) of
a790b94e090c removing fishing for split thm in the predicate compiler
bulwahn
parents: 35878
diff changeset
   169
          SOME raw_split_thm =>
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   170
          let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 40843
diff changeset
   171
            val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm
36029
a790b94e090c removing fishing for split thm in the predicate compiler
bulwahn
parents: 35878
diff changeset
   172
            val (assms, concl) = Logic.strip_horn (prop_of split_thm)
50056
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
   173
            val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
39802
7cadad6a18cc applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
bulwahn
parents: 39797
diff changeset
   174
            val t' = case_betapply thy t
7cadad6a18cc applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
bulwahn
parents: 39797
diff changeset
   175
            val subst = Pattern.match thy (split_t, t') (Vartab.empty, Vartab.empty)
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   176
            fun flatten_of_assm assm =
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   177
              let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   178
                val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   179
                val var_names = Name.variant_list names (map fst vTs)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   180
                val vars = map Free (var_names ~~ (map snd vTs))
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   181
                val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm'))
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   182
                val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   183
                val (lhss : term list, rhss) =
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   184
                  split_list (map (HOLogic.dest_eq o HOLogic.dest_Trueprop) prems')
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   185
              in
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   186
                folds_map flatten' lhss (var_names @ names, prems)
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   187
                |> map (fn (ress, (names, prems)) =>
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   188
                  let
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   189
                    val prems' = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (ress ~~ rhss)
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   190
                  in (names, prems' @ prems) end)
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   191
                |> maps (flatten' inner_t)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   192
              end
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   193
          in
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   194
            maps flatten_of_assm assms
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   195
          end
36029
a790b94e090c removing fishing for split thm in the predicate compiler
bulwahn
parents: 35878
diff changeset
   196
      | NONE =>
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   197
          let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   198
            val (f, args) = strip_comb t
52131
366fa32ee2a3 tuned signature;
wenzelm
parents: 51317
diff changeset
   199
            val args = map (Envir.eta_long []) args
42816
ba14eafef077 eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents: 42361
diff changeset
   200
            val _ = @{assert} (fastype_of t = body_type (fastype_of t))
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   201
            val f' = lookup_pred f
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   202
            val Ts = case f' of
35873
d09a58c890e3 simplifying function flattening
bulwahn
parents: 35845
diff changeset
   203
              SOME pred => (fst (split_last (binder_types (fastype_of pred))))
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   204
            | NONE => binder_types (fastype_of f)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   205
          in
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   206
            folds_map flatten_or_lift (args ~~ Ts) (names, prems) |>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   207
            (case f' of
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   208
              NONE =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   209
                map (fn (argvs, (names', prems')) => (list_comb (f, argvs), (names', prems')))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   210
            | SOME pred =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   211
                map (fn (argvs, (names', prems')) =>
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   212
                  let
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   213
                    fun lift_arg T t =
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   214
                      if (fastype_of t) = T then t
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   215
                      else
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   216
                        let
42816
ba14eafef077 eliminated obsolete "assert" function, including divergent (unused!?) clone in Predicate_Compile_Proof;
wenzelm
parents: 42361
diff changeset
   217
                          val _ = @{assert} (T =
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   218
                            (binder_types (fastype_of t) @ [@{typ bool}] ---> @{typ bool}))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   219
                          fun mk_if T (b, t, e) =
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   220
                            Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ b $ t $ e
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   221
                          val Ts = binder_types (fastype_of t)
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   222
                        in
46219
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 43326
diff changeset
   223
                          fold_rev Term.abs (map (pair "x") Ts @ [("b", @{typ bool})])
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 43326
diff changeset
   224
                            (mk_if @{typ bool} (list_comb (t, map Bound (length Ts downto 1)),
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 43326
diff changeset
   225
                              HOLogic.mk_eq (@{term True}, Bound 0),
426ed18eba43 discontinued old-style Term.list_abs in favour of plain Term.abs;
wenzelm
parents: 43326
diff changeset
   226
                              HOLogic.mk_eq (@{term False}, Bound 0)))
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   227
                        end
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   228
                    val argvs' = map2 lift_arg Ts argvs
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 42816
diff changeset
   229
                    val resname = singleton (Name.variant_list names') "res"
35875
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   230
                    val resvar = Free (resname, body_type (fastype_of t))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   231
                    val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs' @ [resvar]))
b0d24a74b06b restructuring function flattening
bulwahn
parents: 35874
diff changeset
   232
                  in (resvar, (resname :: names', prem :: prems')) end))
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   233
          end
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   234
  in
52131
366fa32ee2a3 tuned signature;
wenzelm
parents: 51317
diff changeset
   235
    map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   236
  end;
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   237
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   238
(* FIXME: create new predicate name -- does not avoid nameclashing *)
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   239
fun pred_of thy f =
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   240
  let
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   241
    val (name, T) = dest_Const f
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   242
    val base_name' = (Long_Name.base_name name ^ "P")
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   243
    val name' = Sign.full_bname thy base_name'
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   244
    val T' = if (body_type T = @{typ bool}) then T else pred_type T
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   245
  in
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   246
    (name', Const (name', T'))
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   247
  end
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   248
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   249
(* assumption: mutual recursive predicates all have the same parameters. *)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   250
fun define_predicates specs thy =
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   251
  if forall (fn (const, _) => defined_const thy const) specs then
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   252
    ([], thy)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   253
  else
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   254
    let
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   255
      val eqns = maps snd specs
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   256
      (* create prednames *)
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   257
      val ((funs, argss), rhss) = map_split dest_code_eqn eqns |>> split_list
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   258
      val dst_funs = distinct (op =) funs
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   259
      val argss' = map (map transform_ho_arg) argss
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   260
      fun is_lifted (t1, t2) = (fastype_of t2 = pred_type (fastype_of t1))
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   261
      (* FIXME: higher order arguments also occur in tuples! *)
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   262
      val lifted_args = distinct (op =) (filter is_lifted (flat argss ~~ flat argss'))
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   263
      val (prednames, preds) = split_list (map (pred_of thy) funs)
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   264
      val dst_preds = distinct (op =) preds
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   265
      val dst_prednames = distinct (op =) prednames
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   266
      (* mapping from term (Free or Const) to term *)
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   267
      val net = fold Item_Net.update
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   268
        ((dst_funs ~~ dst_preds) @ lifted_args)
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   269
          (Fun_Pred.get thy)
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   270
      fun lookup_pred t = lookup thy net t
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   271
      (* create intro rules *)
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   272
      fun mk_intros ((func, pred), (args, rhs)) =
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   273
        if (body_type (fastype_of func) = @{typ bool}) then
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   274
         (* TODO: preprocess predicate definition of rhs *)
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   275
          [Logic.list_implies ([HOLogic.mk_Trueprop rhs], HOLogic.mk_Trueprop (list_comb (pred, args)))]
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   276
        else
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   277
          let
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   278
            val names = Term.add_free_names rhs []
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   279
          in flatten thy lookup_pred rhs (names, [])
50056
72efd6b4038d dropped dead code
haftmann
parents: 49323
diff changeset
   280
            |> map (fn (resultt, (_, prems)) =>
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   281
              Logic.list_implies (prems, HOLogic.mk_Trueprop (list_comb (pred, args @ [resultt]))))
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   282
          end
54247
81ee85f56e2d careful with lists of different lengths
blanchet
parents: 54229
diff changeset
   283
      val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss))
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   284
      val (intrs, thy') = thy
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   285
        |> Sign.add_consts_i
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   286
          (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn))
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   287
           dst_preds)
51317
0e70cc4e94e8 provide explicit dummy names (cf. dfe469293eb4);
wenzelm
parents: 50056
diff changeset
   288
        |> fold_map Specification.axiom
54229
ca638d713ff8 generate stable names for axioms
blanchet
parents: 52131
diff changeset
   289
            (map_index (fn (j, (predname, t)) =>
ca638d713ff8 generate stable names for axioms
blanchet
parents: 52131
diff changeset
   290
                ((Binding.name (Long_Name.base_name predname ^ "_intro_" ^ string_of_int (j + 1)), []), t))
54247
81ee85f56e2d careful with lists of different lengths
blanchet
parents: 54229
diff changeset
   291
              (maps (uncurry (map o pair)) (prednames ~~ intr_tss)))
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   292
      val specs = map (fn predname => (predname,
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   293
          map Drule.export_without_context (filter (Predicate_Compile_Aux.is_intro predname) intrs)))
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   294
        dst_prednames
35878
74a74828d682 cleaning the function flattening
bulwahn
parents: 35877
diff changeset
   295
      val thy'' = Fun_Pred.map
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   296
        (fold Item_Net.update (map (pairself Logic.varify_global)
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   297
          (dst_funs ~~ dst_preds))) thy'
36035
d82682936c52 adding registration of functions in the function flattening
bulwahn
parents: 36029
diff changeset
   298
      fun functional_mode_of T =
d82682936c52 adding registration of functions in the function flattening
bulwahn
parents: 36029
diff changeset
   299
        list_fun_mode (replicate (length (binder_types T)) Input @ [Output])
d82682936c52 adding registration of functions in the function flattening
bulwahn
parents: 36029
diff changeset
   300
      val thy''' = fold
40053
3fa49ea76cbb using a signature in core_data and moving some more functions to core_data
bulwahn
parents: 39802
diff changeset
   301
        (fn (predname, Const (name, T)) => Core_Data.register_alternative_function
36035
d82682936c52 adding registration of functions in the function flattening
bulwahn
parents: 36029
diff changeset
   302
          predname (functional_mode_of T) name)
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   303
      (dst_prednames ~~ dst_funs) thy''
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   304
    in
36035
d82682936c52 adding registration of functions in the function flattening
bulwahn
parents: 36029
diff changeset
   305
      (specs, thy''')
35876
ac44e2312f0a only adding lifted arguments to item net in the function flattening; correcting indentation; removing dead code
bulwahn
parents: 35875
diff changeset
   306
    end
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   307
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   308
fun rewrite_intro thy intro =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   309
  let
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   310
    fun lookup_pred t = lookup thy (Fun_Pred.get thy) t
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   311
    (*val _ = tracing ("Rewriting intro " ^ Display.string_of_thm_global thy intro)*)
35845
e5980f0ad025 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents: 35411
diff changeset
   312
    val intro_t = Logic.unvarify_global (prop_of intro)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   313
    val (prems, concl) = Logic.strip_horn intro_t
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   314
    val frees = map fst (Term.add_frees intro_t [])
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   315
    fun rewrite prem names =
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   316
      let
35324
c9f428269b38 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
bulwahn
parents: 35021
diff changeset
   317
        (*val _ = tracing ("Rewriting premise " ^ Syntax.string_of_term_global thy prem ^ "...")*)
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   318
        val t = HOLogic.dest_Trueprop prem
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   319
        val (lit, mk_lit) = case try HOLogic.dest_not t of
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   320
            SOME t => (t, HOLogic.mk_not)
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   321
          | NONE => (t, I)
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   322
        val (P, args) = strip_comb lit
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   323
      in
35874
bcfa6b4b21c6 renaming mk_prems to flatten in the function flattening
bulwahn
parents: 35873
diff changeset
   324
        folds_map (flatten thy lookup_pred) args (names, [])
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   325
        |> map (fn (resargs, (names', prems')) =>
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   326
          let
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   327
            val prem' = HOLogic.mk_Trueprop (mk_lit (list_comb (P, resargs)))
38954
80ce658600b0 changing order of premises generated when flattening functions in premises; adapting example for second attack for hotel key card system
bulwahn
parents: 38760
diff changeset
   328
          in (prems' @ [prem'], names') end)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   329
      end
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   330
    val intro_ts' = folds_map rewrite prems frees
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   331
      |> maps (fn (prems', frees') =>
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   332
        rewrite concl frees'
38956
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   333
        |> map (fn (conclprems, _) =>
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   334
          let
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   335
            val (conclprems', concl') = split_last conclprems
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   336
          in
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   337
            Logic.list_implies ((flat prems') @ conclprems', concl')
2e5bf3bc7361 renaming
bulwahn
parents: 38954
diff changeset
   338
          end))
36249
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   339
    (*val _ = tracing ("Rewritten intro to " ^
24f2ab79b506 replaced call to inductive package by axiomatization in the function flattening of the predicate compiler
bulwahn
parents: 36051
diff changeset
   340
      commas (map (Syntax.string_of_term_global thy) intro_ts'))*)
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   341
  in
35021
c839a4c670c6 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
wenzelm
parents: 34954
diff changeset
   342
    map (Drule.export_without_context o Skip_Proof.make_thm thy) intro_ts'
33630
68e058d061f5 removed unnecessary oracle in the predicate compiler
bulwahn
parents: 33522
diff changeset
   343
  end
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   344
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
diff changeset
   345
end;