src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
author bulwahn
Wed, 24 Mar 2010 17:40:43 +0100
changeset 35953 0460ff79bb52
child 36053 29e242e9e9a3
permissions -rw-r--r--
moved further predicate compile files to HOL-Library
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35953
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     1
theory Predicate_Compile_Alternative_Defs
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     2
imports "../Predicate_Compile"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     3
begin
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     4
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     5
section {* Common constants *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     6
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     7
declare HOL.if_bool_eq_disj[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     8
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
     9
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    10
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    11
section {* Pairs *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    12
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    13
setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    14
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    15
section {* Bounded quantifiers *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    16
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    17
declare Ball_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    18
declare Bex_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    19
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    20
section {* Set operations *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    21
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    22
declare Collect_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    23
declare mem_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    24
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    25
declare eq_reflection[OF empty_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    26
declare insert_code[code_pred_def]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    27
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    28
declare subset_iff[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    29
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    30
declare Int_def[code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    31
declare eq_reflection[OF Un_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    32
declare eq_reflection[OF UNION_def, code_pred_inline]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    33
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    34
lemma Diff[code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    35
  "(A - B) = (%x. A x \<and> \<not> B x)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    36
by (auto simp add: mem_def)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    37
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    38
lemma set_equality[code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    39
  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    40
by (fastsimp simp add: mem_def)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    41
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    42
section {* Setup for Numerals *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    43
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    44
setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    45
setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    46
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    47
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    48
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    49
subsection {* Inductive definitions for arithmetic on natural numbers *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    50
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    51
inductive plusP
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    52
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    53
  "plusP x 0 x"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    54
|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    55
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    56
setup {* Predicate_Compile_Fun.add_function_predicate_translation
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    57
  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    58
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    59
inductive less_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    60
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    61
  "less_nat 0 (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    62
| "less_nat x y ==> less_nat (Suc x) (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    63
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    64
lemma [code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    65
  "x < y = less_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    66
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    67
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    68
apply (case_tac y) apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    69
apply (case_tac y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    70
apply (auto intro: less_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    71
apply (induct rule: less_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    72
apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    73
done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    74
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    75
inductive less_eq_nat
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    76
where
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    77
  "less_eq_nat 0 y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    78
| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    79
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    80
lemma [code_pred_inline]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    81
"x <= y = less_eq_nat x y"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    82
apply (rule iffI)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    83
apply (induct x arbitrary: y)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    84
apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    85
apply (case_tac y) apply (auto intro: less_eq_nat.intros)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    86
apply (induct rule: less_eq_nat.induct)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    87
apply auto done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    88
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    89
section {* Alternative list definitions *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    90
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    91
text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    92
 
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    93
lemma [code_pred_def]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    94
  "length [] = 0"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    95
  "length (x # xs) = Suc (length xs)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    96
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    97
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    98
subsection {* Alternative rules for set *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
    99
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   100
lemma set_ConsI1 [code_pred_intro]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   101
  "set (x # xs) x"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   102
unfolding mem_def[symmetric, of _ x]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   103
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   104
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   105
lemma set_ConsI2 [code_pred_intro]:
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   106
  "set xs x ==> set (x' # xs) x" 
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   107
unfolding mem_def[symmetric, of _ x]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   108
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   109
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   110
code_pred [skip_proof] set
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   111
proof -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   112
  case set
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   113
  from this show thesis
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   114
    apply (case_tac xb)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   115
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   116
    unfolding mem_def[symmetric, of _ xc]
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   117
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   118
    unfolding mem_def
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   119
    apply fastsimp
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   120
    done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   121
qed
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   122
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   123
subsection {* Alternative rules for list_all2 *}
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   124
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   125
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   126
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   127
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   128
lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   129
by auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   130
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   131
code_pred [skip_proof] list_all2
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   132
proof -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   133
  case list_all2
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   134
  from this show thesis
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   135
    apply -
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   136
    apply (case_tac xb)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   137
    apply (case_tac xc)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   138
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   139
    apply (case_tac xc)
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   140
    apply auto
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   141
    apply fastsimp
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   142
    done
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   143
qed
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   144
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   145
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   146
0460ff79bb52 moved further predicate compile files to HOL-Library
bulwahn
parents:
diff changeset
   147
end