src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 68028 1f9f973eed2a
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned equation
     1 (*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
     2     Author:     Lukas Bulwahn, TU Muenchen
     3 *)
     4 
     5 theory Predicate_Compile_Alternative_Defs
     6   imports Main
     7 begin
     8 
     9 section \<open>Common constants\<close>
    10 
    11 declare HOL.if_bool_eq_disj[code_pred_inline]
    12 
    13 declare bool_diff_def[code_pred_inline]
    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]
    17 
    18 lemma min_bool_eq [code_pred_inline]: "(min :: bool => bool => bool) == (\<and>)"
    19 by (rule eq_reflection) (auto simp add: fun_eq_iff min_def)
    20 
    21 lemma [code_pred_inline]: 
    22   "((A::bool) \<noteq> (B::bool)) = ((A \<and> \<not> B) \<or> (B \<and> \<not> A))"
    23 by fast
    24 
    25 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Let}]\<close>
    26 
    27 section \<open>Pairs\<close>
    28 
    29 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
    30 
    31 section \<open>Filters\<close>
    32 
    33 (*TODO: shouldn't this be done by typedef? *)
    34 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}]\<close>
    35 
    36 section \<open>Bounded quantifiers\<close>
    37 
    38 declare Ball_def[code_pred_inline]
    39 declare Bex_def[code_pred_inline]
    40 
    41 section \<open>Operations on Predicates\<close>
    42 
    43 lemma Diff[code_pred_inline]:
    44   "(A - B) = (%x. A x \<and> \<not> B x)"
    45   by (simp add: fun_eq_iff)
    46 
    47 lemma subset_eq[code_pred_inline]:
    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))"
    49   by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
    50 
    51 lemma set_equality[code_pred_inline]:
    52   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
    53   by (auto simp add: fun_eq_iff)
    54 
    55 section \<open>Setup for Numerals\<close>
    56 
    57 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close>
    58 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close>
    59 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Char}]\<close>
    60 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name Char}]\<close>
    61 
    62 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name modulo}, @{const_name times}]\<close>
    63 
    64 section \<open>Arithmetic operations\<close>
    65 
    66 subsection \<open>Arithmetic on naturals and integers\<close>
    67 
    68 definition plus_eq_nat :: "nat => nat => nat => bool"
    69 where
    70   "plus_eq_nat x y z = (x + y = z)"
    71 
    72 definition minus_eq_nat :: "nat => nat => nat => bool"
    73 where
    74   "minus_eq_nat x y z = (x - y = z)"
    75 
    76 definition plus_eq_int :: "int => int => int => bool"
    77 where
    78   "plus_eq_int x y z = (x + y = z)"
    79 
    80 definition minus_eq_int :: "int => int => int => bool"
    81 where
    82   "minus_eq_int x y z = (x - y = z)"
    83 
    84 definition subtract
    85 where
    86   [code_unfold]: "subtract x y = y - x"
    87 
    88 setup \<open>
    89 let
    90   val Fun = Predicate_Compile_Aux.Fun
    91   val Input = Predicate_Compile_Aux.Input
    92   val Output = Predicate_Compile_Aux.Output
    93   val Bool = Predicate_Compile_Aux.Bool
    94   val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
    95   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
    96   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
    97   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
    98   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
    99   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
   100   fun subtract_nat compfuns (_ : typ) =
   101     let
   102       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
   103     in
   104       absdummy @{typ nat} (absdummy @{typ nat}
   105         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
   106           (@{term "(>) :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
   107           Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
   108           Predicate_Compile_Aux.mk_single compfuns
   109           (@{term "(-) :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
   110     end
   111   fun enumerate_addups_nat compfuns (_ : typ) =
   112     absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
   113     (absdummy @{typ natural} (@{term "Pair :: nat => nat => nat * nat"} $
   114       (@{term "nat_of_natural"} $ Bound 0) $
   115       (@{term "(-) :: nat => nat => nat"} $ Bound 1 $ (@{term "nat_of_natural"} $ Bound 0))),
   116       @{term "0 :: natural"}, @{term "natural_of_nat"} $ Bound 0))
   117   fun enumerate_nats compfuns  (_ : typ) =
   118     let
   119       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
   120       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
   121     in
   122       absdummy @{typ nat} (absdummy @{typ nat}
   123         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
   124           (@{term "(=) :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
   125           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "nat_of_natural"},
   126             @{term "0::natural"}, @{term "natural_of_nat"} $ Bound 1)) $
   127             (single_const $ (@{term "(+) :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
   128     end
   129 in
   130   Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
   131     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
   132      (ooi, (enumerate_addups_nat, false))]
   133   #> Predicate_Compile_Fun.add_function_predicate_translation
   134        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
   135   #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
   136        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
   137   #> Predicate_Compile_Fun.add_function_predicate_translation
   138       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
   139   #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
   140     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
   141      (oii, (@{const_name subtract}, false))]
   142   #> Predicate_Compile_Fun.add_function_predicate_translation
   143        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
   144   #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
   145     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
   146      (ioi, (@{const_name minus}, false))]
   147   #> Predicate_Compile_Fun.add_function_predicate_translation
   148       (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
   149 end
   150 \<close>
   151 
   152 subsection \<open>Inductive definitions for ordering on naturals\<close>
   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 
   159 lemma less_nat[code_pred_inline]:
   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 
   184 section \<open>Alternative list definitions\<close>
   185 
   186 subsection \<open>Alternative rules for \<open>length\<close>\<close>
   187 
   188 definition size_list' :: "'a list => nat"
   189 where "size_list' = size"
   190 
   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)
   195 
   196 declare size_list'_simps[code_pred_def]
   197 declare size_list'_def[symmetric, code_pred_inline]
   198 
   199 
   200 subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
   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 
   221 subsection \<open>Alternative rules for membership in lists\<close>
   222 
   223 declare in_set_member[code_pred_inline]
   224 
   225 lemma member_intros [code_pred_intro]:
   226   "List.member (x#xs) x"
   227   "List.member xs x \<Longrightarrow> List.member (y#xs) x"
   228 by(simp_all add: List.member_def)
   229 
   230 code_pred List.member
   231   by(auto simp add: List.member_def elim: list.set_cases)
   232 
   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 
   245 section \<open>Setup for String.literal\<close>
   246 
   247 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\<close>
   248 
   249 section \<open>Simplification rules for optimisation\<close>
   250 
   251 lemma [code_pred_simp]: "\<not> False == True"
   252 by auto
   253 
   254 lemma [code_pred_simp]: "\<not> True == False"
   255 by auto
   256 
   257 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
   258 unfolding less_nat[symmetric] by auto
   259 
   260 end