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