81 higher-order functions. The following set of lemmas specifies the |
81 higher-order functions. The following set of lemmas specifies the |
82 properties of such (extensional) arrays. |
82 properties of such (extensional) arrays. |
83 *} |
83 *} |
84 |
84 |
85 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def |
85 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def |
|
86 |
|
87 |
|
88 subsection {* Normalization *} |
|
89 |
|
90 lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" |
|
91 by simp |
|
92 |
|
93 lemma nat_int: "\<forall>n. nat (int n) = n" by simp |
|
94 lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp |
|
95 lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp |
|
96 |
|
97 lemma nat_zero_as_int: "0 = nat 0" by (rule transfer_nat_int_numerals(1)) |
|
98 lemma nat_one_as_int: "1 = nat 1" by (rule transfer_nat_int_numerals(2)) |
|
99 lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp |
|
100 lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp |
|
101 lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp |
|
102 lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp |
|
103 lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp |
|
104 lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp |
|
105 lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib) |
|
106 lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib) |
|
107 lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) |
|
108 |
|
109 lemma int_Suc: "int (Suc n) = int n + 1" by simp |
|
110 lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) |
|
111 lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto |
|
112 |
|
113 lemmas Ex1_def_raw = Ex1_def[abs_def] |
|
114 lemmas Ball_def_raw = Ball_def[abs_def] |
|
115 lemmas Bex_def_raw = Bex_def[abs_def] |
|
116 lemmas abs_if_raw = abs_if[abs_def] |
|
117 lemmas min_def_raw = min_def[abs_def] |
|
118 lemmas max_def_raw = max_def[abs_def] |
86 |
119 |
87 |
120 |
88 subsection {* Integer division and modulo for Z3 *} |
121 subsection {* Integer division and modulo for Z3 *} |
89 |
122 |
90 text {* |
123 text {* |