src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
 author bulwahn Mon Apr 30 12:14:51 2012 +0200 (2012-04-30) changeset 47840 732ea1f08e3f parent 47108 2a1953f0d20d child 48640 053cc8dfde35 permissions -rw-r--r--
removing obsolete setup for sets now that sets are executable
1 theory Predicate_Compile_Alternative_Defs
2 imports Main
3 begin
5 section {* Common constants *}
7 declare HOL.if_bool_eq_disj[code_pred_inline]
9 declare bool_diff_def[code_pred_inline]
10 declare inf_bool_def[abs_def, code_pred_inline]
11 declare less_bool_def[abs_def, code_pred_inline]
12 declare le_bool_def[abs_def, code_pred_inline]
14 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (op &)"
15 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
17 lemma [code_pred_inline]:
18   "((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))"
19 by fast
21 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
23 section {* Pairs *}
25 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
27 section {* Bounded quantifiers *}
29 declare Ball_def[code_pred_inline]
30 declare Bex_def[code_pred_inline]
32 section {* Operations on Predicates *}
34 lemma Diff[code_pred_inline]:
35   "(A - B) = (%x. A x \<and> \<not> B x)"
38 lemma subset_eq[code_pred_inline]:
39   "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
40   by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
42 lemma set_equality[code_pred_inline]:
43   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
44   by (auto simp add: fun_eq_iff)
46 section {* Setup for Numerals *}
48 setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
49 setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
51 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
53 section {* Arithmetic operations *}
55 subsection {* Arithmetic on naturals and integers *}
57 definition plus_eq_nat :: "nat => nat => nat => bool"
58 where
59   "plus_eq_nat x y z = (x + y = z)"
61 definition minus_eq_nat :: "nat => nat => nat => bool"
62 where
63   "minus_eq_nat x y z = (x - y = z)"
65 definition plus_eq_int :: "int => int => int => bool"
66 where
67   "plus_eq_int x y z = (x + y = z)"
69 definition minus_eq_int :: "int => int => int => bool"
70 where
71   "minus_eq_int x y z = (x - y = z)"
73 definition subtract
74 where
75   [code_unfold]: "subtract x y = y - x"
77 setup {*
78 let
79   val Fun = Predicate_Compile_Aux.Fun
80   val Input = Predicate_Compile_Aux.Input
81   val Output = Predicate_Compile_Aux.Output
82   val Bool = Predicate_Compile_Aux.Bool
83   val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
84   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
85   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
86   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
87   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
88   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
89   fun subtract_nat compfuns (_ : typ) =
90     let
91       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
92     in
93       absdummy @{typ nat} (absdummy @{typ nat}
94         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) \$
95           (@{term "op > :: nat => nat => bool"} \$ Bound 1 \$ Bound 0) \$
96           Predicate_Compile_Aux.mk_empty compfuns @{typ nat} \$
97           Predicate_Compile_Aux.mk_single compfuns
98           (@{term "op - :: nat => nat => nat"} \$ Bound 0 \$ Bound 1)))
99     end
100   fun enumerate_addups_nat compfuns (_ : typ) =
101     absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
102     (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} \$
103       (@{term "Code_Numeral.nat_of"} \$ Bound 0) \$
104       (@{term "op - :: nat => nat => nat"} \$ Bound 1 \$ (@{term "Code_Numeral.nat_of"} \$ Bound 0))),
105       @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} \$ Bound 0))
106   fun enumerate_nats compfuns  (_ : typ) =
107     let
108       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
109       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
110     in
111       absdummy @{typ nat} (absdummy @{typ nat}
112         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) \$
113           (@{term "op = :: nat => nat => bool"} \$ Bound 0 \$ @{term "0::nat"}) \$
114           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
115             @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} \$ Bound 1)) \$
116             (single_const \$ (@{term "op + :: nat => nat => nat"} \$ Bound 1 \$ Bound 0))))
117     end
118 in
119   Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
120     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
123        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
124   #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
125        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
127       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
128   #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
129     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
130      (oii, (@{const_name subtract}, false))]
132        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
133   #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
134     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
135      (ioi, (@{const_name minus}, false))]
137       (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
138 end
139 *}
141 subsection {* Inductive definitions for ordering on naturals *}
143 inductive less_nat
144 where
145   "less_nat 0 (Suc y)"
146 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
148 lemma less_nat[code_pred_inline]:
149   "x < y = less_nat x y"
150 apply (rule iffI)
151 apply (induct x arbitrary: y)
152 apply (case_tac y) apply (auto intro: less_nat.intros)
153 apply (case_tac y)
154 apply (auto intro: less_nat.intros)
155 apply (induct rule: less_nat.induct)
156 apply auto
157 done
159 inductive less_eq_nat
160 where
161   "less_eq_nat 0 y"
162 | "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
164 lemma [code_pred_inline]:
165 "x <= y = less_eq_nat x y"
166 apply (rule iffI)
167 apply (induct x arbitrary: y)
168 apply (auto intro: less_eq_nat.intros)
169 apply (case_tac y) apply (auto intro: less_eq_nat.intros)
170 apply (induct rule: less_eq_nat.induct)
171 apply auto done
173 section {* Alternative list definitions *}
175 subsection {* Alternative rules for length *}
177 definition size_list :: "'a list => nat"
178 where "size_list = size"
180 lemma size_list_simps:
181   "size_list [] = 0"
182   "size_list (x # xs) = Suc (size_list xs)"
183 by (auto simp add: size_list_def)
185 declare size_list_simps[code_pred_def]
186 declare size_list_def[symmetric, code_pred_inline]
189 subsection {* Alternative rules for list_all2 *}
191 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
192 by auto
194 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
195 by auto
197 code_pred [skip_proof] list_all2
198 proof -
199   case list_all2
200   from this show thesis
201     apply -
202     apply (case_tac xb)
203     apply (case_tac xc)
204     apply auto
205     apply (case_tac xc)
206     apply auto
207     apply fastforce
208     done
209 qed
211 section {* Setup for String.literal *}
213 setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
215 section {* Simplification rules for optimisation *}
217 lemma [code_pred_simp]: "\<not> False == True"
218 by auto
220 lemma [code_pred_simp]: "\<not> True == False"
221 by auto
223 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
224 unfolding less_nat[symmetric] by auto
226 end