src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61585 a9599d3d7610 child 62597 b3f2b8c906a6 permissions -rw-r--r--
more symbols;
```     1 theory Predicate_Compile_Alternative_Defs
```
```     2 imports Main
```
```     3 begin
```
```     4
```
```     5 section \<open>Common constants\<close>
```
```     6
```
```     7 declare HOL.if_bool_eq_disj[code_pred_inline]
```
```     8
```
```     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]
```
```    13
```
```    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)
```
```    16
```
```    17 lemma [code_pred_inline]:
```
```    18   "((A::bool) ~= (B::bool)) = ((A & ~ B) | (B & ~ A))"
```
```    19 by fast
```
```    20
```
```    21 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Let}]\<close>
```
```    22
```
```    23 section \<open>Pairs\<close>
```
```    24
```
```    25 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name case_prod}]\<close>
```
```    26
```
```    27 section \<open>Filters\<close>
```
```    28
```
```    29 (*TODO: shouldn't this be done by typedef? *)
```
```    30 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name Abs_filter}, @{const_name Rep_filter}]\<close>
```
```    31
```
```    32 section \<open>Bounded quantifiers\<close>
```
```    33
```
```    34 declare Ball_def[code_pred_inline]
```
```    35 declare Bex_def[code_pred_inline]
```
```    36
```
```    37 section \<open>Operations on Predicates\<close>
```
```    38
```
```    39 lemma Diff[code_pred_inline]:
```
```    40   "(A - B) = (%x. A x \<and> \<not> B x)"
```
```    41   by (simp add: fun_eq_iff)
```
```    42
```
```    43 lemma subset_eq[code_pred_inline]:
```
```    44   "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
```
```    45   by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
```
```    46
```
```    47 lemma set_equality[code_pred_inline]:
```
```    48   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
```
```    49   by (auto simp add: fun_eq_iff)
```
```    50
```
```    51 section \<open>Setup for Numerals\<close>
```
```    52
```
```    53 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name numeral}]\<close>
```
```    54 setup \<open>Predicate_Compile_Data.keep_functions [@{const_name numeral}]\<close>
```
```    55
```
```    56 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name divide}, @{const_name mod}, @{const_name times}]\<close>
```
```    57
```
```    58 section \<open>Arithmetic operations\<close>
```
```    59
```
```    60 subsection \<open>Arithmetic on naturals and integers\<close>
```
```    61
```
```    62 definition plus_eq_nat :: "nat => nat => nat => bool"
```
```    63 where
```
```    64   "plus_eq_nat x y z = (x + y = z)"
```
```    65
```
```    66 definition minus_eq_nat :: "nat => nat => nat => bool"
```
```    67 where
```
```    68   "minus_eq_nat x y z = (x - y = z)"
```
```    69
```
```    70 definition plus_eq_int :: "int => int => int => bool"
```
```    71 where
```
```    72   "plus_eq_int x y z = (x + y = z)"
```
```    73
```
```    74 definition minus_eq_int :: "int => int => int => bool"
```
```    75 where
```
```    76   "minus_eq_int x y z = (x - y = z)"
```
```    77
```
```    78 definition subtract
```
```    79 where
```
```    80   [code_unfold]: "subtract x y = y - x"
```
```    81
```
```    82 setup \<open>
```
```    83 let
```
```    84   val Fun = Predicate_Compile_Aux.Fun
```
```    85   val Input = Predicate_Compile_Aux.Input
```
```    86   val Output = Predicate_Compile_Aux.Output
```
```    87   val Bool = Predicate_Compile_Aux.Bool
```
```    88   val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
```
```    89   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
```
```    90   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
```
```    91   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
```
```    92   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
```
```    93   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
```
```    94   fun subtract_nat compfuns (_ : typ) =
```
```    95     let
```
```    96       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
```
```    97     in
```
```    98       absdummy @{typ nat} (absdummy @{typ nat}
```
```    99         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) \$
```
```   100           (@{term "op > :: nat => nat => bool"} \$ Bound 1 \$ Bound 0) \$
```
```   101           Predicate_Compile_Aux.mk_empty compfuns @{typ nat} \$
```
```   102           Predicate_Compile_Aux.mk_single compfuns
```
```   103           (@{term "op - :: nat => nat => nat"} \$ Bound 0 \$ Bound 1)))
```
```   104     end
```
```   105   fun enumerate_addups_nat compfuns (_ : typ) =
```
```   106     absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
```
```   107     (absdummy @{typ natural} (@{term "Pair :: nat => nat => nat * nat"} \$
```
```   108       (@{term "nat_of_natural"} \$ Bound 0) \$
```
```   109       (@{term "op - :: nat => nat => nat"} \$ Bound 1 \$ (@{term "nat_of_natural"} \$ Bound 0))),
```
```   110       @{term "0 :: natural"}, @{term "natural_of_nat"} \$ Bound 0))
```
```   111   fun enumerate_nats compfuns  (_ : typ) =
```
```   112     let
```
```   113       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
```
```   114       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
```
```   115     in
```
```   116       absdummy @{typ nat} (absdummy @{typ nat}
```
```   117         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) \$
```
```   118           (@{term "op = :: nat => nat => bool"} \$ Bound 0 \$ @{term "0::nat"}) \$
```
```   119           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "nat_of_natural"},
```
```   120             @{term "0::natural"}, @{term "natural_of_nat"} \$ Bound 1)) \$
```
```   121             (single_const \$ (@{term "op + :: nat => nat => nat"} \$ Bound 1 \$ Bound 0))))
```
```   122     end
```
```   123 in
```
```   124   Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
```
```   125     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
```
```   126      (ooi, (enumerate_addups_nat, false))]
```
```   127   #> Predicate_Compile_Fun.add_function_predicate_translation
```
```   128        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
```
```   129   #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
```
```   130        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
```
```   131   #> Predicate_Compile_Fun.add_function_predicate_translation
```
```   132       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
```
```   133   #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
```
```   134     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
```
```   135      (oii, (@{const_name subtract}, false))]
```
```   136   #> Predicate_Compile_Fun.add_function_predicate_translation
```
```   137        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
```
```   138   #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
```
```   139     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
```
```   140      (ioi, (@{const_name minus}, false))]
```
```   141   #> Predicate_Compile_Fun.add_function_predicate_translation
```
```   142       (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
```
```   143 end
```
```   144 \<close>
```
```   145
```
```   146 subsection \<open>Inductive definitions for ordering on naturals\<close>
```
```   147
```
```   148 inductive less_nat
```
```   149 where
```
```   150   "less_nat 0 (Suc y)"
```
```   151 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
```
```   152
```
```   153 lemma less_nat[code_pred_inline]:
```
```   154   "x < y = less_nat x y"
```
```   155 apply (rule iffI)
```
```   156 apply (induct x arbitrary: y)
```
```   157 apply (case_tac y) apply (auto intro: less_nat.intros)
```
```   158 apply (case_tac y)
```
```   159 apply (auto intro: less_nat.intros)
```
```   160 apply (induct rule: less_nat.induct)
```
```   161 apply auto
```
```   162 done
```
```   163
```
```   164 inductive less_eq_nat
```
```   165 where
```
```   166   "less_eq_nat 0 y"
```
```   167 | "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
```
```   168
```
```   169 lemma [code_pred_inline]:
```
```   170 "x <= y = less_eq_nat x y"
```
```   171 apply (rule iffI)
```
```   172 apply (induct x arbitrary: y)
```
```   173 apply (auto intro: less_eq_nat.intros)
```
```   174 apply (case_tac y) apply (auto intro: less_eq_nat.intros)
```
```   175 apply (induct rule: less_eq_nat.induct)
```
```   176 apply auto done
```
```   177
```
```   178 section \<open>Alternative list definitions\<close>
```
```   179
```
```   180 subsection \<open>Alternative rules for \<open>length\<close>\<close>
```
```   181
```
```   182 definition size_list' :: "'a list => nat"
```
```   183 where "size_list' = size"
```
```   184
```
```   185 lemma size_list'_simps:
```
```   186   "size_list' [] = 0"
```
```   187   "size_list' (x # xs) = Suc (size_list' xs)"
```
```   188 by (auto simp add: size_list'_def)
```
```   189
```
```   190 declare size_list'_simps[code_pred_def]
```
```   191 declare size_list'_def[symmetric, code_pred_inline]
```
```   192
```
```   193
```
```   194 subsection \<open>Alternative rules for \<open>list_all2\<close>\<close>
```
```   195
```
```   196 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
```
```   197 by auto
```
```   198
```
```   199 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
```
```   200 by auto
```
```   201
```
```   202 code_pred [skip_proof] list_all2
```
```   203 proof -
```
```   204   case list_all2
```
```   205   from this show thesis
```
```   206     apply -
```
```   207     apply (case_tac xb)
```
```   208     apply (case_tac xc)
```
```   209     apply auto
```
```   210     apply (case_tac xc)
```
```   211     apply auto
```
```   212     done
```
```   213 qed
```
```   214
```
```   215 subsection \<open>Alternative rules for membership in lists\<close>
```
```   216
```
```   217 declare in_set_member[code_pred_inline]
```
```   218
```
```   219 lemma member_intros [code_pred_intro]:
```
```   220   "List.member (x#xs) x"
```
```   221   "List.member xs x \<Longrightarrow> List.member (y#xs) x"
```
```   222 by(simp_all add: List.member_def)
```
```   223
```
```   224 code_pred List.member
```
```   225   by(auto simp add: List.member_def elim: list.set_cases)
```
```   226
```
```   227 code_identifier constant member_i_i
```
```   228    \<rightharpoonup> (SML) "List.member_i_i"
```
```   229   and (OCaml) "List.member_i_i"
```
```   230   and (Haskell) "List.member_i_i"
```
```   231   and (Scala) "List.member_i_i"
```
```   232
```
```   233 code_identifier constant member_i_o
```
```   234    \<rightharpoonup> (SML) "List.member_i_o"
```
```   235   and (OCaml) "List.member_i_o"
```
```   236   and (Haskell) "List.member_i_o"
```
```   237   and (Scala) "List.member_i_o"
```
```   238
```
```   239 section \<open>Setup for String.literal\<close>
```
```   240
```
```   241 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>
```
```   242
```
```   243 section \<open>Simplification rules for optimisation\<close>
```
```   244
```
```   245 lemma [code_pred_simp]: "\<not> False == True"
```
```   246 by auto
```
```   247
```
```   248 lemma [code_pred_simp]: "\<not> True == False"
```
```   249 by auto
```
```   250
```
```   251 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
```
```   252 unfolding less_nat[symmetric] by auto
```
```   253
```
```   254 end
```