src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author haftmann
Tue, 24 Apr 2018 14:17:58 +0000
changeset 68028 1f9f973eed2a
parent 67399 eab6ce8368fa
child 69593 3dda49e08b9d
permissions -rw-r--r--
proper datatype for 8-bit characters
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63764
f3ad26c4b2d9 tuned headers;
wenzelm
parents: 62597
diff changeset
     1
(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
f3ad26c4b2d9 tuned headers;
wenzelm
parents: 62597
diff changeset
     2
    Author:     Lukas Bulwahn, TU Muenchen
f3ad26c4b2d9 tuned headers;
wenzelm
parents: 62597
diff changeset
     3
*)
f3ad26c4b2d9 tuned headers;
wenzelm
parents: 62597
diff changeset
     4
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     5
theory Predicate_Compile_Alternative_Defs
63764
f3ad26c4b2d9 tuned headers;
wenzelm
parents: 62597
diff changeset
     6
  imports Main
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     7
begin
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     8
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
     9
section \<open>Common constants\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    10
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    11
declare HOL.if_bool_eq_disj[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    12
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    13
declare bool_diff_def[code_pred_inline]
46905
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
    14
declare inf_bool_def[abs_def, code_pred_inline]
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
    15
declare less_bool_def[abs_def, code_pred_inline]
6b1c0a80a57a prefer abs_def over def_raw;
wenzelm
parents: 46884
diff changeset
    16
declare le_bool_def[abs_def, code_pred_inline]
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    17
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    18
lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (\<and>)"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45461
diff changeset
    19
by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    20
39650
2a35950ec495 handling equivalences smarter in the predicate compiler
bulwahn
parents: 39302
diff changeset
    21
lemma [code_pred_inline]: 
67091
1393c2340eec more symbols;
wenzelm
parents: 63950
diff changeset
    22
  "((A::bool) \<noteq> (B::bool)) = ((A \<and> \<not> B) \<or> (B \<and> \<not> A))"
39650
2a35950ec495 handling equivalences smarter in the predicate compiler
bulwahn
parents: 39302
diff changeset
    23
by fast
2a35950ec495 handling equivalences smarter in the predicate compiler
bulwahn
parents: 39302
diff changeset
    24
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    25
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Let}]\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    26
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    27
section \<open>Pairs\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    28
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61180
diff changeset
    29
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    30
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    31
section \<open>Filters\<close>
60045
cd2b6debac18 predicate compiler: ignore Abs_filter and Rep_filter
hoelzl
parents: 56679
diff changeset
    32
cd2b6debac18 predicate compiler: ignore Abs_filter and Rep_filter
hoelzl
parents: 56679
diff changeset
    33
(*TODO: shouldn't this be done by typedef? *)
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    34
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}]\<close>
60045
cd2b6debac18 predicate compiler: ignore Abs_filter and Rep_filter
hoelzl
parents: 56679
diff changeset
    35
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    36
section \<open>Bounded quantifiers\<close>
35953
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 Ball_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    39
declare Bex_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    40
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    41
section \<open>Operations on Predicates\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    42
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    43
lemma Diff[code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    44
  "(A - B) = (%x. A x \<and> \<not> B x)"
46884
154dc6ec0041 tuned proofs
noschinl
parents: 45970
diff changeset
    45
  by (simp add: fun_eq_iff)
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    46
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    47
lemma subset_eq[code_pred_inline]:
67091
1393c2340eec more symbols;
wenzelm
parents: 63950
diff changeset
    48
  "(P :: 'a \<Rightarrow> bool) < (Q :: 'a \<Rightarrow> bool) \<equiv> ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall>x. P x \<longrightarrow> Q x))"
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45461
diff changeset
    49
  by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
36253
6e969ce3dfcc added further inlining of boolean constants to the predicate compiler
bulwahn
parents: 36246
diff changeset
    50
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    51
lemma set_equality[code_pred_inline]:
45970
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45461
diff changeset
    52
  "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45461
diff changeset
    53
  by (auto simp add: fun_eq_iff)
b6d0cff57d96 adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents: 45461
diff changeset
    54
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    55
section \<open>Setup for Numerals\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    56
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    57
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close>
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    58
setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close>
62597
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61585
diff changeset
    59
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close>
b3f2b8c906a6 model characters directly as range 0..255
haftmann
parents: 61585
diff changeset
    60
setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    61
63950
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 63764
diff changeset
    62
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name modulo}, @{const_name times}]\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    63
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    64
section \<open>Arithmetic operations\<close>
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
    65
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    66
subsection \<open>Arithmetic on naturals and integers\<close>
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
    67
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
    68
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
    69
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
    70
  "plus_eq_nat x y z = (x + y = z)"
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    71
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
    72
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
    73
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
    74
  "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
    75
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
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
    77
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
    78
  "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
    79
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
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
    81
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
    82
  "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
    83
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
    84
definition subtract
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    85
where
45231
d85a2fdc586c replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents: 44928
diff changeset
    86
  [code_unfold]: "subtract x y = y - x"
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    87
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
    88
setup \<open>
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
    89
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
    90
  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
    91
  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
    92
  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
    93
  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
    94
  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
    95
  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
    96
  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
    97
  val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
40054
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
    98
  val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
    99
  val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
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
   100
  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
   101
    let
45461
130c90bb80b4 using more conventional names for monad plus operations
bulwahn
parents: 45231
diff changeset
   102
      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
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
   103
    in
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41075
diff changeset
   104
      absdummy @{typ nat} (absdummy @{typ nat}
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41075
diff changeset
   105
        (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   106
          (@{term "(>) :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
45461
130c90bb80b4 using more conventional names for monad plus operations
bulwahn
parents: 45231
diff changeset
   107
          Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
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
   108
          Predicate_Compile_Aux.mk_single compfuns
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   109
          (@{term "(-) :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
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
   110
    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
   111
  fun enumerate_addups_nat compfuns (_ : typ) =
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41075
diff changeset
   112
    absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48640
diff changeset
   113
    (absdummy @{typ natural} (@{term "Pair :: nat => nat => nat * nat"} $
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48640
diff changeset
   114
      (@{term "nat_of_natural"} $ Bound 0) $
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   115
      (@{term "(-) :: nat => nat => nat"} $ Bound 1 $ (@{term "nat_of_natural"} $ Bound 0))),
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48640
diff changeset
   116
      @{term "0 :: natural"}, @{term "natural_of_nat"} $ Bound 0))
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
   117
  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
   118
    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
   119
      val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
45461
130c90bb80b4 using more conventional names for monad plus operations
bulwahn
parents: 45231
diff changeset
   120
      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
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
   121
    in
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41075
diff changeset
   122
      absdummy @{typ nat} (absdummy @{typ nat}
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 41075
diff changeset
   123
        (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   124
          (@{term "(=) :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
51143
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48640
diff changeset
   125
          (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "nat_of_natural"},
0a2371e7ced3 two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents: 48640
diff changeset
   126
            @{term "0::natural"}, @{term "natural_of_nat"} $ Bound 1)) $
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   127
            (single_const $ (@{term "(+) :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
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
   128
    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
   129
in
40054
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
   130
  Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
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
   131
    [(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
   132
     (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
   133
  #> 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
   134
       (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
40054
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
   135
  #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
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
   136
       [(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
   137
  #> 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
   138
      (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
40054
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
   139
  #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
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
   140
    [(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
   141
     (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
   142
  #> 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
   143
       (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
40054
cd7b1fa20bce adapting alternative_defs, predicate_compile_quickcheck, examples and code_prolog
bulwahn
parents: 39650
diff changeset
   144
  #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
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
   145
    [(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
   146
     (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
   147
  #> 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
   148
      (@{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
   149
end
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
   150
\<close>
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
   151
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
   152
subsection \<open>Inductive definitions for ordering on naturals\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   153
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   154
inductive less_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   155
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   156
  "less_nat 0 (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   157
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   158
36246
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   159
lemma less_nat[code_pred_inline]:
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   160
  "x < y = less_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   161
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   162
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   163
apply (case_tac y) apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   164
apply (case_tac y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   165
apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   166
apply (induct rule: less_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   167
apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   168
done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   169
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   170
inductive less_eq_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   171
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   172
  "less_eq_nat 0 y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   173
| "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
   174
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   175
lemma [code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   176
"x <= y = less_eq_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   177
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   178
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   179
apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   180
apply (case_tac y) apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   181
apply (induct rule: less_eq_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   182
apply auto done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   183
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
   184
section \<open>Alternative list definitions\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   185
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   186
subsection \<open>Alternative rules for \<open>length\<close>\<close>
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
   187
56679
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   188
definition size_list' :: "'a list => nat"
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   189
where "size_list' = size"
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
   190
56679
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   191
lemma size_list'_simps:
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   192
  "size_list' [] = 0"
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   193
  "size_list' (x # xs) = Suc (size_list' xs)"
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   194
by (auto simp add: size_list'_def)
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
   195
56679
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   196
declare size_list'_simps[code_pred_def]
5545bfdfefcc avoid name shadowing
blanchet
parents: 56073
diff changeset
   197
declare size_list'_def[symmetric, code_pred_inline]
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   198
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   199
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 61424
diff changeset
   200
subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   201
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   202
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   203
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   204
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   205
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
   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] list_all2
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 list_all2
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 -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   213
    apply (case_tac xb)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   214
    apply (case_tac 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
    apply (case_tac xc)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   217
    apply auto
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
61140
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   221
subsection \<open>Alternative rules for membership in lists\<close>
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   222
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   223
declare in_set_member[code_pred_inline]
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   224
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   225
lemma member_intros [code_pred_intro]:
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   226
  "List.member (x#xs) x"
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   227
  "List.member xs x \<Longrightarrow> List.member (y#xs) x"
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   228
by(simp_all add: List.member_def)
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   229
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   230
code_pred List.member
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   231
  by(auto simp add: List.member_def elim: list.set_cases)
78ece168f5b5 reactivate examples with predicate compiler and quickcheck
Andreas Lochbihler
parents: 61125
diff changeset
   232
61180
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   233
code_identifier constant member_i_i
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   234
   \<rightharpoonup> (SML) "List.member_i_i"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   235
  and (OCaml) "List.member_i_i"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   236
  and (Haskell) "List.member_i_i"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   237
  and (Scala) "List.member_i_i"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   238
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   239
code_identifier constant member_i_o
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   240
   \<rightharpoonup> (SML) "List.member_i_o"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   241
  and (OCaml) "List.member_i_o"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   242
  and (Haskell) "List.member_i_o"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   243
  and (Scala) "List.member_i_o"
e4716b792713 avoid module dependency cycles
Andreas Lochbihler
parents: 61140
diff changeset
   244
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
   245
section \<open>Setup for String.literal\<close>
40548
54eb5fd36e5e ignoring the constant STR in the predicate compiler
bulwahn
parents: 40054
diff changeset
   246
68028
1f9f973eed2a proper datatype for 8-bit characters
haftmann
parents: 67399
diff changeset
   247
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\<close>
40548
54eb5fd36e5e ignoring the constant STR in the predicate compiler
bulwahn
parents: 40054
diff changeset
   248
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60352
diff changeset
   249
section \<open>Simplification rules for optimisation\<close>
36246
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 [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
   252
by auto
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   253
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   254
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
   255
by auto
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   256
43fecedff8cf added peephole optimisations to the predicate compiler; added structure Predicate_Compile_Simps for peephole optimisations
bulwahn
parents: 36053
diff changeset
   257
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
   258
unfolding less_nat[symmetric] by auto
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   259
46884
154dc6ec0041 tuned proofs
noschinl
parents: 45970
diff changeset
   260
end