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