src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 41075 4bed56dc95fb
child 44241 7943b69f0188
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
     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_raw[code_pred_inline]
    11 declare less_bool_def_raw[code_pred_inline]
    12 declare le_bool_def_raw[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 le_bool_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 Collect_def[code_pred_inline]
    35 declare mem_def[code_pred_inline]
    36 
    37 declare eq_reflection[OF empty_def, code_pred_inline]
    38 declare insert_code[code_pred_def]
    39 
    40 declare subset_iff[code_pred_inline]
    41 
    42 declare Int_def[code_pred_inline]
    43 declare eq_reflection[OF Un_def, code_pred_inline]
    44 declare eq_reflection[OF UNION_def, code_pred_inline]
    45 
    46 lemma Diff[code_pred_inline]:
    47   "(A - B) = (%x. A x \<and> \<not> B x)"
    48 by (auto simp add: mem_def)
    49 
    50 lemma subset_eq[code_pred_inline]:
    51   "(P :: 'a => bool) < (Q :: 'a => bool) == ((\<exists>x. Q x \<and> (\<not> P x)) \<and> (\<forall> x. P x --> Q x))"
    52 by (rule eq_reflection) (fastsimp simp add: mem_def)
    53 
    54 lemma set_equality[code_pred_inline]:
    55   "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    56 by (fastsimp simp add: mem_def)
    57 
    58 section {* Setup for Numerals *}
    59 
    60 setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
    61 setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
    62 
    63 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    64 
    65 section {* Arithmetic operations *}
    66 
    67 subsection {* Arithmetic on naturals and integers *}
    68 
    69 definition plus_eq_nat :: "nat => nat => nat => bool"
    70 where
    71   "plus_eq_nat x y z = (x + y = z)"
    72 
    73 definition minus_eq_nat :: "nat => nat => nat => bool"
    74 where
    75   "minus_eq_nat x y z = (x - y = z)"
    76 
    77 definition plus_eq_int :: "int => int => int => bool"
    78 where
    79   "plus_eq_int x y z = (x + y = z)"
    80 
    81 definition minus_eq_int :: "int => int => int => bool"
    82 where
    83   "minus_eq_int x y z = (x - y = z)"
    84 
    85 definition subtract
    86 where
    87   [code_inline]: "subtract x y = y - x"
    88 
    89 setup {*
    90 let
    91   val Fun = Predicate_Compile_Aux.Fun
    92   val Input = Predicate_Compile_Aux.Input
    93   val Output = Predicate_Compile_Aux.Output
    94   val Bool = Predicate_Compile_Aux.Bool
    95   val iio = Fun (Input, Fun (Input, Fun (Output, Bool)))
    96   val ioi = Fun (Input, Fun (Output, Fun (Input, Bool)))
    97   val oii = Fun (Output, Fun (Input, Fun (Input, Bool)))
    98   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
    99   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
   100   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
   101   fun subtract_nat compfuns (_ : typ) =
   102     let
   103       val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
   104     in
   105       absdummy (@{typ nat}, absdummy (@{typ nat},
   106         Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
   107           (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
   108           Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
   109           Predicate_Compile_Aux.mk_single compfuns
   110           (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
   111     end
   112   fun enumerate_addups_nat compfuns (_ : typ) =
   113     absdummy (@{typ nat}, Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}
   114     (absdummy (@{typ code_numeral}, @{term "Pair :: nat => nat => nat * nat"} $
   115       (@{term "Code_Numeral.nat_of"} $ Bound 0) $
   116       (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
   117       @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
   118   fun enumerate_nats compfuns  (_ : typ) =
   119     let
   120       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
   121       val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
   122     in
   123       absdummy(@{typ nat}, absdummy (@{typ nat},
   124         Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
   125           (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
   126           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},
   127             @{term "0::code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 1)) $
   128             (single_const $ (@{term "op + :: nat => nat => nat"} $ Bound 1 $ Bound 0))))
   129     end
   130 in
   131   Core_Data.force_modes_and_compilations @{const_name plus_eq_nat}
   132     [(iio, (plus_nat, false)), (oii, (subtract_nat, false)), (ioi, (subtract_nat, false)),
   133      (ooi, (enumerate_addups_nat, false))]
   134   #> Predicate_Compile_Fun.add_function_predicate_translation
   135        (@{term "plus :: nat => nat => nat"}, @{term "plus_eq_nat"})
   136   #> Core_Data.force_modes_and_compilations @{const_name minus_eq_nat}
   137        [(iio, (minus_nat, false)), (oii, (enumerate_nats, false))]
   138   #> Predicate_Compile_Fun.add_function_predicate_translation
   139       (@{term "minus :: nat => nat => nat"}, @{term "minus_eq_nat"})
   140   #> Core_Data.force_modes_and_functions @{const_name plus_eq_int}
   141     [(iio, (@{const_name plus}, false)), (ioi, (@{const_name subtract}, false)),
   142      (oii, (@{const_name subtract}, false))]
   143   #> Predicate_Compile_Fun.add_function_predicate_translation
   144        (@{term "plus :: int => int => int"}, @{term "plus_eq_int"})
   145   #> Core_Data.force_modes_and_functions @{const_name minus_eq_int}
   146     [(iio, (@{const_name minus}, false)), (oii, (@{const_name plus}, false)),
   147      (ioi, (@{const_name minus}, false))]
   148   #> Predicate_Compile_Fun.add_function_predicate_translation
   149       (@{term "minus :: int => int => int"}, @{term "minus_eq_int"})
   150 end
   151 *}
   152 
   153 subsection {* Inductive definitions for ordering on naturals *}
   154 
   155 inductive less_nat
   156 where
   157   "less_nat 0 (Suc y)"
   158 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
   159 
   160 lemma less_nat[code_pred_inline]:
   161   "x < y = less_nat x y"
   162 apply (rule iffI)
   163 apply (induct x arbitrary: y)
   164 apply (case_tac y) apply (auto intro: less_nat.intros)
   165 apply (case_tac y)
   166 apply (auto intro: less_nat.intros)
   167 apply (induct rule: less_nat.induct)
   168 apply auto
   169 done
   170 
   171 inductive less_eq_nat
   172 where
   173   "less_eq_nat 0 y"
   174 | "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
   175 
   176 lemma [code_pred_inline]:
   177 "x <= y = less_eq_nat x y"
   178 apply (rule iffI)
   179 apply (induct x arbitrary: y)
   180 apply (auto intro: less_eq_nat.intros)
   181 apply (case_tac y) apply (auto intro: less_eq_nat.intros)
   182 apply (induct rule: less_eq_nat.induct)
   183 apply auto done
   184 
   185 section {* Alternative list definitions *}
   186 
   187 subsection {* Alternative rules for length *}
   188 
   189 definition size_list :: "'a list => nat"
   190 where "size_list = size"
   191 
   192 lemma size_list_simps:
   193   "size_list [] = 0"
   194   "size_list (x # xs) = Suc (size_list xs)"
   195 by (auto simp add: size_list_def)
   196 
   197 declare size_list_simps[code_pred_def]
   198 declare size_list_def[symmetric, code_pred_inline]
   199 
   200 subsection {* Alternative rules for set *}
   201 
   202 lemma set_ConsI1 [code_pred_intro]:
   203   "set (x # xs) x"
   204 unfolding mem_def[symmetric, of _ x]
   205 by auto
   206 
   207 lemma set_ConsI2 [code_pred_intro]:
   208   "set xs x ==> set (x' # xs) x" 
   209 unfolding mem_def[symmetric, of _ x]
   210 by auto
   211 
   212 code_pred [skip_proof] set
   213 proof -
   214   case set
   215   from this show thesis
   216     apply (case_tac xb)
   217     apply auto
   218     unfolding mem_def[symmetric, of _ xc]
   219     apply auto
   220     unfolding mem_def
   221     apply fastsimp
   222     done
   223 qed
   224 
   225 subsection {* Alternative rules for list_all2 *}
   226 
   227 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   228 by auto
   229 
   230 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
   231 by auto
   232 
   233 code_pred [skip_proof] list_all2
   234 proof -
   235   case list_all2
   236   from this show thesis
   237     apply -
   238     apply (case_tac xb)
   239     apply (case_tac xc)
   240     apply auto
   241     apply (case_tac xc)
   242     apply auto
   243     apply fastsimp
   244     done
   245 qed
   246 
   247 section {* Setup for String.literal *}
   248 
   249 setup {* Predicate_Compile_Data.ignore_consts [@{const_name "STR"}] *}
   250 
   251 section {* Simplification rules for optimisation *}
   252 
   253 lemma [code_pred_simp]: "\<not> False == True"
   254 by auto
   255 
   256 lemma [code_pred_simp]: "\<not> True == False"
   257 by auto
   258 
   259 lemma less_nat_k_0 [code_pred_simp]: "less_nat k 0 == False"
   260 unfolding less_nat[symmetric] by auto
   261 
   262 
   263 end