--- a/NEWS Mon Jul 20 00:37:39 2009 +0200
+++ b/NEWS Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Code_Eval.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Code_Numeral.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/HOL.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Int.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/IntDiv.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Lattices.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Library/Code_Char_chr.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Library/Float.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/List.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Nat_Numeral.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Option.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/OrderedGroup.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Rational.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/RealDef.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/SEQ.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/Set.thy Mon Jul 20 13:52:27 2009 +0200
@@ -10,7 +10,7 @@
text {* A set in HOL is simply a predicate. *}
-subsection {* Basic syntax *}
+subsection {* Basic definitions and syntax *}
global
@@ -19,9 +19,6 @@
consts
Collect :: "('a => bool) => 'a set" -- "comprehension"
"op :" :: "'a => 'a set => bool" -- "membership"
- Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
- Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
- Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers"
local
@@ -29,6 +26,10 @@
"op :" ("op :") and
"op :" ("(_/ : _)" [50, 51] 50)
+defs
+ mem_def [code]: "x : S == S x"
+ Collect_def [code]: "Collect P == P"
+
abbreviation
"not_mem x A == ~ (x : A)" -- "non-membership"
@@ -84,6 +85,20 @@
"{x, xs}" == "CONST insert x {xs}"
"{x}" == "CONST insert x {}"
+global
+
+consts
+ Ball :: "'a set => ('a => bool) => bool" -- "bounded universal quantifiers"
+ Bex :: "'a set => ('a => bool) => bool" -- "bounded existential quantifiers"
+ Bex1 :: "'a set => ('a => bool) => bool" -- "bounded unique existential quantifiers"
+
+local
+
+defs
+ Ball_def: "Ball A P == ALL x. x:A --> P(x)"
+ Bex_def: "Bex A P == EX x. x:A & P(x)"
+ Bex1_def: "Bex1 A P == EX! x. x:A & P(x)"
+
syntax
"_Ball" :: "pttrn => 'a set => bool => bool" ("(3ALL _:_./ _)" [0, 0, 10] 10)
"_Bex" :: "pttrn => 'a set => bool => bool" ("(3EX _:_./ _)" [0, 0, 10] 10)
@@ -112,65 +127,18 @@
"EX! x:A. P" == "Bex1 A (%x. P)"
"LEAST x:A. P" => "LEAST x. x:A & P"
-definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
-
-definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
- "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
-
-definition Inter :: "'a set set \<Rightarrow> 'a set" where
- "Inter S \<equiv> INTER S (\<lambda>x. x)"
-
-definition Union :: "'a set set \<Rightarrow> 'a set" where
- "Union S \<equiv> UNION S (\<lambda>x. x)"
-
-notation (xsymbols)
- Inter ("\<Inter>_" [90] 90) and
- Union ("\<Union>_" [90] 90)
-
subsection {* Additional concrete syntax *}
syntax
"@SetCompr" :: "'a => idts => bool => 'a set" ("(1{_ |/_./ _})")
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ :/ _./ _})")
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
syntax (xsymbols)
"@Collect" :: "idt => 'a set => bool => 'a set" ("(1{_ \<in>/ _./ _})")
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
-
-syntax (latex output)
- "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
- "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
translations
"{x:A. P}" => "{x. x:A & P}"
- "INT x y. B" == "INT x. INT y. B"
- "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
- "INT x. B" == "INT x:CONST UNIV. B"
- "INT x:A. B" == "CONST INTER A (%x. B)"
- "UN x y. B" == "UN x. UN y. B"
- "UN x. B" == "CONST UNION CONST UNIV (%x. B)"
- "UN x. B" == "UN x:CONST UNIV. B"
- "UN x:A. B" == "CONST UNION A (%x. B)"
-
-text {*
- Note the difference between ordinary xsymbol syntax of indexed
- unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
- and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
- former does not make the index expression a subscript of the
- union/intersection symbol because this leads to problems with nested
- subscripts in Proof General.
-*}
abbreviation
subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -313,10 +281,7 @@
fun btr' syn [A, Abs abs] =
let val (x, t) = atomic_abs_tr' abs
in Syntax.const syn $ x $ A $ t end
-in
-[(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex"),
- (@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")]
-end
+in [(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex")] end
*}
print_translation {*
@@ -349,30 +314,6 @@
*}
-subsection {* Rules and definitions *}
-
-text {* Isomorphisms between predicates and sets. *}
-
-defs
- mem_def [code]: "x : S == S x"
- Collect_def [code]: "Collect P == P"
-
-defs
- Ball_def: "Ball A P == ALL x. x:A --> P(x)"
- Bex_def: "Bex A P == EX x. x:A & P(x)"
- Bex1_def: "Bex1 A P == EX! x. x:A & P(x)"
-
-definition Pow :: "'a set => 'a set set" where
- Pow_def: "Pow A = {B. B \<le> A}"
-
-definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
- image_def: "f ` A = {y. EX x:A. y = f(x)}"
-
-abbreviation
- range :: "('a => 'b) => 'b set" where -- "of function"
- "range f == f ` UNIV"
-
-
subsection {* Lemmas and proof tool setup *}
subsubsection {* Relating predicates and sets *}
@@ -671,6 +612,9 @@
subsubsection {* The Powerset operator -- Pow *}
+definition Pow :: "'a set => 'a set set" where
+ Pow_def: "Pow A = {B. B \<le> A}"
+
lemma Pow_iff [iff]: "(A \<in> Pow B) = (A \<subseteq> B)"
by (simp add: Pow_def)
@@ -846,12 +790,397 @@
by (blast elim: equalityE)
-subsubsection {* Unions of families *}
+subsubsection {* Image of a set under a function *}
+
+text {*
+ Frequently @{term b} does not have the syntactic form of @{term "f x"}.
+*}
+
+definition image :: "('a => 'b) => 'a set => 'b set" (infixr "`" 90) where
+ image_def [noatp]: "f ` A = {y. EX x:A. y = f(x)}"
+
+abbreviation
+ range :: "('a => 'b) => 'b set" where -- "of function"
+ "range f == f ` UNIV"
+
+lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
+ by (unfold image_def) blast
+
+lemma imageI: "x : A ==> f x : f ` A"
+ by (rule image_eqI) (rule refl)
+
+lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
+ -- {* This version's more effective when we already have the
+ required @{term x}. *}
+ by (unfold image_def) blast
+
+lemma imageE [elim!]:
+ "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
+ -- {* The eta-expansion gives variable-name preservation. *}
+ by (unfold image_def) blast
+
+lemma image_Un: "f`(A Un B) = f`A Un f`B"
+ by blast
+
+lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
+ by blast
+
+lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+ -- {* This rewrite rule would confuse users if made default. *}
+ by blast
+
+lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
+ apply safe
+ prefer 2 apply fast
+ apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
+ done
+
+lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
+ -- {* Replaces the three steps @{text subsetI}, @{text imageE},
+ @{text hypsubst}, but breaks too many existing proofs. *}
+ by blast
text {*
- @{term [source] "UN x:A. B x"} is @{term "Union (B`A)"}.
+ \medskip Range of a function -- just a translation for image!
+*}
+
+lemma range_eqI: "b = f x ==> b \<in> range f"
+ by simp
+
+lemma rangeI: "f x \<in> range f"
+ by simp
+
+lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
+ by blast
+
+
+subsection {* Complete lattices *}
+
+notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65)
+
+class complete_lattice = lattice + bot + top +
+ fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+ and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+ assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
+ and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
+ assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
+ and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
+begin
+
+lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
+ by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
+lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
+ by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
+
+lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
+ unfolding Sup_Inf by (auto simp add: UNIV_def)
+
+lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
+ unfolding Inf_Sup by (auto simp add: UNIV_def)
+
+lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+ 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: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
+
+lemma Inf_singleton [simp]:
+ "\<Sqinter>{a} = a"
+ by (auto intro: antisym Inf_lower Inf_greatest)
+
+lemma Sup_singleton [simp]:
+ "\<Squnion>{a} = a"
+ by (auto intro: antisym Sup_upper Sup_least)
+
+lemma Inf_insert_simp:
+ "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
+ by (cases "A = {}") (simp_all, simp add: Inf_insert)
+
+lemma Sup_insert_simp:
+ "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
+ by (cases "A = {}") (simp_all, simp add: Sup_insert)
+
+lemma Inf_binary:
+ "\<Sqinter>{a, b} = a \<sqinter> b"
+ by (auto simp add: Inf_insert_simp)
+
+lemma Sup_binary:
+ "\<Squnion>{a, b} = a \<squnion> b"
+ by (auto simp add: Sup_insert_simp)
+
+lemma bot_def:
+ "bot = \<Squnion>{}"
+ by (auto intro: antisym Sup_least)
+
+lemma top_def:
+ "top = \<Sqinter>{}"
+ by (auto intro: antisym Inf_greatest)
+
+lemma sup_bot [simp]:
+ "x \<squnion> bot = x"
+ using bot_least [of x] by (simp add: le_iff_sup sup_commute)
+
+lemma inf_top [simp]:
+ "x \<sqinter> top = x"
+ using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
+
+definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "SUPR A f == \<Squnion> (f ` A)"
+
+definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
+ "INFI A f == \<Sqinter> (f ` A)"
+
+end
+
+syntax
+ "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
+ "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
+ "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
+
+translations
+ "SUP x y. B" == "SUP x. SUP y. B"
+ "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
+ "SUP x. B" == "SUP x:CONST UNIV. B"
+ "SUP x:A. B" == "CONST SUPR A (%x. B)"
+ "INF x y. B" == "INF x. INF y. B"
+ "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
+ "INF x. B" == "INF x:CONST UNIV. B"
+ "INF x:A. B" == "CONST INFI A (%x. B)"
+
+(* To avoid eta-contraction of body: *)
+print_translation {*
+let
+ fun btr' syn (A :: Abs abs :: ts) =
+ let val (x,t) = atomic_abs_tr' abs
+ in list_comb (Syntax.const syn $ x $ A $ t, ts) end
+ val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
+in
+[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
+end
*}
+context complete_lattice
+begin
+
+lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
+ by (auto simp add: SUPR_def intro: Sup_upper)
+
+lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
+ by (auto simp add: SUPR_def intro: Sup_least)
+
+lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
+ by (auto simp add: INFI_def intro: Inf_lower)
+
+lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
+ by (auto simp add: INFI_def intro: Inf_greatest)
+
+lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
+ by (auto intro: antisym SUP_leI le_SUPI)
+
+lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
+ by (auto intro: antisym INF_leI le_INFI)
+
+end
+
+
+subsection {* Bool as complete lattice *}
+
+instantiation bool :: complete_lattice
+begin
+
+definition
+ Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
+
+definition
+ Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
+
+instance proof
+qed (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
+
+end
+
+lemma Inf_empty_bool [simp]:
+ "\<Sqinter>{}"
+ unfolding Inf_bool_def by auto
+
+lemma not_Sup_empty_bool [simp]:
+ "\<not> \<Squnion>{}"
+ unfolding Sup_bool_def by auto
+
+
+subsection {* Fun as complete lattice *}
+
+instantiation "fun" :: (type, complete_lattice) complete_lattice
+begin
+
+definition
+ Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+
+definition
+ Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+
+instance proof
+qed (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
+ intro: Inf_lower Sup_upper Inf_greatest Sup_least)
+
+end
+
+lemma Inf_empty_fun:
+ "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
+ by rule (simp add: Inf_fun_def, simp add: empty_def)
+
+lemma Sup_empty_fun:
+ "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
+ by rule (simp add: Sup_fun_def, simp add: empty_def)
+
+
+subsection {* Set as lattice *}
+
+definition INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "INTER A B \<equiv> {y. \<forall>x\<in>A. y \<in> B x}"
+
+definition UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
+ "UNION A B \<equiv> {y. \<exists>x\<in>A. y \<in> B x}"
+
+definition Inter :: "'a set set \<Rightarrow> 'a set" where
+ "Inter S \<equiv> INTER S (\<lambda>x. x)"
+
+definition Union :: "'a set set \<Rightarrow> 'a set" where
+ "Union S \<equiv> UNION S (\<lambda>x. x)"
+
+notation (xsymbols)
+ Inter ("\<Inter>_" [90] 90) and
+ Union ("\<Union>_" [90] 90)
+
+syntax
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
+
+syntax (xsymbols)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
+
+syntax (latex output)
+ "@INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "@UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+ "@INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "@UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+
+translations
+ "INT x y. B" == "INT x. INT y. B"
+ "INT x. B" == "CONST INTER CONST UNIV (%x. B)"
+ "INT x. B" == "INT x:CONST UNIV. B"
+ "INT x:A. B" == "CONST INTER A (%x. B)"
+ "UN x y. B" == "UN x. UN y. B"
+ "UN x. B" == "CONST UNION CONST UNIV (%x. B)"
+ "UN x. B" == "UN x:CONST UNIV. B"
+ "UN x:A. B" == "CONST UNION A (%x. B)"
+
+text {*
+ Note the difference between ordinary xsymbol syntax of indexed
+ unions and intersections (e.g.\ @{text"\<Union>a\<^isub>1\<in>A\<^isub>1. B"})
+ and their \LaTeX\ rendition: @{term"\<Union>a\<^isub>1\<in>A\<^isub>1. B"}. The
+ former does not make the index expression a subscript of the
+ union/intersection symbol because this leads to problems with nested
+ subscripts in Proof General.
+*}
+
+(* To avoid eta-contraction of body: *)
+print_translation {*
+let
+ fun btr' syn [A, Abs abs] =
+ let val (x, t) = atomic_abs_tr' abs
+ in Syntax.const syn $ x $ A $ t end
+in [(@{const_syntax UNION}, btr' "@UNION"),(@{const_syntax INTER}, btr' "@INTER")] end
+*}
+
+lemma Inter_image_eq [simp]:
+ "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
+ by (auto simp add: Inter_def INTER_def image_def)
+
+lemma Union_image_eq [simp]:
+ "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
+ by (auto simp add: Union_def UNION_def image_def)
+
+lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
+ by (simp add: inf_fun_eq inf_bool_eq Int_def Collect_def mem_def)
+
+lemma sup_set_eq: "A \<squnion> B = A \<union> B"
+ by (simp add: sup_fun_eq sup_bool_eq Un_def Collect_def mem_def)
+
+lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
+ apply (fold inf_set_eq sup_set_eq)
+ apply (erule mono_inf)
+ done
+
+lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
+ apply (fold inf_set_eq sup_set_eq)
+ apply (erule mono_sup)
+ done
+
+lemma top_set_eq: "top = UNIV"
+ by (iprover intro!: subset_antisym subset_UNIV top_greatest)
+
+lemma bot_set_eq: "bot = {}"
+ by (iprover intro!: subset_antisym empty_subsetI bot_least)
+
+lemma Inter_eq:
+ "\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
+ by (simp add: Inter_def INTER_def)
+
+lemma Union_eq:
+ "\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
+ by (simp add: Union_def UNION_def)
+
+lemma Inf_set_eq:
+ "\<Sqinter>S = \<Inter>S"
+proof (rule set_ext)
+ fix x
+ have "(\<forall>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<forall>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Sqinter>S \<longleftrightarrow> x \<in> \<Inter>S"
+ by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def)
+qed
+
+lemma Sup_set_eq:
+ "\<Squnion>S = \<Union>S"
+proof (rule set_ext)
+ fix x
+ have "(\<exists>Q\<in>{P. \<exists>A\<in>S. P \<longleftrightarrow> x \<in> A}. Q) \<longleftrightarrow> (\<exists>A\<in>S. x \<in> A)"
+ by auto
+ then show "x \<in> \<Squnion>S \<longleftrightarrow> x \<in> \<Union>S"
+ by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def)
+qed
+
+lemma INFI_set_eq:
+ "(INF x:S. f x) = (\<Inter>x\<in>S. f x)"
+ by (simp add: INFI_def Inf_set_eq)
+
+lemma SUPR_set_eq:
+ "(SUP x:S. f x) = (\<Union>x\<in>S. f x)"
+ by (simp add: SUPR_def Sup_set_eq)
+
+no_notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ Inf ("\<Sqinter>_" [900] 900) and
+ Sup ("\<Squnion>_" [900] 900)
+
+
+subsubsection {* Unions of families *}
+
declare UNION_def [noatp]
lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)"
@@ -873,11 +1202,12 @@
"A = B ==> (!!x. x:B =simp=> C x = D x) ==> (UN x:A. C x) = (UN x:B. D x)"
by (simp add: UNION_def simp_implies_def)
+lemma image_eq_UN: "f`A = (UN x:A. {f x})"
+ by blast
+
subsubsection {* Intersections of families *}
-text {* @{term [source] "INT x:A. B x"} is @{term "Inter (B`A)"}. *}
-
lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)"
by (unfold INTER_def) blast
@@ -932,66 +1262,6 @@
@{prop "X:C"}. *}
by (unfold Inter_def) blast
-text {*
- \medskip Image of a set under a function. Frequently @{term b} does
- not have the syntactic form of @{term "f x"}.
-*}
-
-declare image_def [noatp]
-
-lemma image_eqI [simp, intro]: "b = f x ==> x:A ==> b : f`A"
- by (unfold image_def) blast
-
-lemma imageI: "x : A ==> f x : f ` A"
- by (rule image_eqI) (rule refl)
-
-lemma rev_image_eqI: "x:A ==> b = f x ==> b : f`A"
- -- {* This version's more effective when we already have the
- required @{term x}. *}
- by (unfold image_def) blast
-
-lemma imageE [elim!]:
- "b : (%x. f x)`A ==> (!!x. b = f x ==> x:A ==> P) ==> P"
- -- {* The eta-expansion gives variable-name preservation. *}
- by (unfold image_def) blast
-
-lemma image_Un: "f`(A Un B) = f`A Un f`B"
- by blast
-
-lemma image_eq_UN: "f`A = (UN x:A. {f x})"
- by blast
-
-lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
- by blast
-
-lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
- -- {* This rewrite rule would confuse users if made default. *}
- by blast
-
-lemma subset_image_iff: "(B \<subseteq> f`A) = (EX AA. AA \<subseteq> A & B = f`AA)"
- apply safe
- prefer 2 apply fast
- apply (rule_tac x = "{a. a : A & f a : B}" in exI, fast)
- done
-
-lemma image_subsetI: "(!!x. x \<in> A ==> f x \<in> B) ==> f`A \<subseteq> B"
- -- {* Replaces the three steps @{text subsetI}, @{text imageE},
- @{text hypsubst}, but breaks too many existing proofs. *}
- by blast
-
-text {*
- \medskip Range of a function -- just a translation for image!
-*}
-
-lemma range_eqI: "b = f x ==> b \<in> range f"
- by simp
-
-lemma rangeI: "f x \<in> range f"
- by simp
-
-lemma rangeE [elim?]: "b \<in> range (\<lambda>x. f x) ==> (!!x. b = f x ==> P) ==> P"
- by blast
-
subsubsection {* Set reasoning tools *}
@@ -1632,15 +1902,9 @@
"u \<in> A ==> (\<Inter>x\<in>A. insert a (B x)) = insert a (\<Inter>x\<in>A. B x)"
by blast
-lemma Union_image_eq [simp]: "\<Union>(B`A) = (\<Union>x\<in>A. B x)"
- by blast
-
lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
by blast
-lemma Inter_image_eq [simp]: "\<Inter>(B`A) = (\<Inter>x\<in>A. B x)"
- by blast
-
lemma UN_constant [simp]: "(\<Union>y\<in>A. c) = (if A = {} then {} else c)"
by auto
@@ -2219,256 +2483,6 @@
unfolding vimage_def Collect_def mem_def ..
-subsection {* Complete lattices *}
-
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65)
-
-class complete_lattice = lattice + bot + top +
- fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
- and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
- assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
- and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
- assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
- and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
-begin
-
-lemma Inf_Sup: "\<Sqinter>A = \<Squnion>{b. \<forall>a \<in> A. b \<le> a}"
- by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-
-lemma Sup_Inf: "\<Squnion>A = \<Sqinter>{b. \<forall>a \<in> A. a \<le> b}"
- by (auto intro: antisym Inf_lower Inf_greatest Sup_upper Sup_least)
-
-lemma Inf_Univ: "\<Sqinter>UNIV = \<Squnion>{}"
- unfolding Sup_Inf by auto
-
-lemma Sup_Univ: "\<Squnion>UNIV = \<Sqinter>{}"
- unfolding Inf_Sup by auto
-
-lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
- by (auto intro: antisym Inf_greatest Inf_lower)
-
-lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
- by (auto intro: antisym Sup_least Sup_upper)
-
-lemma Inf_singleton [simp]:
- "\<Sqinter>{a} = a"
- by (auto intro: antisym Inf_lower Inf_greatest)
-
-lemma Sup_singleton [simp]:
- "\<Squnion>{a} = a"
- by (auto intro: antisym Sup_upper Sup_least)
-
-lemma Inf_insert_simp:
- "\<Sqinter>insert a A = (if A = {} then a else a \<sqinter> \<Sqinter>A)"
- by (cases "A = {}") (simp_all, simp add: Inf_insert)
-
-lemma Sup_insert_simp:
- "\<Squnion>insert a A = (if A = {} then a else a \<squnion> \<Squnion>A)"
- by (cases "A = {}") (simp_all, simp add: Sup_insert)
-
-lemma Inf_binary:
- "\<Sqinter>{a, b} = a \<sqinter> b"
- by (simp add: Inf_insert_simp)
-
-lemma Sup_binary:
- "\<Squnion>{a, b} = a \<squnion> b"
- by (simp add: Sup_insert_simp)
-
-lemma bot_def:
- "bot = \<Squnion>{}"
- by (auto intro: antisym Sup_least)
-
-lemma top_def:
- "top = \<Sqinter>{}"
- by (auto intro: antisym Inf_greatest)
-
-lemma sup_bot [simp]:
- "x \<squnion> bot = x"
- using bot_least [of x] by (simp add: le_iff_sup sup_commute)
-
-lemma inf_top [simp]:
- "x \<sqinter> top = x"
- using top_greatest [of x] by (simp add: le_iff_inf inf_commute)
-
-definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "SUPR A f == \<Squnion> (f ` A)"
-
-definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
- "INFI A f == \<Sqinter> (f ` A)"
-
-end
-
-syntax
- "_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
- "_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
-
-translations
- "SUP x y. B" == "SUP x. SUP y. B"
- "SUP x. B" == "CONST SUPR CONST UNIV (%x. B)"
- "SUP x. B" == "SUP x:CONST UNIV. B"
- "SUP x:A. B" == "CONST SUPR A (%x. B)"
- "INF x y. B" == "INF x. INF y. B"
- "INF x. B" == "CONST INFI CONST UNIV (%x. B)"
- "INF x. B" == "INF x:CONST UNIV. B"
- "INF x:A. B" == "CONST INFI A (%x. B)"
-
-(* To avoid eta-contraction of body: *)
-print_translation {*
-let
- fun btr' syn (A :: Abs abs :: ts) =
- let val (x,t) = atomic_abs_tr' abs
- in list_comb (Syntax.const syn $ x $ A $ t, ts) end
- val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const
-in
-[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")]
-end
-*}
-
-context complete_lattice
-begin
-
-lemma le_SUPI: "i : A \<Longrightarrow> M i \<le> (SUP i:A. M i)"
- by (auto simp add: SUPR_def intro: Sup_upper)
-
-lemma SUP_leI: "(\<And>i. i : A \<Longrightarrow> M i \<le> u) \<Longrightarrow> (SUP i:A. M i) \<le> u"
- by (auto simp add: SUPR_def intro: Sup_least)
-
-lemma INF_leI: "i : A \<Longrightarrow> (INF i:A. M i) \<le> M i"
- by (auto simp add: INFI_def intro: Inf_lower)
-
-lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<le> M i) \<Longrightarrow> u \<le> (INF i:A. M i)"
- by (auto simp add: INFI_def intro: Inf_greatest)
-
-lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
- by (auto intro: antisym SUP_leI le_SUPI)
-
-lemma INF_const[simp]: "A \<noteq> {} \<Longrightarrow> (INF i:A. M) = M"
- by (auto intro: antisym INF_leI le_INFI)
-
-end
-
-
-subsection {* Bool as complete lattice *}
-
-instantiation bool :: complete_lattice
-begin
-
-definition
- Inf_bool_def: "\<Sqinter>A \<longleftrightarrow> (\<forall>x\<in>A. x)"
-
-definition
- Sup_bool_def: "\<Squnion>A \<longleftrightarrow> (\<exists>x\<in>A. x)"
-
-instance
- by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def)
-
-end
-
-lemma Inf_empty_bool [simp]:
- "\<Sqinter>{}"
- unfolding Inf_bool_def by auto
-
-lemma not_Sup_empty_bool [simp]:
- "\<not> \<Squnion>{}"
- unfolding Sup_bool_def by auto
-
-
-subsection {* Fun as complete lattice *}
-
-instantiation "fun" :: (type, complete_lattice) complete_lattice
-begin
-
-definition
- Inf_fun_def [code del]: "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
-
-definition
- Sup_fun_def [code del]: "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
-
-instance
- by intro_classes
- (auto simp add: Inf_fun_def Sup_fun_def le_fun_def
- intro: Inf_lower Sup_upper Inf_greatest Sup_least)
-
-end
-
-lemma Inf_empty_fun:
- "\<Sqinter>{} = (\<lambda>_. \<Sqinter>{})"
- by rule (auto simp add: Inf_fun_def)
-
-lemma Sup_empty_fun:
- "\<Squnion>{} = (\<lambda>_. \<Squnion>{})"
- by rule (auto simp add: Sup_fun_def)
-
-
-subsection {* Set as lattice *}
-
-lemma inf_set_eq: "A \<sqinter> B = A \<inter> B"
- apply (rule subset_antisym)
- apply (rule Int_greatest)
- apply (rule inf_le1)
- apply (rule inf_le2)
- apply (rule inf_greatest)
- apply (rule Int_lower1)
- apply (rule Int_lower2)
- done
-
-lemma sup_set_eq: "A \<squnion> B = A \<union> B"
- apply (rule subset_antisym)
- apply (rule sup_least)
- apply (rule Un_upper1)
- apply (rule Un_upper2)
- apply (rule Un_least)
- apply (rule sup_ge1)
- apply (rule sup_ge2)
- done
-
-lemma mono_Int: "mono f \<Longrightarrow> f (A \<inter> B) \<subseteq> f A \<inter> f B"
- apply (fold inf_set_eq sup_set_eq)
- apply (erule mono_inf)
- done
-
-lemma mono_Un: "mono f \<Longrightarrow> f A \<union> f B \<subseteq> f (A \<union> B)"
- apply (fold inf_set_eq sup_set_eq)
- apply (erule mono_sup)
- done
-
-lemma Inf_set_eq: "\<Sqinter>S = \<Inter>S"
- apply (rule subset_antisym)
- apply (rule Inter_greatest)
- apply (erule Inf_lower)
- apply (rule Inf_greatest)
- apply (erule Inter_lower)
- done
-
-lemma Sup_set_eq: "\<Squnion>S = \<Union>S"
- apply (rule subset_antisym)
- apply (rule Sup_least)
- apply (erule Union_upper)
- apply (rule Union_least)
- apply (erule Sup_upper)
- done
-
-lemma top_set_eq: "top = UNIV"
- by (iprover intro!: subset_antisym subset_UNIV top_greatest)
-
-lemma bot_set_eq: "bot = {}"
- by (iprover intro!: subset_antisym empty_subsetI bot_least)
-
-no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- Inf ("\<Sqinter>_" [900] 900) and
- Sup ("\<Squnion>_" [900] 900)
-
-
subsection {* Misc theorem and ML bindings *}
lemmas equalityI = subset_antisym
--- a/src/HOL/String.thy Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/String.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/ex/Eval_Examples.thy Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/HOL/ex/Numeral.thy Mon Jul 20 13:52:27 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/class_target.ML Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Mon Jul 20 13:52:27 2009 +0200
@@ -242,15 +242,16 @@
val diff_sort = Sign.complete_sort thy [sup]
|> subtract (op =) (Sign.complete_sort thy [sub])
|> filter (is_class thy);
- val deps_witss = case some_dep_morph
- of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
- | NONE => []
+ val add_dependency = case some_dep_morph
+ of SOME dep_morph => Locale.add_dependency sub
+ (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
+ | NONE => I
in
thy
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> Locale.add_dependencies sub deps_witss export
+ |> add_dependency
end;
--- a/src/Pure/Isar/code.ML Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Pure/Isar/code.ML Mon Jul 20 13:52:27 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/Isar/expression.ML Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Pure/Isar/expression.ML Mon Jul 20 13:52:27 2009 +0200
@@ -788,27 +788,6 @@
(*** Interpretation ***)
-(** Interpretation between locales: declaring sublocale relationships **)
-
-local
-
-fun gen_sublocale prep_expr intern raw_target expression thy =
- let
- val target = intern thy raw_target;
- val target_ctxt = Locale.init target thy;
- val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
- fun after_qed witss = ProofContext.theory
- (Locale.add_dependencies target (deps ~~ witss) export);
- in Element.witness_proof after_qed propss goal_ctxt end;
-
-in
-
-fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
-fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
-
-end;
-
-
(** Interpretation in theories **)
local
@@ -816,46 +795,31 @@
fun gen_interpretation prep_expr parse_prop prep_attr
expression equations theory =
let
- val ((propss, regs, export), expr_ctxt) = ProofContext.init theory
+ val ((propss, deps, export), expr_ctxt) = ProofContext.init theory
|> prep_expr expression;
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
- val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations;
+ val attrss = map ((apsnd o map) (prep_attr theory) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- fun store_reg ((name, morph), wits) thy =
+ fun note_eqns raw_eqns thy =
let
- val wits' = map (Element.morph_witness export') wits;
- val morph' = morph $> Element.satisfy_morphism wits';
+ val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
+ val eqn_attrss = map2 (fn attrs => fn eqn =>
+ ((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
+ fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
+ Drule.abs_def) o maps snd;
in
thy
- |> Locale.add_registration (name, (morph', export))
- |> pair (name, morph')
+ |> PureThy.note_thmss Thm.lemmaK eqn_attrss
+ |-> (fn facts => `(fn thy => meta_rewrite thy facts))
end;
- fun store_eqns_activate regs [] thy =
- thy
- |> fold (fn (name, morph) =>
- Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
- | store_eqns_activate regs eqs thy =
- let
- val eqs' = eqs |> map (Morphism.thm (export' $> export));
- val morph_eqs = eqs' |> map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
- Drule.abs_def);
- val eq_morph = Element.eq_morphism thy morph_eqs;
- val eq_attns' = map ((apsnd o map) (Attrib.attribute_i thy)) eq_attns;
- in
- thy
- |> fold (fn (name, morph) =>
- Locale.amend_registration eq_morph (name, morph) #>
- Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
- |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
- |> snd
- end;
-
- fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
- #-> (fn regs => store_eqns_activate regs eqs));
+ fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
+ #-> (fn eqns => fold (fn ((dep, morph), wits) =>
+ Locale.add_registration_eqs (dep, morph $> Element.satisfy_morphism
+ (map (Element.morph_witness export') wits)) eqns export) (deps ~~ witss)));
in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
@@ -868,12 +832,33 @@
end;
+(** Interpretation between locales: declaring sublocale relationships **)
+
+local
+
+fun gen_sublocale prep_expr intern raw_target expression thy =
+ let
+ val target = intern thy raw_target;
+ val target_ctxt = Locale.init target thy;
+ val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
+ fun after_qed witss = ProofContext.theory
+ (fold (fn ((dep, morph), wits) => Locale.add_dependency
+ target (dep, morph $> Element.satisfy_morphism wits) export) (deps ~~ witss));
+ in Element.witness_proof after_qed propss goal_ctxt end;
+
+in
+
+fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
+fun sublocale_cmd x = gen_sublocale read_goal_expression Locale.intern x;
+
+end;
+
+
(** Interpretation in proof contexts **)
local
-fun gen_interpret prep_expr
- expression int state =
+fun gen_interpret prep_expr expression int state =
let
val _ = Proof.assert_forward_or_chain state;
val ctxt = Proof.context_of state;
--- a/src/Pure/Isar/locale.ML Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Pure/Isar/locale.ML Mon Jul 20 13:52:27 2009 +0200
@@ -70,8 +70,8 @@
(* Registrations and dependencies *)
val add_registration: string * (morphism * morphism) -> theory -> theory
val amend_registration: morphism -> string * morphism -> theory -> theory
- val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
- morphism -> theory -> theory
+ val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory
+ val add_dependency: string -> string * morphism -> morphism -> theory -> theory
(* Diagnostic *)
val print_locales: theory -> unit
@@ -368,14 +368,22 @@
(fn ((name, (base, export)), stamp) => ((name, (base $> morph, export)), stamp))) thy
end;
+fun add_registration_eqs (dep, proto_morph) eqns export thy =
+ let
+ val morph = if null eqns then proto_morph
+ else proto_morph $> Element.eq_morphism thy eqns;
+ in
+ thy
+ |> add_registration (dep, (morph, export))
+ |> Context.theory_map (activate_facts (dep, morph $> export))
+ end;
+
(*** Dependencies ***)
-fun add_dependencies loc deps_witss export thy =
+fun add_dependency loc (dep, morph) export thy =
thy
- |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
- (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
- deps_witss
+ |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
|> (fn thy => fold_rev (Context.theory_map o activate_facts)
(all_registrations thy) thy);
--- a/src/Pure/codegen.ML Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Pure/codegen.ML Mon Jul 20 13:52:27 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 Mon Jul 20 00:37:39 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Mon Jul 20 13:52:27 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 _ =