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