(* Title: HOL/Library/Predicate_Compile_Alternative_Defs.thy
Author: Lukas Bulwahn, TU Muenchen
*)
theory Predicate_Compile_Alternative_Defs
imports Main
begin
section ‹Common constants
›
declare HOL.if_bool_eq_disj[code_pred_inline]
declare bool_diff_def[code_pred_inline]
declare inf_bool_def[abs_def, code_pred_inline]
declare less_bool_def[abs_def, code_pred_inline]
declare le_bool_def[abs_def, code_pred_inline]
lemma min_bool_eq [code_pred_inline]:
"(min :: bool => bool => bool) == (\)"
by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
lemma [code_pred_inline]:
"((A::bool) \ (B::bool)) = ((A \ \ B) \ (B \ \ A))"
by fast
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹Let›]
›
section ‹Pairs
›
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹fst
›,
🍋‹snd
›,
🍋‹case_prod
›]
›
section ‹Filters
›
(*TODO: shouldn't this be done by typedef? *)
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹Abs_filter
›,
🍋‹Rep_filter
›]
›
section ‹Bounded quantifiers
›
declare Ball_def[code_pred_inline]
declare Bex_def[code_pred_inline]
section ‹Operations on Predicates
›
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \ \ B x)"
by (simp add: fun_eq_iff)
lemma subset_eq[code_pred_inline]:
"(P :: 'a \ bool) < (Q :: 'a \ bool) \ ((\x. Q x \ (\ P x)) \ (\x. P x \ Q x))"
by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
lemma set_equality[code_pred_inline]:
"A = B \ (\x. A x \ B x) \ (\x. B x \ A x)"
by (auto simp add: fun_eq_iff)
section ‹Setup for Numerals
›
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹numeral
›]
›
setup ‹Predicate_Compile_Data.keep_functions [
🍋‹numeral
›]
›
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹Char
›]
›
setup ‹Predicate_Compile_Data.keep_functions [
🍋‹Char
›]
›
setup ‹Predicate_Compile_Data.ignore_consts [
🍋‹divide
›,
🍋‹modulo
›,
🍋‹times
›]
›
section ‹Arithmetic operations
›
subsection ‹Arithmetic on naturals
and integers
›
definition plus_eq_nat ::
"nat => nat => nat => bool"
where
"plus_eq_nat x y z = (x + y = z)"
definition minus_eq_nat ::
"nat => nat => nat => bool"
where
"minus_eq_nat x y z = (x - y = z)"
definition plus_eq_int ::
"int => int => int => bool"
where
"plus_eq_int x y z = (x + y = z)"
definition minus_eq_int ::
"int => int => int => bool"
where
"minus_eq_int x y z = (x - y = z)"
definition subtract
where
[code_unfold]:
"subtract x y = y - x"
setup ‹
let
val
Fun = Predicate_Compile_Aux.
Fun
val Input = Predicate_Compile_Aux.Input
val
Output = Predicate_Compile_Aux.
Output
val Bool = Predicate_Compile_Aux.Bool
val iio =
Fun (Input,
Fun (Input,
Fun (
Output, Bool)))
val ioi =
Fun (Input,
Fun (
Output,
Fun (Input, Bool)))
val oii =
Fun (
Output,
Fun (Input,
Fun (Input, Bool)))
val ooi =
Fun (
Output,
Fun (
Output,
Fun (Input, Bool)))
val plus_nat = Core_Data.functional_compilation
🍋‹plus
› iio
val minus_nat = Core_Data.functional_compilation
🍋‹minus
› iio
fun subtract_nat compfuns (_ :
typ) =
let
val T = Predicate_Compile_Aux.mk_monadT compfuns
🍋‹nat
›
in
absdummy
🍋‹nat
› (absdummy
🍋‹nat
›
(Const (
🍋‹If›,
🍋‹bool
› --> T --> T --> T) $
(
🍋‹(>) :: nat => nat => bool
› $ Bound 1 $ Bound 0) $
Predicate_Compile_Aux.mk_empty compfuns
🍋‹nat
› $
Predicate_Compile_Aux.mk_single compfuns
(
🍋‹(-) :: nat => nat => nat
› $ Bound 0 $ Bound 1)))
end
fun enumerate_addups_nat compfuns (_ :
typ) =
absdummy
🍋‹nat
› (Predicate_Compile_Aux.mk_iterate_upto compfuns
🍋‹nat * nat
›
(absdummy
🍋‹natural
› (
🍋‹Pair :: nat => nat => nat * nat
› $
(
🍋‹nat_of_natural
› $ Bound 0) $
(
🍋‹(-) :: nat => nat => nat
› $ Bound 1 $ (
🍋‹nat_of_natural
› $ Bound 0))),
🍋‹0 :: natural
›,
🍋‹natural_of_nat
› $ Bound 0))
fun enumerate_nats compfuns (_ :
typ) =
let
val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns
🍋‹0 :: nat
›)
val T = Predicate_Compile_Aux.mk_monadT compfuns 🍋‹nat›
in
absdummy 🍋‹nat› (absdummy 🍋‹nat›
(Const (🍋‹If›, 🍋‹bool› --> T --> T --> T) $
(🍋‹(=) :: nat => nat => bool› $ Bound 0 $ 🍋‹0::nat›) $
(Predicate_Compile_Aux.mk_iterate_upto compfuns 🍋‹nat› (🍋‹nat_of_natural›,
🍋‹0::natural›, 🍋‹natural_of_nat› $ Bound 1)) $
(single_const $ (🍋‹(+) :: nat => nat => nat› $ Bound 1 $ Bound 0))))
end
in
Core_Data.force_modes_and_compilations 🍋‹plus_eq_nat›
[(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
(ooi, (enumerate_addups_nat, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(🍋‹plus :: nat => nat => nat›, 🍋‹plus_eq_nat›)
#> Core_Data.force_modes_and_compilations 🍋‹minus_eq_nat›
[(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(🍋‹minus :: nat => nat => nat›, 🍋‹minus_eq_nat›)
#> Core_Data.force_modes_and_functions 🍋‹plus_eq_int›
[(iio, (🍋‹plus›, false)), (ioi, (🍋‹subtract›, false)),
(oii, (🍋‹subtract›, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(🍋‹plus :: int => int => int›, 🍋‹plus_eq_int›)
#> Core_Data.force_modes_and_functions 🍋‹minus_eq_int›
[(iio, (🍋‹minus›, false)), (oii, (🍋‹plus›, false)),
(ioi, (🍋‹minus›, false))]
#> Predicate_Compile_Fun.add_function_predicate_translation
(🍋‹minus :: int => int => int›, 🍋‹minus_eq_int›)
end
›
subsection ‹Inductive definitions for ordering on naturals›
inductive less_nat
where
"less_nat 0 (Suc y)"
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
lemma less_nat[code_pred_inline]:
"x < y = less_nat x y"
apply (rule iffI)
apply (induct x arbitrary: y)
apply (case_tac y) apply (auto intro: less_nat.intros)
apply (case_tac y)
apply (auto intro: less_nat.intros)
apply (induct rule: less_nat.induct)
apply auto
done
inductive less_eq_nat
where
"less_eq_nat 0 y"
| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
lemma [code_pred_inline]:
"x <= y = less_eq_nat x y"
apply (rule iffI)
apply (induct x arbitrary: y)
apply (auto intro: less_eq_nat.intros)
apply (case_tac y) apply (auto intro: less_eq_nat.intros)
apply (induct rule: less_eq_nat.induct)
apply auto done
section ‹Alternative list definitions›
subsection ‹Alternative rules for ‹length››
definition size_list' :: "'a list => nat"
where "size_list' = size"
lemma size_list'_simps:
"size_list' [] = 0"
"size_list' (x # xs) = Suc (size_list' xs)"
by (auto simp add: size_list'_def)
declare size_list'_simps[code_pred_def]
declare size_list'_def[symmetric, code_pred_inline]
subsection ‹Alternative rules for ‹list_all2››
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
by auto
lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
by auto
code_pred [skip_proof] list_all2
proof -
case list_all2
from this show thesis
apply -
apply (case_tac xb)
apply (case_tac xc)
apply auto
apply (case_tac xc)
apply auto
done
qed
subsection ‹Alternative rules for membership in lists›
lemma in_set_member [code_pred_inline]:
"x \ set xs \ List.member xs x"
by simp
lemma member_intros [code_pred_intro]:
"List.member (x#xs) x"
"List.member xs x \ List.member (y#xs) x"
by simp_all
code_pred List.member
by(auto simp add: elim: list.set_cases)
code_identifier constant member_i_i
⇀ (SML) "List.member_i_i"
and (OCaml) "List.member_i_i"
and (Haskell) "List.member_i_i"
and (Scala) "List.member_i_i"
code_identifier constant member_i_o
⇀ (SML) "List.member_i_o"
and (OCaml) "List.member_i_o"
and (Haskell) "List.member_i_o"
and (Scala) "List.member_i_o"
section ‹Setup for String.literal›
setup ‹Predicate_Compile_Data.ignore_consts [🍋‹String.Literal›]›
section ‹Simplification rules for optimisation›
lemma [code_pred_simp]: "\ False == True"
by auto
lemma [code_pred_simp]: "\ True == False"
by auto
lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
unfolding less_nat[symmetric] by auto
end
