src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author haftmann
Mon, 28 Jun 2010 15:03:07 +0200
changeset 37591 d3daea901123
parent 36253 6e969ce3dfcc
child 39198 f967a16dfcdd
permissions -rw-r--r--
merged constants "split" and "prod_case"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     1
theory Predicate_Compile_Alternative_Defs
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
     2
imports Main
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     3
begin
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     4
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     5
section {* Common constants *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     6
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     7
declare HOL.if_bool_eq_disj[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     8
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
     9
declare bool_diff_def[code_pred_inline]
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    10
declare inf_bool_eq_raw[code_pred_inline]
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    11
declare less_bool_def_raw[code_pred_inline]
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    12
declare le_bool_def_raw[code_pred_inline]
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    13
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    14
lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    15
by (rule eq_reflection) (auto simp add: expand_fun_eq min_def le_bool_def)
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    16
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    17
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    18
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    19
section {* Pairs *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    20
37591
d3daea901123 merged constants "split" and "prod_case"
haftmann
parents: 36253
diff changeset
    21
setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    22
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    23
section {* Bounded quantifiers *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    24
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    25
declare Ball_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    26
declare Bex_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    27
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    28
section {* Set operations *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    29
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    30
declare Collect_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    31
declare mem_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    32
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    33
declare eq_reflection[OF empty_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    34
declare insert_code[code_pred_def]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    35
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    36
declare subset_iff[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    37
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    38
declare Int_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    39
declare eq_reflection[OF Un_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    40
declare eq_reflection[OF UNION_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    41
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    42
lemma Diff[code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    43
  "(A - B) = (%x. A x \<and> \<not> B x)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    44
by (auto simp add: mem_def)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    45
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    46
lemma subset_eq[code_pred_inline]:
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    47
  "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    48
by (rule eq_reflection) (fastsimp simp add: mem_def)
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    49
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    50
lemma set_equality[code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    51
  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    52
by (fastsimp simp add: mem_def)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    53
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    54
section {* Setup for Numerals *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    55
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    56
setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    57
setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    58
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    59
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    60
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    61
section {* Arithmetic operations *}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    62
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    63
subsection {* Arithmetic on naturals and integers *}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    64
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    65
definition plus_eq_nat :: "nat => nat => nat => bool"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    66
where
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    67
  "plus_eq_nat x y z = (x + y = z)"
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    68
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    69
definition minus_eq_nat :: "nat => nat => nat => bool"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    70
where
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    71
  "minus_eq_nat x y z = (x - y = z)"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    72
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    73
definition plus_eq_int :: "int => int => int => bool"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    74
where
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    75
  "plus_eq_int x y z = (x + y = z)"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    76
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    77
definition minus_eq_int :: "int => int => int => bool"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    78
where
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    79
  "minus_eq_int x y z = (x - y = z)"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    80
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    81
definition subtract
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    82
where
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    83
  [code_inline]: "subtract x y = y - x"
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    84
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    85
setup {*
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    86
let
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    87
  val Fun = Predicate_Compile_Aux.Fun
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    88
  val Input = Predicate_Compile_Aux.Input
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    89
  val Output = Predicate_Compile_Aux.Output
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    90
  val Bool = Predicate_Compile_Aux.Bool
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    91
  val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    92
  val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    93
  val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    94
  val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    95
  val plus_nat = Predicate_Compile_Core.functional_compilation @{const_name plus} iio
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    96
  val minus_nat = Predicate_Compile_Core.functional_compilation @{const_name "minus"} iio
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    97
  fun subtract_nat compfuns (_ : typ) =
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    98
    let
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
    99
      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   100
    in
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   101
      absdummy (@{typ nat}, absdummy (@{typ nat},
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   102
        Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   103
          (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   104
          Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   105
          Predicate_Compile_Aux.mk_single compfuns
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   106
          (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   107
    end
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   108
  fun enumerate_addups_nat compfuns (_ : typ) =
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   109
    absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   110
    (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   111
      (@{term "Code_Numeral.nat_of"} $ Bound 0) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   112
      (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   113
      @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   114
  fun enumerate_nats compfuns  (_ : typ) =
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   115
    let
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   116
      val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   117
      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   118
    in
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   119
      absdummy(@{typ nat}, absdummy (@{typ nat},
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   120
        Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   121
          (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   122
          (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   123
            @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   124
            (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   125
    end
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   126
in
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   127
  Predicate_Compile_Core.force_modes_and_compilations @{const_name plus_eq_nat}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   128
    [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   129
     (ooi, (enumerate_addups_nat, false))]
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   130
  #> Predicate_Compile_Fun.add_function_predicate_translation
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   131
       (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   132
  #> Predicate_Compile_Core.force_modes_and_compilations @{const_name minus_eq_nat}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   133
       [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   134
  #> Predicate_Compile_Fun.add_function_predicate_translation
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   135
      (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   136
  #> Predicate_Compile_Core.force_modes_and_functions @{const_name plus_eq_int}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   137
    [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   138
     (oii, (@{const_name subtract}, false))]
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   139
  #> Predicate_Compile_Fun.add_function_predicate_translation
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   140
       (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   141
  #> Predicate_Compile_Core.force_modes_and_functions @{const_name minus_eq_int}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   142
    [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   143
     (ioi, (@{const_name minus}, false))]
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   144
  #> Predicate_Compile_Fun.add_function_predicate_translation
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   145
      (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   146
end
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   147
*}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   148
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   149
subsection {* Inductive definitions for ordering on naturals *}
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   150
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   151
inductive less_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   152
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   153
  "less_nat 0 (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   154
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   155
36246
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   156
lemma less_nat[code_pred_inline]:
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   157
  "x < y = less_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   158
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   159
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   160
apply (case_tac y) apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   161
apply (case_tac y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   162
apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   163
apply (induct rule: less_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   164
apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   165
done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   166
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   167
inductive less_eq_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   168
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   169
  "less_eq_nat 0 y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   170
| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   171
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   172
lemma [code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   173
"x <= y = less_eq_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   174
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   175
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   176
apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   177
apply (case_tac y) apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   178
apply (induct rule: less_eq_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   179
apply auto done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   180
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   181
section {* Alternative list definitions *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   182
36053
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   183
subsection {* Alternative rules for length *}
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   184
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   185
definition size_list :: "'a list => nat"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   186
where "size_list = size"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   187
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   188
lemma size_list_simps:
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   189
  "size_list [] = 0"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   190
  "size_list (x # xs) = Suc (size_list xs)"
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   191
by (auto simp add: size_list_def)
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   192
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   193
declare size_list_simps[code_pred_def]
29e242e9e9a3 adding setup for handling arithmetic of natural numbers and integers precisely and more efficiently in the predicate compiler; changed alternative size_list definition for predicate compiler
bulwahn
parents: 35953
diff changeset
   194
declare size_list_def[symmetric, code_pred_inline]
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   195
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   196
subsection {* Alternative rules for set *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   197
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   198
lemma set_ConsI1 [code_pred_intro]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   199
  "set (x # xs) x"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   200
unfolding mem_def[symmetric, of _ x]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   201
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   202
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   203
lemma set_ConsI2 [code_pred_intro]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   204
  "set xs x ==> set (x' # xs) x" 
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   205
unfolding mem_def[symmetric, of _ x]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   206
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   207
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   208
code_pred [skip_proof] set
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   209
proof -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   210
  case set
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   211
  from this show thesis
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   212
    apply (case_tac xb)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   213
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   214
    unfolding mem_def[symmetric, of _ xc]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   215
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   216
    unfolding mem_def
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   217
    apply fastsimp
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   218
    done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   219
qed
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   220
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   221
subsection {* Alternative rules for list_all2 *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   222
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   223
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   224
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   225
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   226
lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   227
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   228
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   229
code_pred [skip_proof] list_all2
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   230
proof -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   231
  case list_all2
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   232
  from this show thesis
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   233
    apply -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   234
    apply (case_tac xb)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   235
    apply (case_tac xc)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   236
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   237
    apply (case_tac xc)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   238
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   239
    apply fastsimp
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   240
    done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   241
qed
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   242
36246
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   243
section {* Simplification rules for optimisation *}
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   244
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   245
lemma [code_pred_simp]: "\<not> False == True"
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   246
by auto
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   247
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   248
lemma [code_pred_simp]: "\<not> True == False"
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   249
by auto
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   250
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   251
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   252
unfolding less_nat[symmetric] by auto
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   253
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   254
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   255
end