--- a/NEWS Wed Jul 15 15:09:33 2009 +0200
+++ b/NEWS Wed Jul 15 16:00:06 2009 +0200
@@ -28,6 +28,14 @@
* New type class boolean_algebra.
+* Refinements to lattices classes:
+ - added boolean_algebra type class
+ - less default intro/elim rules in locale variant, more default
+ intro/elim rules in class variant: more uniformity
+ - lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
+ - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
+ - renamed ACI to inf_sup_aci
+
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
--- a/src/HOL/Code_Eval.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Code_Eval.thy Wed Jul 15 16:00:06 2009 +0200
@@ -32,7 +32,7 @@
\<Rightarrow> 'a \<times> (unit \<Rightarrow> term) \<Rightarrow> 'b \<times> (unit \<Rightarrow> term)" where
"valapp f x = (fst f (fst x), \<lambda>u. App (snd f ()) (snd x ()))"
-lemma valapp_code [code, code_inline]:
+lemma valapp_code [code, code_unfold]:
"valapp (f, tf) (x, tx) = (f x, \<lambda>u. App (tf ()) (tx ()))"
by (simp only: valapp_def fst_conv snd_conv)
--- a/src/HOL/Code_Numeral.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Code_Numeral.thy Wed Jul 15 16:00:06 2009 +0200
@@ -176,13 +176,13 @@
end
-lemma zero_code_numeral_code [code_inline, code]:
+lemma zero_code_numeral_code [code, code_unfold]:
"(0\<Colon>code_numeral) = Numeral0"
by (simp add: number_of_code_numeral_def Pls_def)
lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
using zero_code_numeral_code ..
-lemma one_code_numeral_code [code_inline, code]:
+lemma one_code_numeral_code [code, code_unfold]:
"(1\<Colon>code_numeral) = Numeral1"
by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
lemma [code_post]: "Numeral1 = (1\<Colon>code_numeral)"
--- a/src/HOL/Finite_Set.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Finite_Set.thy Wed Jul 15 16:00:06 2009 +0200
@@ -812,7 +812,7 @@
by(rule fun_left_comm_idem.fold_insert_idem[OF ab_semigroup_idem_mult.fun_left_comm_idem[OF ab_semigroup_idem_mult_inf]])
lemma inf_le_fold_inf: "finite A \<Longrightarrow> ALL a:A. b \<le> a \<Longrightarrow> inf b c \<le> fold inf c A"
-by (induct pred:finite) auto
+by (induct pred: finite) (auto intro: le_infI1)
lemma fold_inf_le_inf: "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> fold inf b A \<le> inf a b"
proof(induct arbitrary: a pred:finite)
@@ -823,7 +823,7 @@
proof cases
assume "A = {}" thus ?thesis using insert by simp
next
- assume "A \<noteq> {}" thus ?thesis using insert by auto
+ assume "A \<noteq> {}" thus ?thesis using insert by (auto intro: le_infI2)
qed
qed
--- a/src/HOL/HOL.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/HOL.thy Wed Jul 15 16:00:06 2009 +0200
@@ -187,8 +187,8 @@
True_or_False: "(P=True) | (P=False)"
defs
- Let_def: "Let s f == f(s)"
- if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
+ Let_def [code]: "Let s f == f(s)"
+ if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"
finalconsts
"op ="
@@ -1029,8 +1029,8 @@
"(P ~= Q) = (P = (~Q))"
"(P | ~P) = True" "(~P | P) = True"
"(x = x) = True"
- and not_True_eq_False: "(\<not> True) = False"
- and not_False_eq_True: "(\<not> False) = True"
+ and not_True_eq_False [code]: "(\<not> True) = False"
+ and not_False_eq_True [code]: "(\<not> False) = True"
and
"(~P) ~= P" "P ~= (~P)"
"(True=P) = P"
@@ -1157,10 +1157,10 @@
text {* \medskip if-then-else rules *}
-lemma if_True: "(if True then x else y) = x"
+lemma if_True [code]: "(if True then x else y) = x"
by (unfold if_def) blast
-lemma if_False: "(if False then x else y) = y"
+lemma if_False [code]: "(if False then x else y) = y"
by (unfold if_def) blast
lemma if_P: "P ==> (if P then x else y) = x"
@@ -1722,6 +1722,7 @@
setup {*
Codegen.setup
#> RecfunCodegen.setup
+ #> Codegen.map_unfold (K HOL_basic_ss)
*}
types_code
@@ -1841,13 +1842,7 @@
and "x \<or> False \<longleftrightarrow> x"
and "x \<or> True \<longleftrightarrow> True" by simp_all
-lemma [code]:
- shows "\<not> True \<longleftrightarrow> False"
- and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+
-
-lemmas [code] = Let_def if_True if_False
-
-lemmas [code, code_unfold, symmetric, code_post] = imp_conv_disj
+declare imp_conv_disj [code, code_unfold_post]
instantiation itself :: (type) eq
begin
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Jul 15 16:00:06 2009 +0200
@@ -283,7 +283,7 @@
where
[code del]: "raise_exc e = raise []"
-lemma raise_raise_exc [code, code_inline]:
+lemma raise_raise_exc [code, code_unfold]:
"raise s = raise_exc (Fail (STR s))"
unfolding Fail_def raise_exc_def raise_def ..
--- a/src/HOL/Int.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Int.thy Wed Jul 15 16:00:06 2009 +0200
@@ -2126,11 +2126,11 @@
hide (open) const nat_aux
-lemma zero_is_num_zero [code, code_inline, symmetric, code_post]:
+lemma zero_is_num_zero [code, code_unfold_post]:
"(0\<Colon>int) = Numeral0"
by simp
-lemma one_is_num_one [code, code_inline, symmetric, code_post]:
+lemma one_is_num_one [code, code_unfold_post]:
"(1\<Colon>int) = Numeral1"
by simp
--- a/src/HOL/IntDiv.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/IntDiv.thy Wed Jul 15 16:00:06 2009 +0200
@@ -36,7 +36,7 @@
text{*algorithm for the general case @{term "b\<noteq>0"}*}
definition negateSnd :: "int \<times> int \<Rightarrow> int \<times> int" where
- [code_inline]: "negateSnd = apsnd uminus"
+ [code_unfold]: "negateSnd = apsnd uminus"
definition divmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
--{*The full division algorithm considers all possible signs for a, b
--- a/src/HOL/Lattices.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Lattices.thy Wed Jul 15 16:00:06 2009 +0200
@@ -44,38 +44,27 @@
context lower_semilattice
begin
-lemma le_infI1[intro]:
- assumes "a \<sqsubseteq> x"
- shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
- from assms show "a \<sqsubseteq> x" .
- show "a \<sqinter> b \<sqsubseteq> a" by simp
-qed
-lemmas (in -) [rule del] = le_infI1
+lemma le_infI1:
+ "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+ by (rule order_trans) auto
-lemma le_infI2[intro]:
- assumes "b \<sqsubseteq> x"
- shows "a \<sqinter> b \<sqsubseteq> x"
-proof (rule order_trans)
- from assms show "b \<sqsubseteq> x" .
- show "a \<sqinter> b \<sqsubseteq> b" by simp
-qed
-lemmas (in -) [rule del] = le_infI2
+lemma le_infI2:
+ "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+ by (rule order_trans) auto
-lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
-by(blast intro: inf_greatest)
-lemmas (in -) [rule del] = le_infI
+lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+ by (blast intro: inf_greatest)
-lemma le_infE [elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_infE
+lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+ by (blast intro: order_trans le_infI1 le_infI2)
lemma le_inf_iff [simp]:
- "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
-by blast
+ "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
+ by (blast intro: le_infI elim: le_infE)
-lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
- by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_inf:
+ "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
+ by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
lemma mono_inf:
fixes f :: "'a \<Rightarrow> 'b\<Colon>lower_semilattice"
@@ -87,28 +76,29 @@
context upper_semilattice
begin
-lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1:
+ "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI1
-lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2:
+ "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
by (rule order_trans) auto
-lemmas (in -) [rule del] = le_supI2
-lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI:
+ "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
by (blast intro: sup_least)
-lemmas (in -) [rule del] = le_supI
-lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
- by (blast intro: order_trans)
-lemmas (in -) [rule del] = le_supE
+lemma le_supE:
+ "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+ by (blast intro: le_supI1 le_supI2 order_trans)
-lemma ge_sup_conv[simp]:
- "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
-by blast
+lemma le_sup_iff [simp]:
+ "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+ by (blast intro: le_supI elim: le_supE)
-lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
- by (blast intro: antisym dest: eq_iff [THEN iffD1])
+lemma le_iff_sup:
+ "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
+ by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
lemma mono_sup:
fixes f :: "'a \<Rightarrow> 'b\<Colon>upper_semilattice"
@@ -118,62 +108,61 @@
end
-subsubsection{* Equational laws *}
+subsubsection {* Equational laws *}
context lower_semilattice
begin
lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_infI1 le_infI2)
lemma inf_idem[simp]: "x \<sqinter> x = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_left_idem[simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_infI2)
lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
- by (blast intro: antisym)
-
-lemmas inf_ACI = inf_commute inf_assoc inf_left_commute inf_left_idem
+ by (rule mk_left_commute [of inf]) (fact inf_assoc inf_commute)+
+
+lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
end
-
context upper_semilattice
begin
lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_supI1 le_supI2)
lemma sup_idem[simp]: "x \<squnion> x = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_left_idem[simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
- by (blast intro: antisym)
+ by (rule antisym) (auto intro: le_supI2)
lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_absorb2: "x \<sqsubseteq> y \<Longrightarrow> x \<squnion> y = y"
- by (blast intro: antisym)
+ by (rule antisym) auto
lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
- by (blast intro: antisym)
+ by (rule mk_left_commute [of sup]) (fact sup_assoc sup_commute)+
-lemmas sup_ACI = sup_commute sup_assoc sup_left_commute sup_left_idem
+lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem
end
@@ -191,18 +180,17 @@
lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
by (blast intro: antisym sup_ge1 sup_least inf_le1)
-lemmas ACI = inf_ACI sup_ACI
+lemmas inf_sup_aci = inf_aci sup_aci
lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
text{* Towards distributivity *}
lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
- by blast
+ by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
- by blast
-
+ by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
text{* If you have one of them, you have them all. *}
@@ -230,10 +218,6 @@
finally show ?thesis .
qed
-(* seems unused *)
-lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
-by blast
-
end
@@ -247,7 +231,7 @@
lemma sup_inf_distrib2:
"(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
-by(simp add:ACI sup_inf_distrib1)
+by(simp add: inf_sup_aci sup_inf_distrib1)
lemma inf_sup_distrib1:
"x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -255,7 +239,7 @@
lemma inf_sup_distrib2:
"(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
-by(simp add:ACI inf_sup_distrib1)
+by(simp add: inf_sup_aci inf_sup_distrib1)
lemma dual_distrib_lattice:
"distrib_lattice (op \<ge>) (op >) sup inf"
@@ -458,16 +442,6 @@
lemmas min_ac = min_max.inf_assoc min_max.inf_commute
mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
-text {*
- Now we have inherited antisymmetry as an intro-rule on all
- linear orders. This is a problem because it applies to bool, which is
- undesirable.
-*}
-
-lemmas [rule del] = min_max.le_infI min_max.le_supI
- min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
- min_max.le_infI1 min_max.le_infI2
-
subsection {* Bool as lattice *}
@@ -548,8 +522,6 @@
text {* redundant bindings *}
-lemmas inf_aci = inf_ACI
-lemmas sup_aci = sup_ACI
no_notation
less_eq (infix "\<sqsubseteq>" 50) and
--- a/src/HOL/Library/Code_Char_chr.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Wed Jul 15 16:00:06 2009 +0200
@@ -24,11 +24,11 @@
lemmas [code del] = char.recs char.cases char.size
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
-lemma [code, code_inline]:
+lemma [code, code_unfold]:
"char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
by (cases c) (auto simp add: nibble_pair_of_nat_char)
--- a/src/HOL/Library/Efficient_Nat.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Wed Jul 15 16:00:06 2009 +0200
@@ -26,15 +26,13 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code_inline]:
+lemma zero_nat_code [code, code_unfold_post]:
"0 = (Numeral0 :: nat)"
by simp
-lemmas [code_post] = zero_nat_code [symmetric]
-lemma one_nat_code [code, code_inline]:
+lemma one_nat_code [code, code_unfold_post]:
"1 = (Numeral1 :: nat)"
by simp
-lemmas [code_post] = one_nat_code [symmetric]
lemma Suc_code [code]:
"Suc n = n + 1"
@@ -302,7 +300,7 @@
Natural numerals.
*}
-lemma [code_inline, symmetric, code_post]:
+lemma [code_unfold_post]:
"nat (number_of i) = number_nat_inst.number_of_nat i"
-- {* this interacts as desired with @{thm nat_number_of_def} *}
by (simp add: number_nat_inst.number_of_nat)
@@ -322,9 +320,7 @@
returns @{text "0"}.
*}
-definition
- int :: "nat \<Rightarrow> int"
-where
+definition int :: "nat \<Rightarrow> int" where
[code del]: "int = of_nat"
lemma int_code' [code]:
@@ -335,9 +331,12 @@
"nat (number_of l) = (if neg (number_of l \<Colon> int) then 0 else number_of l)"
unfolding nat_number_of_def number_of_is_id neg_def by simp
-lemma of_nat_int [code_unfold]:
+lemma of_nat_int [code_unfold_post]:
"of_nat = int" by (simp add: int_def)
-declare of_nat_int [symmetric, code_post]
+
+lemma of_nat_aux_int [code_unfold]:
+ "of_nat_aux (\<lambda>i. i + 1) k 0 = int k"
+ by (simp add: int_def Nat.of_nat_code)
code_const int
(SML "_")
--- a/src/HOL/Library/Float.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Library/Float.thy Wed Jul 15 16:00:06 2009 +0200
@@ -42,7 +42,7 @@
instance ..
end
-lemma number_of_float_Float [code_inline, symmetric, code_post]:
+lemma number_of_float_Float [code_unfold_post]:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
--- a/src/HOL/Library/Nat_Infinity.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Wed Jul 15 16:00:06 2009 +0200
@@ -40,10 +40,10 @@
"0 = Fin 0"
definition
- [code_inline]: "1 = Fin 1"
+ [code_unfold]: "1 = Fin 1"
definition
- [code_inline, code del]: "number_of k = Fin (number_of k)"
+ [code_unfold, code del]: "number_of k = Fin (number_of k)"
instance ..
--- a/src/HOL/List.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/List.thy Wed Jul 15 16:00:06 2009 +0200
@@ -3760,7 +3760,7 @@
"xs = [] \<longleftrightarrow> null xs"
by (cases xs) simp_all
-lemma [code_inline]:
+lemma [code_unfold]:
"eq_class.eq xs [] \<longleftrightarrow> null xs"
by (simp add: eq empty_null)
@@ -3808,7 +3808,7 @@
"map_filter f P xs = map f (filter P xs)"
by (induct xs) auto
-lemma length_remdups_length_unique [code_inline]:
+lemma length_remdups_length_unique [code_unfold]:
"length (remdups xs) = length_unique xs"
by (induct xs) simp_all
--- a/src/HOL/Nat_Numeral.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Wed Jul 15 16:00:06 2009 +0200
@@ -20,7 +20,7 @@
begin
definition
- nat_number_of_def [code_inline, code del]: "number_of v = nat (number_of v)"
+ nat_number_of_def [code_unfold, code del]: "number_of v = nat (number_of v)"
instance ..
--- a/src/HOL/Option.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Option.thy Wed Jul 15 16:00:06 2009 +0200
@@ -105,7 +105,7 @@
"is_none x \<longleftrightarrow> x = None"
by (simp add: is_none_def)
-lemma [code_inline]:
+lemma [code_unfold]:
"eq_class.eq x None \<longleftrightarrow> is_none x"
by (simp add: eq is_none_none)
--- a/src/HOL/OrderedGroup.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Wed Jul 15 16:00:06 2009 +0200
@@ -1075,16 +1075,16 @@
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def)
lemma pprt_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
lemma pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0"
-by (simp add: pprt_def le_iff_sup sup_ACI)
+by (simp add: pprt_def le_iff_sup sup_aci)
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0"
-by (simp add: nprt_def le_iff_inf inf_ACI)
+by (simp add: nprt_def le_iff_inf inf_aci)
lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
proof -
@@ -1120,7 +1120,7 @@
assume "0 <= a + a"
hence a:"inf (a+a) 0 = 0" by (simp add: le_iff_inf inf_commute)
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
- by (simp add: add_sup_inf_distribs inf_ACI)
+ by (simp add: add_sup_inf_distribs inf_aci)
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
hence "inf a 0 = 0" by (simp only: add_right_cancel)
then show "0 <= a" by (simp add: le_iff_inf inf_commute)
@@ -1206,10 +1206,10 @@
by (simp add: le_iff_inf nprt_def inf_commute)
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b"
-by (simp add: le_iff_sup pprt_def sup_ACI sup_assoc [symmetric, of a])
+by (simp add: le_iff_sup pprt_def sup_aci sup_assoc [symmetric, of a])
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b"
-by (simp add: le_iff_inf nprt_def inf_ACI inf_assoc [symmetric, of a])
+by (simp add: le_iff_inf nprt_def inf_aci inf_assoc [symmetric, of a])
end
@@ -1230,7 +1230,7 @@
then have "0 \<le> sup a (- a)" unfolding abs_lattice .
then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
then show ?thesis
- by (simp add: add_sup_inf_distribs sup_ACI
+ by (simp add: add_sup_inf_distribs sup_aci
pprt_def nprt_def diff_minus abs_lattice)
qed
@@ -1254,7 +1254,7 @@
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
proof -
have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
- by (simp add: abs_lattice add_sup_inf_distribs sup_ACI diff_minus)
+ by (simp add: abs_lattice add_sup_inf_distribs sup_aci diff_minus)
have a:"a+b <= sup ?m ?n" by (simp)
have b:"-a-b <= ?n" by (simp)
have c:"?n <= sup ?m ?n" by (simp)
--- a/src/HOL/Rational.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Rational.thy Wed Jul 15 16:00:06 2009 +0200
@@ -1003,7 +1003,7 @@
definition (in term_syntax)
valterm_fract :: "int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> int \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> rat \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code_inline]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
+ [code_unfold]: "valterm_fract k l = Code_Eval.valtermify Fract {\<cdot>} k {\<cdot>} l"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/RealDef.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/RealDef.thy Wed Jul 15 16:00:06 2009 +0200
@@ -946,7 +946,7 @@
end
-lemma [code_unfold, symmetric, code_post]:
+lemma [code_unfold_post]:
"number_of k = real_of_int (number_of k)"
unfolding number_of_is_id real_number_of_def ..
@@ -1129,7 +1129,7 @@
definition (in term_syntax)
valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
- [code_inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+ [code_unfold]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
notation fcomp (infixl "o>" 60)
notation scomp (infixl "o\<rightarrow>" 60)
--- a/src/HOL/SEQ.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/SEQ.thy Wed Jul 15 16:00:06 2009 +0200
@@ -113,8 +113,8 @@
lemma Bseq_conv_Bfun: "Bseq X \<longleftrightarrow> Bfun X sequentially"
unfolding Bfun_def eventually_sequentially
apply (rule iffI)
-apply (simp add: Bseq_def, fast)
-apply (fast intro: BseqI2')
+apply (simp add: Bseq_def)
+apply (auto intro: BseqI2')
done
@@ -762,13 +762,25 @@
lemma lemma_NBseq_def:
"(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) =
(\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
-apply auto
- prefer 2 apply force
-apply (cut_tac x = K in reals_Archimedean2, clarify)
-apply (rule_tac x = n in exI, clarify)
-apply (drule_tac x = na in spec)
-apply (auto simp add: real_of_nat_Suc)
-done
+proof auto
+ fix K :: real
+ from reals_Archimedean2 obtain n :: nat where "K < real n" ..
+ then have "K \<le> real (Suc n)" by auto
+ assume "\<forall>m. norm (X m) \<le> K"
+ have "\<forall>m. norm (X m) \<le> real (Suc n)"
+ proof
+ fix m :: 'a
+ from `\<forall>m. norm (X m) \<le> K` have "norm (X m) \<le> K" ..
+ with `K \<le> real (Suc n)` show "norm (X m) \<le> real (Suc n)" by auto
+ qed
+ then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
+next
+ fix N :: nat
+ have "real (Suc N) > 0" by (simp add: real_of_nat_Suc)
+ moreover assume "\<forall>n. norm (X n) \<le> real (Suc N)"
+ ultimately show "\<exists>K>0. \<forall>n. norm (X n) \<le> K" by blast
+qed
+
text{* alternative definition for Bseq *}
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -1105,7 +1117,7 @@
lemma (in real_Cauchy) isLub_ex: "\<exists>u. isLub UNIV S u"
proof (rule reals_complete)
obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (X m - X n) < 1"
- using CauchyD [OF X zero_less_one] by fast
+ using CauchyD [OF X zero_less_one] by auto
hence N: "\<forall>n\<ge>N. norm (X n - X N) < 1" by simp
show "\<exists>x. x \<in> S"
proof
@@ -1129,7 +1141,7 @@
fix r::real assume "0 < r"
hence r: "0 < r/2" by simp
obtain N where "\<forall>n\<ge>N. \<forall>m\<ge>N. norm (X n - X m) < r/2"
- using CauchyD [OF X r] by fast
+ using CauchyD [OF X r] by auto
hence "\<forall>n\<ge>N. norm (X n - X N) < r/2" by simp
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
by (simp only: real_norm_def real_abs_diff_less_iff)
--- a/src/HOL/Set.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/Set.thy Wed Jul 15 16:00:06 2009 +0200
@@ -2249,10 +2249,10 @@
unfolding Inf_Sup by auto
lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
- by (auto intro: antisym Inf_greatest Inf_lower)
+ by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
- by (auto intro: antisym Sup_least Sup_upper)
+ by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma Inf_singleton [simp]:
"\<Sqinter>{a} = a"
--- a/src/HOL/String.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/String.thy Wed Jul 15 16:00:06 2009 +0200
@@ -58,11 +58,11 @@
end
*}
-lemma char_case_nibble_pair [code, code_inline]:
+lemma char_case_nibble_pair [code, code_unfold]:
"char_case f = split f o nibble_pair_of_char"
by (simp add: expand_fun_eq split: char.split)
-lemma char_rec_nibble_pair [code, code_inline]:
+lemma char_rec_nibble_pair [code, code_unfold]:
"char_rec f = split f o nibble_pair_of_char"
unfolding char_case_nibble_pair [symmetric]
by (simp add: expand_fun_eq split: char.split)
--- a/src/HOL/ex/Eval_Examples.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Wed Jul 15 16:00:06 2009 +0200
@@ -3,7 +3,7 @@
header {* Small examples for evaluation mechanisms *}
theory Eval_Examples
-imports Code_Eval Rational
+imports Complex_Main
begin
text {* evaluation oracle *}
--- a/src/HOL/ex/Numeral.thy Wed Jul 15 15:09:33 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Wed Jul 15 16:00:06 2009 +0200
@@ -758,7 +758,7 @@
code_datatype "0::int" Pls Mns
-lemmas [code_inline] = Pls_def [symmetric] Mns_def [symmetric]
+lemmas [code_unfold] = Pls_def [symmetric] Mns_def [symmetric]
definition sub :: "num \<Rightarrow> num \<Rightarrow> int" where
[simp, code del]: "sub m n = (of_num m - of_num n)"
@@ -874,10 +874,10 @@
using of_num_pos [of l, where ?'a = int] of_num_pos [of k, where ?'a = int]
by (simp_all add: of_num_less_iff)
-lemma [code_inline del]: "(0::int) \<equiv> Numeral0" by simp
-lemma [code_inline del]: "(1::int) \<equiv> Numeral1" by simp
-declare zero_is_num_zero [code_inline del]
-declare one_is_num_one [code_inline del]
+lemma [code_unfold del]: "(0::int) \<equiv> Numeral0" by simp
+lemma [code_unfold del]: "(1::int) \<equiv> Numeral1" by simp
+declare zero_is_num_zero [code_unfold del]
+declare one_is_num_one [code_unfold del]
hide (open) const sub dup
--- a/src/Pure/Isar/code.ML Wed Jul 15 15:09:33 2009 +0200
+++ b/src/Pure/Isar/code.ML Wed Jul 15 16:00:06 2009 +0200
@@ -886,7 +886,9 @@
of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
| NONE => thy;
-structure Code_Attr = TheoryDataFun (
+(* c.f. src/HOL/Tools/recfun_codegen.ML *)
+
+structure Code_Target_Attr = TheoryDataFun (
type T = (string -> thm -> theory -> theory) option;
val empty = NONE;
val copy = I;
@@ -895,7 +897,14 @@
| merge _ (f1, _) = f1;
);
-fun set_code_target_attr f = Code_Attr.map (K (SOME f));
+fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
+
+fun code_target_attr prefix thm thy =
+ let
+ val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
+ in thy |> add_warning_eqn thm |> attr prefix thm end;
+
+(* setup *)
val _ = Context.>> (Context.map_theory
(let
@@ -904,9 +913,7 @@
Args.del |-- Scan.succeed (mk_attribute del_eqn)
|| Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
|| (Args.$$$ "target" |-- Args.colon |-- Args.name >>
- (fn prefix => mk_attribute (fn thm => fn thy => thy
- |> add_warning_eqn thm
- |> the_default ((K o K) I) (Code_Attr.get thy) prefix thm)))
+ (mk_attribute o code_target_attr))
|| Scan.succeed (mk_attribute add_warning_eqn);
in
Type_Interpretation.init
--- a/src/Pure/codegen.ML Wed Jul 15 15:09:33 2009 +0200
+++ b/src/Pure/codegen.ML Wed Jul 15 16:00:06 2009 +0200
@@ -85,7 +85,9 @@
val num_args_of: 'a mixfix list -> int
val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
val mk_deftab: theory -> deftab
+ val map_unfold: (simpset -> simpset) -> theory -> theory
val add_unfold: thm -> theory -> theory
+ val del_unfold: thm -> theory -> theory
val get_node: codegr -> string -> node
val add_edge: string * string -> codegr -> codegr
@@ -296,13 +298,9 @@
fun merge _ = merge_ss;
);
-fun add_unfold eqn =
- let
- val ctxt = ProofContext.init (Thm.theory_of_thm eqn);
- val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn;
- in
- UnfoldData.map (fn ss => ss addsimps [eqn'])
- end;
+val map_unfold = UnfoldData.map;
+val add_unfold = map_unfold o MetaSimplifier.add_simp;
+val del_unfold = map_unfold o MetaSimplifier.del_simp;
fun unfold_preprocessor thy =
let val ss = Simplifier.theory_context thy (UnfoldData.get thy)
--- a/src/Tools/Code/code_preproc.ML Wed Jul 15 15:09:33 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Jul 15 16:00:06 2009 +0200
@@ -9,7 +9,7 @@
sig
val map_pre: (simpset -> simpset) -> theory -> theory
val map_post: (simpset -> simpset) -> theory -> theory
- val add_inline: thm -> theory -> theory
+ val add_unfold: thm -> theory -> theory
val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory
val del_functrans: string -> theory -> theory
val simple_functrans: (theory -> thm list -> thm list option)
@@ -77,14 +77,24 @@
|> Code.purge_data
|> (Code_Preproc_Data.map o map_thmproc) f;
-val map_pre = map_data o apfst o apfst;
-val map_post = map_data o apfst o apsnd;
+val map_pre_post = map_data o apfst;
+val map_pre = map_pre_post o apfst;
+val map_post = map_pre_post o apsnd;
-val add_inline = map_pre o MetaSimplifier.add_simp;
-val del_inline = map_pre o MetaSimplifier.del_simp;
+val add_unfold = map_pre o MetaSimplifier.add_simp;
+val del_unfold = map_pre o MetaSimplifier.del_simp;
val add_post = map_post o MetaSimplifier.add_simp;
val del_post = map_post o MetaSimplifier.del_simp;
-
+
+fun add_unfold_post raw_thm thy =
+ let
+ val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+ val thm_sym = Thm.symmetric thm;
+ in
+ thy |> map_pre_post (fn (pre, post) =>
+ (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym))
+ end;
+
fun add_functrans (name, f) = (map_data o apsnd)
(AList.update (op =) (name, (serial (), f)));
@@ -526,16 +536,19 @@
val setup =
let
fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
- fun add_del_attribute_parser (add, del) =
+ fun add_del_attribute_parser add del =
Attrib.add_del (mk_attribute add) (mk_attribute del);
+ fun both f g thm = f thm #> g thm;
in
- Attrib.setup @{binding code_inline} (add_del_attribute_parser (add_inline, del_inline))
+ Attrib.setup @{binding code_unfold} (add_del_attribute_parser
+ (both Codegen.add_unfold add_unfold) (both Codegen.del_unfold del_unfold))
+ "preprocessing equations for code generators"
+ #> Attrib.setup @{binding code_inline} (add_del_attribute_parser add_unfold del_unfold)
"preprocessing equations for code generator"
- #> Attrib.setup @{binding code_post} (add_del_attribute_parser (add_post, del_post))
+ #> Attrib.setup @{binding code_post} (add_del_attribute_parser add_post del_post)
"postprocessing equations for code generator"
- #> Attrib.setup @{binding code_unfold} (Scan.succeed (mk_attribute
- (fn thm => Codegen.add_unfold thm #> add_inline thm)))
- "preprocessing equations for code generators"
+ #> Attrib.setup @{binding code_unfold_post} (Scan.succeed (mk_attribute add_unfold_post))
+ "pre- and postprocessing equations for code generator"
end;
val _ =