--- a/src/Doc/Main/Main_Doc.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/Doc/Main/Main_Doc.thy Sun Feb 16 18:39:40 2014 +0100
@@ -485,7 +485,7 @@
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@{const Option.the} & @{typeof Option.the}\\
@{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
-@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
+@{const set_option} & @{term_type_only set_option "'a option \<Rightarrow> 'a set"}\\
@{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
\end{tabular}
--- a/src/HOL/Bali/Basis.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/Basis.thy Sun Feb 16 18:39:40 2014 +0100
@@ -199,8 +199,8 @@
"_Oex" :: "[pttrn, 'a option, bool] \<Rightarrow> bool" ("(3\<exists>_\<in>_:/ _)" [0,0,10] 10)
translations
- "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST Option.set A. P"
- "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST Option.set A. P"
+ "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST set_option A. P"
+ "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
section "Special map update"
--- a/src/HOL/Bali/Decl.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/Decl.thy Sun Feb 16 18:39:40 2014 +0100
@@ -818,7 +818,7 @@
--{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
"imethds G I = iface_rec G I
(\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
- (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
+ (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
--- a/src/HOL/Bali/DeclConcepts.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sun Feb 16 18:39:40 2014 +0100
@@ -1402,7 +1402,7 @@
imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
"imethds G I =
iface_rec G I (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
- (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
+ (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
definition
@@ -1543,7 +1543,7 @@
lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set (isuperIfs i)) \<oplus>\<oplus>
- (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
+ (set_option \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
apply (unfold imethds_def)
apply (rule iface_rec [THEN trans])
apply auto
--- a/src/HOL/Bali/Example.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/Example.thy Sun Feb 16 18:39:40 2014 +0100
@@ -458,7 +458,7 @@
lemmas methd_rec' = methd_rec [OF _ ws_tprg]
lemma imethds_HasFoo [simp]:
- "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
+ "imethds tprg HasFoo = set_option \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
apply (rule trans)
apply (rule imethds_rec')
apply (auto simp add: HasFooInt_def)
--- a/src/HOL/Bali/Table.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/Table.thy Sun Feb 16 18:39:40 2014 +0100
@@ -190,7 +190,7 @@
done
lemma Ball_set_tableD:
- "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
+ "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> set_option (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
apply (frule Ball_set_table)
by auto
--- a/src/HOL/Bali/WellForm.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/WellForm.thy Sun Feb 16 18:39:40 2014 +0100
@@ -236,7 +236,7 @@
under (\<lambda> new old. accmodi old \<noteq> Private)
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and>
is_static new = is_static old)) \<and>
- (Option.set \<circ> table_of (imethods i)
+ (set_option \<circ> table_of (imethods i)
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
@@ -248,7 +248,7 @@
lemma wf_idecl_hidings:
"wf_idecl G (I, i) \<Longrightarrow>
- (\<lambda>s. Option.set (table_of (imethods i) s))
+ (\<lambda>s. set_option (table_of (imethods i) s))
hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))
entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
apply (unfold wf_idecl_def o_def)
@@ -753,7 +753,7 @@
show "\<not>is_static im \<and> accmodi im = Public"
proof -
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
- let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
+ let ?new = "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
by (simp add: imethds_rec)
from wf if_I have
@@ -1765,7 +1765,7 @@
by (blast dest: subint1D)
let ?newMethods
- = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
+ = "(set_option \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
show ?case
proof (cases "?newMethods sig = {}")
case True
@@ -1845,7 +1845,7 @@
apply (drule (1) wf_prog_idecl)
apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1
[THEN is_acc_ifaceD [THEN conjunct1]]]])
-apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
+apply (case_tac "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
sig ={}")
apply force
--- a/src/HOL/Bali/WellType.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Bali/WellType.thy Sun Feb 16 18:39:40 2014 +0100
@@ -81,13 +81,13 @@
definition
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
- where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
+ where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` set_option (accmethd G S C sig))"
definition
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
"Objectmheads G S =
(\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
- ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
+ ` set_option (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
definition
accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
--- a/src/HOL/Option.thy Sun Feb 16 17:50:13 2014 +0100
+++ b/src/HOL/Option.thy Sun Feb 16 18:39:40 2014 +0100
@@ -65,19 +65,15 @@
subsubsection {* Operations *}
-primrec set :: "'a option => 'a set" where
-"set None = {}" |
-"set (Some x) = {x}"
-
-lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
+lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
by simp
setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
-lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
+lemma elem_set [iff]: "(x : set_option xo) = (xo = Some x)"
by (cases xo) auto
-lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
+lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
by (cases xo) auto
lemma map_option_case: "map_option f y = (case y of None => None | Some x => Some (f x))"
@@ -182,7 +178,7 @@
"these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
by (auto simp add: these_empty_eq)
-hide_const (open) set bind these
+hide_const (open) bind these
hide_fact (open) bind_cong