folded 'Option.set' into BNF-generated 'set_option'
authorblanchet
Sun Feb 16 18:39:40 2014 +0100 (2014-02-16)
changeset 555181ddb2edf5ceb
parent 55517 a3870c12f254
child 55519 8a54bf4a92ca
folded 'Option.set' into BNF-generated 'set_option'
src/Doc/Main/Main_Doc.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/WellForm.thy
src/HOL/Bali/WellType.thy
src/HOL/Option.thy
     1.1 --- a/src/Doc/Main/Main_Doc.thy	Sun Feb 16 17:50:13 2014 +0100
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Sun Feb 16 18:39:40 2014 +0100
     1.3 @@ -485,7 +485,7 @@
     1.4  \begin{tabular}{@ {} l @ {~::~} l @ {}}
     1.5  @{const Option.the} & @{typeof Option.the}\\
     1.6  @{const map_option} & @{typ[source]"('a \<Rightarrow> 'b) \<Rightarrow> 'a option \<Rightarrow> 'b option"}\\
     1.7 -@{const Option.set} & @{term_type_only Option.set "'a option \<Rightarrow> 'a set"}\\
     1.8 +@{const set_option} & @{term_type_only set_option "'a option \<Rightarrow> 'a set"}\\
     1.9  @{const Option.bind} & @{term_type_only Option.bind "'a option \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"}
    1.10  \end{tabular}
    1.11  
     2.1 --- a/src/HOL/Bali/Basis.thy	Sun Feb 16 17:50:13 2014 +0100
     2.2 +++ b/src/HOL/Bali/Basis.thy	Sun Feb 16 18:39:40 2014 +0100
     2.3 @@ -199,8 +199,8 @@
     2.4    "_Oex"  :: "[pttrn, 'a option, bool] \<Rightarrow> bool"   ("(3\<exists>_\<in>_:/ _)"  [0,0,10] 10)
     2.5  
     2.6  translations
     2.7 -  "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST Option.set A. P"
     2.8 -  "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST Option.set A. P"
     2.9 +  "\<forall>x\<in>A: P" \<rightleftharpoons> "\<forall>x\<in>CONST set_option A. P"
    2.10 +  "\<exists>x\<in>A: P" \<rightleftharpoons> "\<exists>x\<in>CONST set_option A. P"
    2.11  
    2.12  
    2.13  section "Special map update"
     3.1 --- a/src/HOL/Bali/Decl.thy	Sun Feb 16 17:50:13 2014 +0100
     3.2 +++ b/src/HOL/Bali/Decl.thy	Sun Feb 16 18:39:40 2014 +0100
     3.3 @@ -818,7 +818,7 @@
     3.4    --{* methods of an interface, with overriding and inheritance, cf. 9.2 *}
     3.5    "imethds G I = iface_rec G I
     3.6                (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus> 
     3.7 -                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     3.8 +                        (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     3.9          
    3.10  
    3.11  
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Sun Feb 16 17:50:13 2014 +0100
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Sun Feb 16 18:39:40 2014 +0100
     4.3 @@ -1402,7 +1402,7 @@
     4.4    imethds :: "prog \<Rightarrow> qtname \<Rightarrow> (sig,qtname \<times> mhead) tables" where
     4.5    "imethds G I =
     4.6      iface_rec G I  (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
     4.7 -                        (Option.set \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     4.8 +                        (set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))"
     4.9  text {* methods of an interface, with overriding and inheritance, cf. 9.2 *}
    4.10  
    4.11  definition
    4.12 @@ -1543,7 +1543,7 @@
    4.13  
    4.14  lemma imethds_rec: "\<lbrakk>iface G I = Some i; ws_prog G\<rbrakk> \<Longrightarrow>  
    4.15    imethds G I = Un_tables ((\<lambda>J. imethds  G J)`set (isuperIfs i)) \<oplus>\<oplus>  
    4.16 -                      (Option.set \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    4.17 +                      (set_option \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))"
    4.18  apply (unfold imethds_def)
    4.19  apply (rule iface_rec [THEN trans])
    4.20  apply auto
     5.1 --- a/src/HOL/Bali/Example.thy	Sun Feb 16 17:50:13 2014 +0100
     5.2 +++ b/src/HOL/Bali/Example.thy	Sun Feb 16 18:39:40 2014 +0100
     5.3 @@ -458,7 +458,7 @@
     5.4  lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
     5.5  
     5.6  lemma imethds_HasFoo [simp]: 
     5.7 -  "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     5.8 +  "imethds tprg HasFoo = set_option \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
     5.9  apply (rule trans)
    5.10  apply (rule imethds_rec')
    5.11  apply  (auto simp add: HasFooInt_def)
     6.1 --- a/src/HOL/Bali/Table.thy	Sun Feb 16 17:50:13 2014 +0100
     6.2 +++ b/src/HOL/Bali/Table.thy	Sun Feb 16 18:39:40 2014 +0100
     6.3 @@ -190,7 +190,7 @@
     6.4  done
     6.5  
     6.6  lemma Ball_set_tableD: 
     6.7 -  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     6.8 +  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> set_option (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
     6.9  apply (frule Ball_set_table)
    6.10  by auto
    6.11  
     7.1 --- a/src/HOL/Bali/WellForm.thy	Sun Feb 16 17:50:13 2014 +0100
     7.2 +++ b/src/HOL/Bali/WellForm.thy	Sun Feb 16 18:39:40 2014 +0100
     7.3 @@ -236,7 +236,7 @@
     7.4            under  (\<lambda> new old. accmodi old \<noteq> Private)
     7.5            entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
     7.6                               is_static new = is_static old)) \<and> 
     7.7 -        (Option.set \<circ> table_of (imethods i) 
     7.8 +        (set_option \<circ> table_of (imethods i) 
     7.9                 hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
    7.10                 entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))"
    7.11  
    7.12 @@ -248,7 +248,7 @@
    7.13  
    7.14  lemma wf_idecl_hidings: 
    7.15  "wf_idecl G (I, i) \<Longrightarrow> 
    7.16 -  (\<lambda>s. Option.set (table_of (imethods i) s)) 
    7.17 +  (\<lambda>s. set_option (table_of (imethods i) s)) 
    7.18    hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
    7.19    entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
    7.20  apply (unfold wf_idecl_def o_def)
    7.21 @@ -753,7 +753,7 @@
    7.22      show "\<not>is_static im \<and> accmodi im = Public" 
    7.23      proof -
    7.24        let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
    7.25 -      let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
    7.26 +      let ?new = "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
    7.27        from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
    7.28          by (simp add: imethds_rec)
    7.29        from wf if_I have 
    7.30 @@ -1765,7 +1765,7 @@
    7.31        by (blast dest: subint1D)
    7.32  
    7.33      let ?newMethods 
    7.34 -          = "(Option.set \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    7.35 +          = "(set_option \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))"
    7.36      show ?case
    7.37      proof (cases "?newMethods sig = {}")
    7.38        case True
    7.39 @@ -1845,7 +1845,7 @@
    7.40  apply (drule (1) wf_prog_idecl)
    7.41  apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 
    7.42                                         [THEN is_acc_ifaceD [THEN conjunct1]]]])
    7.43 -apply (case_tac "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
    7.44 +apply (case_tac "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i)))
    7.45                    sig ={}")
    7.46  apply   force
    7.47  
     8.1 --- a/src/HOL/Bali/WellType.thy	Sun Feb 16 17:50:13 2014 +0100
     8.2 +++ b/src/HOL/Bali/WellType.thy	Sun Feb 16 18:39:40 2014 +0100
     8.3 @@ -81,13 +81,13 @@
     8.4  
     8.5  definition
     8.6    cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
     8.7 -  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` Option.set (accmethd G S C sig))"
     8.8 +  where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` set_option (accmethd G S C sig))"
     8.9  
    8.10  definition
    8.11    Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where
    8.12    "Objectmheads G S =
    8.13      (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 
    8.14 -      ` Option.set (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
    8.15 +      ` set_option (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))"
    8.16  
    8.17  definition
    8.18    accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
     9.1 --- a/src/HOL/Option.thy	Sun Feb 16 17:50:13 2014 +0100
     9.2 +++ b/src/HOL/Option.thy	Sun Feb 16 18:39:40 2014 +0100
     9.3 @@ -65,19 +65,15 @@
     9.4  
     9.5  subsubsection {* Operations *}
     9.6  
     9.7 -primrec set :: "'a option => 'a set" where
     9.8 -"set None = {}" |
     9.9 -"set (Some x) = {x}"
    9.10 -
    9.11 -lemma ospec [dest]: "(ALL x:set A. P x) ==> A = Some x ==> P x"
    9.12 +lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
    9.13    by simp
    9.14  
    9.15  setup {* map_theory_claset (fn ctxt => ctxt addSD2 ("ospec", @{thm ospec})) *}
    9.16  
    9.17 -lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    9.18 +lemma elem_set [iff]: "(x : set_option xo) = (xo = Some x)"
    9.19    by (cases xo) auto
    9.20  
    9.21 -lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)"
    9.22 +lemma set_empty_eq [simp]: "(set_option xo = {}) = (xo = None)"
    9.23    by (cases xo) auto
    9.24  
    9.25  lemma map_option_case: "map_option f y = (case y of None => None | Some x => Some (f x))"
    9.26 @@ -182,7 +178,7 @@
    9.27    "these B \<noteq> {} \<longleftrightarrow> B \<noteq> {} \<and> B \<noteq> {None}"
    9.28    by (auto simp add: these_empty_eq)
    9.29  
    9.30 -hide_const (open) set bind these
    9.31 +hide_const (open) bind these
    9.32  hide_fact (open) bind_cong
    9.33  
    9.34