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
```