# HG changeset patch
# User blanchet
# Date 1392572380 -3600
# Node ID 1ddb2edf5ceb34bb16155d2189d624cb8a6149df
# Parent  a3870c12f254172d1daee474247d1be0e8afc85d
folded 'Option.set' into BNF-generated 'set_option'

diff -r a3870c12f254 -r 1ddb2edf5ceb src/Doc/Main/Main_Doc.thy
--- 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}
 
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/Basis.thy
--- 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"
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/Decl.thy
--- 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))))"
         
 
 
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/DeclConcepts.thy
--- 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
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/Example.thy
--- 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)
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/Table.thy
--- 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
 
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/WellForm.thy
--- 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
 
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Bali/WellType.thy
--- 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"
diff -r a3870c12f254 -r 1ddb2edf5ceb src/HOL/Option.thy
--- 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