author | haftmann |
Tue, 24 Apr 2018 14:17:58 +0000 | |
changeset 68028 | 1f9f973eed2a |
parent 67399 | eab6ce8368fa |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
63764 | 1 |
(* Title: HOL/Library/Predicate_Compile_Alternative_Defs.thy |
2 |
Author: Lukas Bulwahn, TU Muenchen |
|
3 |
*) |
|
4 |
||
35953 | 5 |
theory Predicate_Compile_Alternative_Defs |
63764 | 6 |
imports Main |
35953 | 7 |
begin |
8 |
||
60500 | 9 |
section \<open>Common constants\<close> |
35953 | 10 |
|
11 |
declare HOL.if_bool_eq_disj[code_pred_inline] |
|
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 | 14 |
declare inf_bool_def[abs_def, code_pred_inline] |
15 |
declare less_bool_def[abs_def, code_pred_inline] |
|
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 | 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 | 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 | 25 |
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Let}]\<close> |
35953 | 26 |
|
60500 | 27 |
section \<open>Pairs\<close> |
35953 | 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 | 30 |
|
60500 | 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 | 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 | 36 |
section \<open>Bounded quantifiers\<close> |
35953 | 37 |
|
38 |
declare Ball_def[code_pred_inline] |
|
39 |
declare Bex_def[code_pred_inline] |
|
40 |
||
60500 | 41 |
section \<open>Operations on Predicates\<close> |
35953 | 42 |
|
43 |
lemma Diff[code_pred_inline]: |
|
44 |
"(A - B) = (%x. A x \<and> \<not> B x)" |
|
46884 | 45 |
by (simp add: fun_eq_iff) |
35953 | 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 | 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 | 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 | 55 |
section \<open>Setup for Numerals\<close> |
35953 | 56 |
|
60500 | 57 |
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close> |
58 |
setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close> |
|
62597 | 59 |
setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close> |
60 |
setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close> |
|
35953 | 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 | 63 |
|
60500 | 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 | 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 | 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 | 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 | 87 |
|
60500 | 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 | 104 |
absdummy @{typ nat} (absdummy @{typ nat} |
105 |
(Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $ |
|
67399 | 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 | 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 | 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 | 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 | 122 |
absdummy @{typ nat} (absdummy @{typ nat} |
123 |
(Const (@{const_name If}, @{typ bool} --> T --> T --> T) $ |
|
67399 | 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 | 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 | 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 | 152 |
subsection \<open>Inductive definitions for ordering on naturals\<close> |
35953 | 153 |
|
154 |
inductive less_nat |
|
155 |
where |
|
156 |
"less_nat 0 (Suc y)" |
|
157 |
| "less_nat x y ==> less_nat (Suc x) (Suc y)" |
|
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 | 160 |
"x < y = less_nat x y" |
161 |
apply (rule iffI) |
|
162 |
apply (induct x arbitrary: y) |
|
163 |
apply (case_tac y) apply (auto intro: less_nat.intros) |
|
164 |
apply (case_tac y) |
|
165 |
apply (auto intro: less_nat.intros) |
|
166 |
apply (induct rule: less_nat.induct) |
|
167 |
apply auto |
|
168 |
done |
|
169 |
||
170 |
inductive less_eq_nat |
|
171 |
where |
|
172 |
"less_eq_nat 0 y" |
|
173 |
| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)" |
|
174 |
||
175 |
lemma [code_pred_inline]: |
|
176 |
"x <= y = less_eq_nat x y" |
|
177 |
apply (rule iffI) |
|
178 |
apply (induct x arbitrary: y) |
|
179 |
apply (auto intro: less_eq_nat.intros) |
|
180 |
apply (case_tac y) apply (auto intro: less_eq_nat.intros) |
|
181 |
apply (induct rule: less_eq_nat.induct) |
|
182 |
apply auto done |
|
183 |
||
60500 | 184 |
section \<open>Alternative list definitions\<close> |
35953 | 185 |
|
61585 | 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 | 188 |
definition size_list' :: "'a list => nat" |
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 | 191 |
lemma size_list'_simps: |
192 |
"size_list' [] = 0" |
|
193 |
"size_list' (x # xs) = Suc (size_list' xs)" |
|
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 | 196 |
declare size_list'_simps[code_pred_def] |
197 |
declare size_list'_def[symmetric, code_pred_inline] |
|
35953 | 198 |
|
199 |
||
61585 | 200 |
subsection \<open>Alternative rules for \<open>list_all2\<close>\<close> |
35953 | 201 |
|
202 |
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []" |
|
203 |
by auto |
|
204 |
||
205 |
lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)" |
|
206 |
by auto |
|
207 |
||
208 |
code_pred [skip_proof] list_all2 |
|
209 |
proof - |
|
210 |
case list_all2 |
|
211 |
from this show thesis |
|
212 |
apply - |
|
213 |
apply (case_tac xb) |
|
214 |
apply (case_tac xc) |
|
215 |
apply auto |
|
216 |
apply (case_tac xc) |
|
217 |
apply auto |
|
218 |
done |
|
219 |
qed |
|
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 | 233 |
code_identifier constant member_i_i |
234 |
\<rightharpoonup> (SML) "List.member_i_i" |
|
235 |
and (OCaml) "List.member_i_i" |
|
236 |
and (Haskell) "List.member_i_i" |
|
237 |
and (Scala) "List.member_i_i" |
|
238 |
||
239 |
code_identifier constant member_i_o |
|
240 |
\<rightharpoonup> (SML) "List.member_i_o" |
|
241 |
and (OCaml) "List.member_i_o" |
|
242 |
and (Haskell) "List.member_i_o" |
|
243 |
and (Scala) "List.member_i_o" |
|
244 |
||
60500 | 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 | 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 | 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 | 259 |
|
46884 | 260 |
end |