src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author huffman
Fri Mar 30 12:32:35 2012 +0200 (2012-03-30)
changeset 47220 52426c62b5d0
parent 47108 2a1953f0d20d
child 47840 732ea1f08e3f
permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
     1 theory Predicate_Compile_Alternative_Defs
     2 imports Main
     3 begin
     4 
     5 section {* Common constants *}
     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 {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    22 
    23 section {* Pairs *}
    24 
    25 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
    26 
    27 section {* Bounded quantifiers *}
    28 
    29 declare Ball_def[code_pred_inline]
    30 declare Bex_def[code_pred_inline]
    31 
    32 section {* Set operations *}
    33 
    34 declare eq_reflection[OF empty_def, code_pred_inline]
    35 
    36 declare subset_iff[code_pred_inline]
    37 
    38 declare Int_def[code_pred_inline]
    39 declare eq_reflection[OF Un_def, code_pred_inline]
    40 declare eq_reflection[OF UNION_eq, code_pred_inline]
    41 
    42 lemma Diff[code_pred_inline]:
    43   "(A - B) = (%x. A x \<and> \<not> B x)"
    44   by (simp add: fun_eq_iff)
    45 
    46 lemma subset_eq[code_pred_inline]:
    47   "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
    48   by (rule eq_reflection) (auto simp add: less_fun_def le_fun_def)
    49 
    50 lemma set_equality[code_pred_inline]:
    51   "A = B \<longleftrightarrow> (\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x)"
    52   by (auto simp add: fun_eq_iff)
    53 
    54 
    55 section {* Setup for Numerals *}
    56 
    57 setup {* Predicate_Compile_Data.ignore_consts [@{const_name numeral}, @{const_name neg_numeral}] *}
    58 setup {* Predicate_Compile_Data.keep_functions [@{const_name numeral}, @{const_name neg_numeral}] *}
    59 
    60 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    61 
    62 section {* Arithmetic operations *}
    63 
    64 subsection {* Arithmetic on naturals and integers *}
    65 
    66 definition plus_eq_nat :: "nat => nat => nat => bool"
    67 where
    68   "plus_eq_nat x y z = (x + y = z)"
    69 
    70 definition minus_eq_nat :: "nat => nat => nat => bool"
    71 where
    72   "minus_eq_nat x y z = (x - y = z)"
    73 
    74 definition plus_eq_int :: "int => int => int => bool"
    75 where
    76   "plus_eq_int x y z = (x + y = z)"
    77 
    78 definition minus_eq_int :: "int => int => int => bool"
    79 where
    80   "minus_eq_int x y z = (x - y = z)"
    81 
    82 definition subtract
    83 where
    84   [code_unfold]: "subtract x y = y - x"
    85 
    86 setup {*
    87 let
    88   val Fun = Predicate_Compile_Aux.Fun
    89   val Input = Predicate_Compile_Aux.Input
    90   val Output = Predicate_Compile_Aux.Output
    91   val Bool = Predicate_Compile_Aux.Bool
    92   val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
    93   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
    94   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
    95   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
    96   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
    97   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
    98   fun subtract_nat compfuns (_ : typ) =
    99     let
   100       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
   101     in
   102       absdummy @{typ nat} (absdummy @{typ nat}
   103         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
   104           (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
   105           Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
   106           Predicate_Compile_Aux.mk_single compfuns
   107           (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
   108     end
   109   fun enumerate_addups_nat compfuns (_ : typ) =
   110     absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
   111     (absdummy @{typ code_numeral} (@{term "Pair :: nat => nat => nat * nat"} $
   112       (@{term "Code_Numeral.nat_of"} $ Bound 0) $
   113       (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
   114       @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
   115   fun enumerate_nats compfuns  (_ : typ) =
   116     let
   117       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
   118       val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
   119     in
   120       absdummy @{typ nat} (absdummy @{typ nat}
   121         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
   122           (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
   123           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
   124             @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
   125             (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
   126     end
   127 in
   128   Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
   129     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
   130      (ooi, (enumerate_addups_nat, false))]
   131   #> Predicate_Compile_Fun.add_function_predicate_translation
   132        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
   133   #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
   134        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
   135   #> Predicate_Compile_Fun.add_function_predicate_translation
   136       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
   137   #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
   138     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
   139      (oii, (@{const_name subtract}, false))]
   140   #> Predicate_Compile_Fun.add_function_predicate_translation
   141        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
   142   #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
   143     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
   144      (ioi, (@{const_name minus}, false))]
   145   #> Predicate_Compile_Fun.add_function_predicate_translation
   146       (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
   147 end
   148 *}
   149 
   150 subsection {* Inductive definitions for ordering on naturals *}
   151 
   152 inductive less_nat
   153 where
   154   "less_nat 0 (Suc y)"
   155 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
   156 
   157 lemma less_nat[code_pred_inline]:
   158   "x < y = less_nat x y"
   159 apply (rule iffI)
   160 apply (induct x arbitrary: y)
   161 apply (case_tac y) apply (auto intro: less_nat.intros)
   162 apply (case_tac y)
   163 apply (auto intro: less_nat.intros)
   164 apply (induct rule: less_nat.induct)
   165 apply auto
   166 done
   167 
   168 inductive less_eq_nat
   169 where
   170   "less_eq_nat 0 y"
   171 | "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
   172 
   173 lemma [code_pred_inline]:
   174 "x <= y = less_eq_nat x y"
   175 apply (rule iffI)
   176 apply (induct x arbitrary: y)
   177 apply (auto intro: less_eq_nat.intros)
   178 apply (case_tac y) apply (auto intro: less_eq_nat.intros)
   179 apply (induct rule: less_eq_nat.induct)
   180 apply auto done
   181 
   182 section {* Alternative list definitions *}
   183 
   184 subsection {* Alternative rules for length *}
   185 
   186 definition size_list :: "'a list => nat"
   187 where "size_list = size"
   188 
   189 lemma size_list_simps:
   190   "size_list [] = 0"
   191   "size_list (x # xs) = Suc (size_list xs)"
   192 by (auto simp add: size_list_def)
   193 
   194 declare size_list_simps[code_pred_def]
   195 declare size_list_def[symmetric, code_pred_inline]
   196 
   197 
   198 subsection {* Alternative rules for list_all2 *}
   199 
   200 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   201 by auto
   202 
   203 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
   204 by auto
   205 
   206 code_pred [skip_proof] list_all2
   207 proof -
   208   case list_all2
   209   from this show thesis
   210     apply -
   211     apply (case_tac xb)
   212     apply (case_tac xc)
   213     apply auto
   214     apply (case_tac xc)
   215     apply auto
   216     apply fastforce
   217     done
   218 qed
   219 
   220 section {* Setup for String.literal *}
   221 
   222 setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
   223 
   224 section {* Simplification rules for optimisation *}
   225 
   226 lemma [code_pred_simp]: "\<not> False == True"
   227 by auto
   228 
   229 lemma [code_pred_simp]: "\<not> True == False"
   230 by auto
   231 
   232 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
   233 unfolding less_nat[symmetric] by auto
   234 
   235 end