clarified syntax of ``long'' statements: fixes/assumes/shows;
authorwenzelm
Mon Feb 25 20:48:14 2002 +0100 (2002-02-25)
changeset 129370c4fd7529467
parent 12936 84eb6c75cfe3
child 12938 a646d0467d81
clarified syntax of ``long'' statements: fixes/assumes/shows;
src/FOL/IFOL.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Bali/WellForm.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/Induct/Term.thy
src/HOL/Set.thy
src/HOL/Transitive_Closure.thy
src/HOL/ex/Locales.thy
src/ZF/Induct/Tree_Forest.thy
     1.1 --- a/src/FOL/IFOL.thy	Mon Feb 25 20:46:09 2002 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Mon Feb 25 20:48:14 2002 +0100
     1.3 @@ -126,7 +126,10 @@
     1.4  subsection {* Intuitionistic Reasoning *}
     1.5  
     1.6  lemma impE':
     1.7 -  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
     1.8 +  assumes 1: "P --> Q"
     1.9 +    and 2: "Q ==> R"
    1.10 +    and 3: "P --> Q ==> P"
    1.11 +  shows R
    1.12  proof -
    1.13    from 3 and 1 have P .
    1.14    with 1 have Q by (rule impE)
    1.15 @@ -134,13 +137,18 @@
    1.16  qed
    1.17  
    1.18  lemma allE':
    1.19 -  (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
    1.20 +  assumes 1: "ALL x. P(x)"
    1.21 +    and 2: "P(x) ==> ALL x. P(x) ==> Q"
    1.22 +  shows Q
    1.23  proof -
    1.24    from 1 have "P(x)" by (rule spec)
    1.25    from this and 1 show Q by (rule 2)
    1.26  qed
    1.27  
    1.28 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
    1.29 +lemma notE':
    1.30 +  assumes 1: "~ P"
    1.31 +    and 2: "~ P ==> P"
    1.32 +  shows R
    1.33  proof -
    1.34    from 2 and 1 have P .
    1.35    with 1 show R by (rule notE)
     2.1 --- a/src/HOL/Bali/AxSound.thy	Mon Feb 25 20:46:09 2002 +0100
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Feb 25 20:48:14 2002 +0100
     2.3 @@ -247,11 +247,11 @@
     2.4  done
     2.5  
     2.6  corollary evaln_type_sound:
     2.7 -      (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
     2.8 -                  wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
     2.9 -             conf_s0: "s0\<Colon>\<preceq>(G,L)" and
    2.10 -                  wf: "wf_prog G"                         
    2.11 -      ) "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
    2.12 +  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
    2.13 +             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
    2.14 +        conf_s0: "s0\<Colon>\<preceq>(G,L)" and
    2.15 +             wf: "wf_prog G"                         
    2.16 +  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
    2.17           (error_free s0 = error_free s1)"
    2.18  proof -
    2.19    from evaln wt conf_s0 wf
     3.1 --- a/src/HOL/Bali/Decl.thy	Mon Feb 25 20:46:09 2002 +0100
     3.2 +++ b/src/HOL/Bali/Decl.thy	Mon Feb 25 20:48:14 2002 +0100
     3.3 @@ -723,12 +723,12 @@
     3.4  qed
     3.5  
     3.6  lemma ws_interface_induct [consumes 2, case_names Step]:
     3.7 - (assumes is_if_I: "is_iface G I" and 
     3.8 +  assumes is_if_I: "is_iface G I" and 
     3.9                 ws: "ws_prog G" and
    3.10            hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i; 
    3.11                              \<forall> J \<in> set (isuperIfs i).
    3.12                                   (I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
    3.13 - ) "P I"
    3.14 +  shows "P I"
    3.15  proof -
    3.16    from is_if_I ws 
    3.17    show "P I"
     4.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:46:09 2002 +0100
     4.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Feb 25 20:48:14 2002 +0100
     4.3 @@ -1007,10 +1007,10 @@
     4.4              split: memberdecl.splits)
     4.5  
     4.6  lemma unique_member_of: 
     4.7 - (assumes n: "G\<turnstile>n member_of C" and  
     4.8 +  assumes n: "G\<turnstile>n member_of C" and  
     4.9            m: "G\<turnstile>m member_of C" and
    4.10         eqid: "memberid n = memberid m"
    4.11 - ) "n=m"
    4.12 +  shows "n=m"
    4.13  proof -
    4.14    from n m eqid  
    4.15    show "n=m"
    4.16 @@ -1173,9 +1173,9 @@
    4.17  by (cases "accmodi m") (auto simp add: permits_acc_def)
    4.18  
    4.19  lemma dyn_accessible_from_static_declC: 
    4.20 -  (assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
    4.21 +  assumes  acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
    4.22             static: "is_static m"
    4.23 -  ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    4.24 +  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    4.25  proof -
    4.26    from acc_C static
    4.27    show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
    4.28 @@ -1304,11 +1304,11 @@
    4.29  by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
    4.30  
    4.31  lemma member_of_inheritance:
    4.32 -  (assumes    m: "G\<turnstile>m member_of D" and 
    4.33 +  assumes       m: "G\<turnstile>m member_of D" and
    4.34       subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
    4.35       subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
    4.36                 ws: "ws_prog G" 
    4.37 -  ) "G\<turnstile>m member_of C"
    4.38 +  shows "G\<turnstile>m member_of C"
    4.39  proof -
    4.40    from m subclseq_D_C subclseq_C_m
    4.41    show ?thesis
    4.42 @@ -1352,13 +1352,13 @@
    4.43  qed
    4.44  
    4.45  lemma member_of_subcls:
    4.46 -  (assumes    old: "G\<turnstile>old member_of C" and 
    4.47 +  assumes     old: "G\<turnstile>old member_of C" and 
    4.48                new: "G\<turnstile>new member_of D" and
    4.49               eqid: "memberid new = memberid old" and
    4.50       subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
    4.51     subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
    4.52                 ws: "ws_prog G"
    4.53 -  ) "G\<turnstile>D \<prec>\<^sub>C C"
    4.54 +  shows "G\<turnstile>D \<prec>\<^sub>C C"
    4.55  proof -
    4.56    from old 
    4.57    have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
    4.58 @@ -1423,10 +1423,10 @@
    4.59  
    4.60  
    4.61  lemma inherited_field_access: 
    4.62 - (assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
    4.63 +  assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
    4.64            is_field: "is_field membr" and 
    4.65            subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
    4.66 - ) "G\<turnstile>membr in dynC dyn_accessible_from accC"
    4.67 +  shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
    4.68  proof -
    4.69    from stat_acc is_field subclseq 
    4.70    show ?thesis
    4.71 @@ -1437,11 +1437,11 @@
    4.72  qed
    4.73  
    4.74  lemma accessible_inheritance:
    4.75 - (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
    4.76 +  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
    4.77            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
    4.78         member_dynC: "G\<turnstile>m member_of dynC" and
    4.79            dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
    4.80 - ) "G\<turnstile>m of dynC accessible_from accC"
    4.81 +  shows "G\<turnstile>m of dynC accessible_from accC"
    4.82  proof -
    4.83    from stat_acc
    4.84    have member_statC: "G\<turnstile>m member_of statC" 
    4.85 @@ -1664,13 +1664,13 @@
    4.86  done
    4.87  
    4.88  lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
    4.89 - (assumes im: "im \<in> imethds G I sig" and  
    4.90 +  assumes im: "im \<in> imethds G I sig" and  
    4.91           ifI: "iface G I = Some i" and
    4.92            ws: "ws_prog G" and
    4.93       hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
    4.94                  = Some im \<Longrightarrow> P" and
    4.95       hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
    4.96 -  ) "P"
    4.97 +  shows P
    4.98  proof -
    4.99    from ifI ws im hyp_new hyp_inh
   4.100    show "P"
   4.101 @@ -1756,9 +1756,9 @@
   4.102  by (auto dest: methd_declC method_declared_inI)
   4.103  
   4.104  lemma member_methd:
   4.105 - (assumes member_of: "G\<turnstile>Methd sig m member_of C" and
   4.106 +  assumes member_of: "G\<turnstile>Methd sig m member_of C" and
   4.107                   ws: "ws_prog G"
   4.108 - ) "methd G C sig = Some m"
   4.109 +  shows "methd G C sig = Some m"
   4.110  proof -
   4.111    from member_of 
   4.112    have iscls_C: "is_class G C" 
   4.113 @@ -2013,13 +2013,13 @@
   4.114  by (auto simp add: dynmethd_rec)
   4.115   
   4.116  lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
   4.117 -  (assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.118 +  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.119          is_cls_dynC: "is_class G dynC" and
   4.120                   ws: "ws_prog G" and
   4.121           hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   4.122         hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
   4.123                         G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   4.124 -   ) "P"
   4.125 +  shows P
   4.126  proof -
   4.127    from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   4.128    from clsDynC ws dynM hyp_static hyp_override
   4.129 @@ -2037,13 +2037,12 @@
   4.130  qed
   4.131  
   4.132  lemma no_override_in_Object:
   4.133 -  (assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.134 +  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.135              is_cls_dynC: "is_class G dynC" and
   4.136                       ws: "ws_prog G" and
   4.137                    statM: "methd G statC sig = Some statM" and
   4.138           neq_dynM_statM: "dynM\<noteq>statM"
   4.139 -   )
   4.140 -   "dynC \<noteq> Object"
   4.141 +  shows "dynC \<noteq> Object"
   4.142  proof -
   4.143    from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
   4.144    from clsDynC ws dynM statM neq_dynM_statM 
   4.145 @@ -2063,7 +2062,7 @@
   4.146  
   4.147  lemma dynmethd_Some_rec_cases [consumes 3, 
   4.148                                 case_names Static Override  Recursion]:
   4.149 -(assumes     dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.150 +  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
   4.151                  clsDynC: "class G dynC = Some c" and
   4.152                       ws: "ws_prog G" and
   4.153               hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
   4.154 @@ -2072,8 +2071,8 @@
   4.155                                       G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
   4.156  
   4.157            hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
   4.158 -                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P" 
   4.159 -  ) "P"
   4.160 +                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
   4.161 +  shows P
   4.162  proof -
   4.163    from clsDynC have "is_class G dynC" by simp
   4.164    note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
   4.165 @@ -2139,12 +2138,12 @@
   4.166  qed
   4.167  
   4.168  lemma methd_Some_dynmethd_Some:
   4.169 -  (assumes    statM: "methd G statC sig = Some statM" and 
   4.170 +  assumes     statM: "methd G statC sig = Some statM" and
   4.171             subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   4.172         is_cls_statC: "is_class G statC" and
   4.173                   ws: "ws_prog G"
   4.174 -   ) "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
   4.175 -   (is "?P dynC")
   4.176 +  shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
   4.177 +    (is "?P dynC")
   4.178  proof -
   4.179    from subclseq is_cls_statC 
   4.180    have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   4.181 @@ -2185,7 +2184,7 @@
   4.182  qed
   4.183  
   4.184  lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
   4.185 -  (assumes    statM: "methd G statC sig = Some statM" and 
   4.186 +  assumes     statM: "methd G statC sig = Some statM" and 
   4.187             subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   4.188         is_cls_statC: "is_class G statC" and
   4.189                   ws: "ws_prog G" and
   4.190 @@ -2193,7 +2192,7 @@
   4.191         hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
   4.192                                   dynM\<noteq>statM;
   4.193                             G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
   4.194 -   ) "P"
   4.195 +  shows P
   4.196  proof -
   4.197    from subclseq is_cls_statC 
   4.198    have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   4.199 @@ -2215,13 +2214,13 @@
   4.200  qed
   4.201  
   4.202  lemma ws_dynmethd:
   4.203 -  (assumes statM: "methd G statC sig = Some statM" and
   4.204 +  assumes  statM: "methd G statC sig = Some statM" and
   4.205          subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   4.206      is_cls_statC: "is_class G statC" and
   4.207                ws: "ws_prog G"
   4.208 -   )
   4.209 -   "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
   4.210 -            is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
   4.211 +  shows
   4.212 +    "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
   4.213 +             is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
   4.214  proof - 
   4.215    from statM subclseq is_cls_statC ws
   4.216    show ?thesis
     5.1 --- a/src/HOL/Bali/Evaln.thy	Mon Feb 25 20:46:09 2002 +0100
     5.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Feb 25 20:48:14 2002 +0100
     5.3 @@ -324,12 +324,12 @@
     5.4  done
     5.5  
     5.6  lemma evaln_eval:  
     5.7 - (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
     5.8 +  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
     5.9               wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
    5.10          conf_s0: "s0\<Colon>\<preceq>(G, L)" and
    5.11               wf: "wf_prog G" 
    5.12         
    5.13 - )  "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
    5.14 +  shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
    5.15  proof -
    5.16    from evaln 
    5.17    show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
    5.18 @@ -477,8 +477,9 @@
    5.19    next
    5.20      case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
    5.21             v vs L accC T)
    5.22 -    (* Repeats large parts of the type soundness proof. One should factor
    5.23 -       out some lemmata about the relations and conformance of s2, s3 and s3'*)
    5.24 +    txt {* Repeats large parts of the type soundness proof. One should factor
    5.25 +      out some lemmata about the relations and conformance of @{text
    5.26 +      s2}, @{text s3} and @{text s3'} *}
    5.27      have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
    5.28      have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
    5.29      have invDeclC: "invDeclC 
    5.30 @@ -934,8 +935,7 @@
    5.31        show ?thesis
    5.32  	by simp
    5.33      qed
    5.34 -    from cls this
    5.35 -    show ?case
    5.36 +    with cls show ?case
    5.37        by (rule eval.Init)
    5.38    qed 
    5.39  qed
    5.40 @@ -994,13 +994,14 @@
    5.41    show ?thesis .
    5.42  qed
    5.43  
    5.44 +text {* *} (* FIXME *)
    5.45  
    5.46  lemma eval_evaln: 
    5.47 - (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
    5.48 -          wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
    5.49 -     conf_s0: "s0\<Colon>\<preceq>(G, L)" and
    5.50 -          wf: "wf_prog G"  
    5.51 - )  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
    5.52 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
    5.53 +            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
    5.54 +       conf_s0: "s0\<Colon>\<preceq>(G, L)" and
    5.55 +            wf: "wf_prog G"  
    5.56 +  shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
    5.57  proof -
    5.58    from eval 
    5.59    show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
    5.60 @@ -1185,7 +1186,7 @@
    5.61  	with xcpt_s2 conf_s2 wf 
    5.62  	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
    5.63  	  by (auto dest: Try_lemma)
    5.64 -	(* FIXME extract lemma for this conformance, also usefull for
    5.65 +	(* FIXME extract lemma for this conformance, also useful for
    5.66                 eval_type_sound and evaln_eval *)
    5.67  	from this wt_c2
    5.68  	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
     6.1 --- a/src/HOL/Bali/TypeSafe.thy	Mon Feb 25 20:46:09 2002 +0100
     6.2 +++ b/src/HOL/Bali/TypeSafe.thy	Mon Feb 25 20:48:14 2002 +0100
     6.3 @@ -10,9 +10,9 @@
     6.4  section "error free"
     6.5   
     6.6  lemma error_free_halloc:
     6.7 - (assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
     6.8 +  assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
     6.9            error_free_s0: "error_free s0"
    6.10 - ) "error_free s1"
    6.11 +  shows "error_free s1"
    6.12  proof -
    6.13    from halloc error_free_s0
    6.14    obtain abrupt0 store0 abrupt1 store1
    6.15 @@ -37,8 +37,8 @@
    6.16  qed
    6.17  
    6.18  lemma error_free_sxalloc:
    6.19 - (assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0") 
    6.20 - "error_free s1"
    6.21 +  assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
    6.22 +  shows "error_free s1"
    6.23  proof -
    6.24    from sxalloc error_free_s0
    6.25    obtain abrupt0 store0 abrupt1 store1
    6.26 @@ -857,17 +857,17 @@
    6.27  
    6.28  (* #### stat raus und gleich is_static f schreiben *) 
    6.29  theorem dynamic_field_access_ok:
    6.30 -  (assumes wf: "wf_prog G" and
    6.31 -     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
    6.32 -    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
    6.33 -    conform_s: "s\<Colon>\<preceq>(G, L)" and 
    6.34 -     normal_s: "normal s" and
    6.35 -         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
    6.36 -            f: "accfield G accC statC fn = Some f" and
    6.37 -         dynC: "if stat then dynC=declclass f  
    6.38 -                        else dynC=obj_class (lookup_obj (store s) a)" and
    6.39 -         stat: "if stat then (is_static f) else (\<not> is_static f)"
    6.40 -  ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
    6.41 +  assumes wf: "wf_prog G" and
    6.42 +    not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
    6.43 +   conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
    6.44 +   conform_s: "s\<Colon>\<preceq>(G, L)" and 
    6.45 +    normal_s: "normal s" and
    6.46 +        wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
    6.47 +           f: "accfield G accC statC fn = Some f" and
    6.48 +        dynC: "if stat then dynC=declclass f  
    6.49 +                       else dynC=obj_class (lookup_obj (store s) a)" and
    6.50 +        stat: "if stat then (is_static f) else (\<not> is_static f)"
    6.51 +  shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and> 
    6.52       G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
    6.53  proof (cases "stat")
    6.54    case True
    6.55 @@ -1017,7 +1017,7 @@
    6.56  *)
    6.57  
    6.58  lemma error_free_field_access:
    6.59 - (assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
    6.60 +  assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
    6.61                wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
    6.62           eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
    6.63              eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
    6.64 @@ -1025,7 +1025,7 @@
    6.65              conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
    6.66                fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
    6.67                  wf: "wf_prog G"   
    6.68 - ) "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
    6.69 +  shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
    6.70  proof -
    6.71    from fvar
    6.72    have store_s2': "store s2'=store s2"
    6.73 @@ -1066,12 +1066,12 @@
    6.74  qed
    6.75  
    6.76  lemma call_access_ok:
    6.77 -(assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
    6.78 -     and        wf: "wf_prog G" 
    6.79 -     and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
    6.80 -     and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
    6.81 -     and      invC: "invC = invocation_class (invmode statM e) s a statT"
    6.82 -)"\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
    6.83 +  assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
    6.84 +      and        wf: "wf_prog G" 
    6.85 +      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
    6.86 +      and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
    6.87 +      and      invC: "invC = invocation_class (invmode statM e) s a statT"
    6.88 +  shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
    6.89    G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
    6.90  proof -
    6.91    from wt_e wf have type_statT: "is_type G (RefT statT)"
    6.92 @@ -1123,7 +1123,7 @@
    6.93  qed
    6.94  
    6.95  lemma error_free_call_access:
    6.96 - (assumes     
    6.97 +  assumes
    6.98     eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
    6.99          wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
   6.100         statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
   6.101 @@ -1138,7 +1138,7 @@
   6.102      invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
   6.103                               a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
   6.104            wf: "wf_prog G"
   6.105 - )"check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
   6.106 +  shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
   6.107     = s3"
   6.108  proof (cases "normal s2")
   6.109    case False
   6.110 @@ -1198,11 +1198,11 @@
   6.111  section "main proof of type safety"
   6.112  
   6.113  lemma eval_type_sound:
   6.114 -      (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
   6.115 -                 wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
   6.116 -                 wf: "wf_prog G" and 
   6.117 -            conf_s0: "s0\<Colon>\<preceq>(G,L)"           
   6.118 -      ) "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
   6.119 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
   6.120 +            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
   6.121 +            wf: "wf_prog G" and 
   6.122 +       conf_s0: "s0\<Colon>\<preceq>(G,L)"           
   6.123 +  shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
   6.124           (error_free s0 = error_free s1)"
   6.125  proof -
   6.126    from eval 
     7.1 --- a/src/HOL/Bali/WellForm.thy	Mon Feb 25 20:46:09 2002 +0100
     7.2 +++ b/src/HOL/Bali/WellForm.thy	Mon Feb 25 20:48:14 2002 +0100
     7.3 @@ -718,7 +718,8 @@
     7.4  qed
     7.5  
     7.6  lemma wf_prog_hidesD:
     7.7 - (assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G") 
     7.8 +  assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G"
     7.9 +  shows
    7.10     "accmodi old \<le> accmodi new \<and>
    7.11      is_static old"
    7.12  proof -
    7.13 @@ -759,7 +760,8 @@
    7.14  @{text wf_prog_dyn_override_prop}.
    7.15  *}
    7.16  lemma wf_prog_stat_overridesD:
    7.17 - (assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G") 
    7.18 +  assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
    7.19 +  shows
    7.20     "G\<turnstile>resTy new\<preceq>resTy old \<and>
    7.21      accmodi old \<le> accmodi new \<and>
    7.22      \<not> is_static old"
    7.23 @@ -790,8 +792,8 @@
    7.24  qed
    7.25      
    7.26  lemma static_to_dynamic_overriding: 
    7.27 -  (assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G")
    7.28 -   "G\<turnstile>new overrides old"
    7.29 +  assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G"
    7.30 +  shows "G\<turnstile>new overrides old"
    7.31  proof -
    7.32    from stat_override 
    7.33    show ?thesis (is "?Overrides new old")
    7.34 @@ -827,14 +829,14 @@
    7.35  qed
    7.36  
    7.37  lemma non_Package_instance_method_inheritance:
    7.38 -(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
    7.39 -             accmodi_old: "accmodi old \<noteq> Package" and 
    7.40 -         instance_method: "\<not> is_static old" and
    7.41 -                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
    7.42 -            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
    7.43 -                      wf: "wf_prog G"
    7.44 -) "G\<turnstile>Method old member_of C \<or>
    7.45 -   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and>  G\<turnstile>Method new member_of C)"
    7.46 +  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
    7.47 +              accmodi_old: "accmodi old \<noteq> Package" and 
    7.48 +          instance_method: "\<not> is_static old" and
    7.49 +                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
    7.50 +             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
    7.51 +                       wf: "wf_prog G"
    7.52 +  shows "G\<turnstile>Method old member_of C \<or>
    7.53 +   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
    7.54  proof -
    7.55    from wf have ws: "ws_prog G" by auto
    7.56    from old_declared have iscls_declC_old: "is_class G (declclass old)"
    7.57 @@ -989,17 +991,17 @@
    7.58  
    7.59  lemma non_Package_instance_method_inheritance_cases [consumes 6,
    7.60           case_names Inheritance Overriding]:
    7.61 -(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
    7.62 -             accmodi_old: "accmodi old \<noteq> Package" and 
    7.63 -         instance_method: "\<not> is_static old" and
    7.64 -                  subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
    7.65 -            old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
    7.66 -                      wf: "wf_prog G" and
    7.67 -             inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
    7.68 -             overriding:  "\<And> new. 
    7.69 +  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
    7.70 +              accmodi_old: "accmodi old \<noteq> Package" and 
    7.71 +          instance_method: "\<not> is_static old" and
    7.72 +                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
    7.73 +             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
    7.74 +                       wf: "wf_prog G" and
    7.75 +              inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
    7.76 +               overriding: "\<And> new.
    7.77                             \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
    7.78                             \<Longrightarrow> P"
    7.79 -) "P"
    7.80 +  shows P
    7.81  proof -
    7.82    from old_inheritable accmodi_old instance_method subcls old_declared wf 
    7.83         inheritance overriding
    7.84 @@ -1008,10 +1010,10 @@
    7.85  qed
    7.86  
    7.87  lemma dynamic_to_static_overriding:
    7.88 -(assumes dyn_override: "G\<turnstile> new overrides old" and
    7.89 -          accmodi_old: "accmodi old \<noteq> Package" and
    7.90 -                   wf: "wf_prog G"
    7.91 -) "G\<turnstile> new overrides\<^sub>S old"  
    7.92 +  assumes dyn_override: "G\<turnstile> new overrides old" and
    7.93 +           accmodi_old: "accmodi old \<noteq> Package" and
    7.94 +                    wf: "wf_prog G"
    7.95 +  shows "G\<turnstile> new overrides\<^sub>S old"  
    7.96  proof - 
    7.97    from dyn_override accmodi_old
    7.98    show ?thesis (is "?Overrides new old")
    7.99 @@ -1101,9 +1103,9 @@
   7.100  qed
   7.101  
   7.102  lemma wf_prog_dyn_override_prop:
   7.103 - (assumes dyn_override: "G \<turnstile> new overrides old" and
   7.104 +  assumes dyn_override: "G \<turnstile> new overrides old" and
   7.105                      wf: "wf_prog G"
   7.106 - ) "accmodi old \<le> accmodi new"
   7.107 +  shows "accmodi old \<le> accmodi new"
   7.108  proof (cases "accmodi old = Package")
   7.109    case True
   7.110    note old_Package = this
   7.111 @@ -1130,10 +1132,10 @@
   7.112  qed 
   7.113  
   7.114  lemma overrides_Package_old: 
   7.115 -(assumes dyn_override: "G \<turnstile> new overrides old" and 
   7.116 -          accmodi_new: "accmodi new = Package" and
   7.117 -                   wf: "wf_prog G "
   7.118 -) "accmodi old = Package"
   7.119 +  assumes dyn_override: "G \<turnstile> new overrides old" and 
   7.120 +           accmodi_new: "accmodi new = Package" and
   7.121 +                    wf: "wf_prog G "
   7.122 +  shows "accmodi old = Package"
   7.123  proof (cases "accmodi old")
   7.124    case Private
   7.125    with dyn_override show ?thesis
   7.126 @@ -1166,11 +1168,11 @@
   7.127  qed
   7.128  
   7.129  lemma dyn_override_Package:
   7.130 - (assumes dyn_override: "G \<turnstile> new overrides old" and
   7.131 -          accmodi_old: "accmodi old = Package" and 
   7.132 -          accmodi_new: "accmodi new = Package" and
   7.133 +  assumes dyn_override: "G \<turnstile> new overrides old" and
   7.134 +           accmodi_old: "accmodi old = Package" and 
   7.135 +           accmodi_new: "accmodi new = Package" and
   7.136                      wf: "wf_prog G"
   7.137 - ) "pid (declclass old) = pid (declclass new)"
   7.138 +  shows "pid (declclass old) = pid (declclass new)"
   7.139  proof - 
   7.140    from dyn_override accmodi_old accmodi_new
   7.141    show ?thesis (is "?EqPid old new")
   7.142 @@ -1195,11 +1197,11 @@
   7.143  qed
   7.144  
   7.145  lemma dyn_override_Package_escape:
   7.146 - (assumes dyn_override: "G \<turnstile> new overrides old" and
   7.147 -          accmodi_old: "accmodi old = Package" and 
   7.148 -         outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
   7.149 +  assumes dyn_override: "G \<turnstile> new overrides old" and
   7.150 +           accmodi_old: "accmodi old = Package" and 
   7.151 +          outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
   7.152                      wf: "wf_prog G"
   7.153 - ) "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
   7.154 +  shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
   7.155               pid (declclass old) = pid (declclass inter) \<and>
   7.156               Protected \<le> accmodi inter"
   7.157  proof -
   7.158 @@ -1373,10 +1375,11 @@
   7.159  qed
   7.160  
   7.161  lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
   7.162 -(assumes methd_C: "methd G C sig = Some m" and
   7.163 -                    ws: "ws_prog G" and
   7.164 -                  clsC: "class G C = Some c" and
   7.165 -             neq_C_Obj: "C\<noteq>Object" )  
   7.166 +  assumes methd_C: "methd G C sig = Some m" and
   7.167 +               ws: "ws_prog G" and
   7.168 +             clsC: "class G C = Some c" and
   7.169 +        neq_C_Obj: "C\<noteq>Object"
   7.170 +  shows
   7.171  "\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
   7.172    \<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P 
   7.173   \<rbrakk> \<Longrightarrow> P"
   7.174 @@ -1406,8 +1409,9 @@
   7.175  
   7.176    
   7.177  lemma methd_member_of:
   7.178 - (assumes wf: "wf_prog G") 
   7.179 -  "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
   7.180 +  assumes wf: "wf_prog G"
   7.181 +  shows
   7.182 +    "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 
   7.183    (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 
   7.184  proof -
   7.185    from wf   have   ws: "ws_prog G" ..
   7.186 @@ -1452,13 +1456,13 @@
   7.187              intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
   7.188  
   7.189  lemma wf_prog_staticD:
   7.190 - (assumes     wf: "wf_prog G" and 
   7.191 +  assumes     wf: "wf_prog G" and
   7.192              clsC: "class G C = Some c" and
   7.193         neq_C_Obj: "C \<noteq> Object" and 
   7.194               old: "methd G (super c) sig = Some old" and 
   7.195       accmodi_old: "Protected \<le> accmodi old" and
   7.196               new: "table_of (methods c) sig = Some new"
   7.197 - ) "is_static new = is_static old"
   7.198 +  shows "is_static new = is_static old"
   7.199  proof -
   7.200    from clsC wf 
   7.201    have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
   7.202 @@ -1508,13 +1512,13 @@
   7.203  qed
   7.204  
   7.205  lemma inheritable_instance_methd: 
   7.206 - (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.207 +  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.208                is_cls_D: "is_class G D" and
   7.209                      wf: "wf_prog G" and 
   7.210                     old: "methd G D sig = Some old" and
   7.211             accmodi_old: "Protected \<le> accmodi old" and  
   7.212          not_static_old: "\<not> is_static old"
   7.213 - )  
   7.214 +  shows
   7.215    "\<exists>new. methd G C sig = Some new \<and>
   7.216           (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
   7.217   (is "(\<exists>new. (?Constraint C new old))")
   7.218 @@ -1644,7 +1648,7 @@
   7.219  
   7.220  lemma inheritable_instance_methd_cases [consumes 6
   7.221                                         , case_names Inheritance Overriding]: 
   7.222 - (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.223 +  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.224                is_cls_D: "is_class G D" and
   7.225                      wf: "wf_prog G" and 
   7.226                     old: "methd G D sig = Some old" and
   7.227 @@ -1654,7 +1658,7 @@
   7.228              overriding:  "\<And> new. \<lbrakk>methd G C sig = Some new;
   7.229                                     G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
   7.230          
   7.231 - ) "P"
   7.232 +  shows P
   7.233  proof -
   7.234  from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 
   7.235  show ?thesis
   7.236 @@ -1662,13 +1666,13 @@
   7.237  qed
   7.238  
   7.239  lemma inheritable_instance_methd_props: 
   7.240 - (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.241 +  assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
   7.242                is_cls_D: "is_class G D" and
   7.243                      wf: "wf_prog G" and 
   7.244                     old: "methd G D sig = Some old" and
   7.245             accmodi_old: "Protected \<le> accmodi old" and  
   7.246          not_static_old: "\<not> is_static old"
   7.247 - )  
   7.248 +  shows
   7.249    "\<exists>new. methd G C sig = Some new \<and>
   7.250            \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
   7.251   (is "(\<exists>new. (?Constraint C new old))")
   7.252 @@ -1976,11 +1980,11 @@
   7.253  *)
   7.254  
   7.255  lemma dynmethd_Object:
   7.256 - (assumes statM: "methd G Object sig = Some statM" and
   7.257 +  assumes statM: "methd G Object sig = Some statM" and
   7.258          private: "accmodi statM = Private" and 
   7.259         is_cls_C: "is_class G C" and
   7.260               wf: "wf_prog G"
   7.261 - ) "dynmethd G Object C sig = Some statM"
   7.262 +  shows "dynmethd G Object C sig = Some statM"
   7.263  proof -
   7.264    from is_cls_C wf 
   7.265    have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 
   7.266 @@ -2002,12 +2006,12 @@
   7.267  qed
   7.268  
   7.269  lemma wf_imethds_hiding_objmethdsD: 
   7.270 -  (assumes     old: "methd G Object sig = Some old" and
   7.271 -           is_if_I: "is_iface G I" and
   7.272 -                wf: "wf_prog G" and    
   7.273 -       not_private: "accmodi old \<noteq> Private" and
   7.274 -               new: "new \<in> imethds G I sig" 
   7.275 -  ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
   7.276 +  assumes     old: "methd G Object sig = Some old" and
   7.277 +          is_if_I: "is_iface G I" and
   7.278 +               wf: "wf_prog G" and    
   7.279 +      not_private: "accmodi old \<noteq> Private" and
   7.280 +              new: "new \<in> imethds G I sig" 
   7.281 +  shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
   7.282  proof -
   7.283    from wf have ws: "ws_prog G" by simp
   7.284    {
   7.285 @@ -2102,10 +2106,10 @@
   7.286  "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
   7.287  
   7.288  lemma valid_lookup_cls_is_class:
   7.289 - (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
   7.290 +  assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
   7.291        ty_statT: "isrtype G statT" and
   7.292              wf: "wf_prog G"
   7.293 - ) "is_class G dynC"
   7.294 +  shows "is_class G dynC"
   7.295  proof (cases statT)
   7.296    case NullT
   7.297    with dynC ty_statT show ?thesis
   7.298 @@ -2503,10 +2507,10 @@
   7.299                   static_to_dynamic_overriding)
   7.300  
   7.301  lemma static_to_dynamic_accessible_from:
   7.302 - (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
   7.303 +  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
   7.304            subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   7.305                  wf: "wf_prog G"
   7.306 - ) "G\<turnstile>m in dynC dyn_accessible_from accC"
   7.307 +  shows "G\<turnstile>m in dynC dyn_accessible_from accC"
   7.308  proof - 
   7.309    from stat_acc subclseq 
   7.310    show ?thesis (is "?Dyn_accessible m")
   7.311 @@ -2528,10 +2532,10 @@
   7.312  qed
   7.313  
   7.314  lemma static_to_dynamic_accessible_from_static:
   7.315 - (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
   7.316 +  assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
   7.317              static: "is_static m" and
   7.318                  wf: "wf_prog G"
   7.319 - ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
   7.320 +  shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
   7.321  proof -
   7.322    from stat_acc wf 
   7.323    have "G\<turnstile>m in statC dyn_accessible_from accC"
   7.324 @@ -2542,10 +2546,10 @@
   7.325  qed
   7.326  
   7.327  lemma dynmethd_member_in:
   7.328 - (assumes    m: "dynmethd G statC dynC sig = Some m" and
   7.329 +  assumes    m: "dynmethd G statC dynC sig = Some m" and
   7.330     iscls_statC: "is_class G statC" and
   7.331              wf: "wf_prog G"
   7.332 - ) "G\<turnstile>Methd sig m member_in dynC"
   7.333 +  shows "G\<turnstile>Methd sig m member_in dynC"
   7.334  proof -
   7.335    from m 
   7.336    have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
   7.337 @@ -2563,11 +2567,11 @@
   7.338  qed
   7.339  
   7.340  lemma dynmethd_access_prop:
   7.341 -  (assumes statM: "methd G statC sig = Some statM" and
   7.342 -        stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
   7.343 -            dynM: "dynmethd G statC dynC sig = Some dynM" and
   7.344 -              wf: "wf_prog G" 
   7.345 -   ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.346 +  assumes statM: "methd G statC sig = Some statM" and
   7.347 +       stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
   7.348 +           dynM: "dynmethd G statC dynC sig = Some dynM" and
   7.349 +             wf: "wf_prog G" 
   7.350 +  shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.351  proof -
   7.352    from wf have ws: "ws_prog G" ..
   7.353    from dynM 
   7.354 @@ -2638,12 +2642,12 @@
   7.355  qed
   7.356  
   7.357  lemma implmt_methd_access:
   7.358 -(fixes accC::qtname
   7.359 - assumes iface_methd: "imethds G I sig \<noteq> {}" and
   7.360 +  fixes accC::qtname
   7.361 +  assumes iface_methd: "imethds G I sig \<noteq> {}" and
   7.362             implements: "G\<turnstile>dynC\<leadsto>I"  and
   7.363                 isif_I: "is_iface G I" and
   7.364                     wf: "wf_prog G" 
   7.365 - ) "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
   7.366 +  shows "\<exists> dynM. methd G dynC sig = Some dynM \<and> 
   7.367              G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.368  proof -
   7.369    from implements 
   7.370 @@ -2668,12 +2672,12 @@
   7.371  qed
   7.372  
   7.373  corollary implmt_dynimethd_access:
   7.374 -(fixes accC::qtname
   7.375 - assumes iface_methd: "imethds G I sig \<noteq> {}" and
   7.376 +  fixes accC::qtname
   7.377 +  assumes iface_methd: "imethds G I sig \<noteq> {}" and
   7.378             implements: "G\<turnstile>dynC\<leadsto>I"  and
   7.379                 isif_I: "is_iface G I" and
   7.380                     wf: "wf_prog G" 
   7.381 - ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
   7.382 +  shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 
   7.383              G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.384  proof -
   7.385    from iface_methd
   7.386 @@ -2686,12 +2690,12 @@
   7.387  qed
   7.388  
   7.389  lemma dynlookup_access_prop:
   7.390 - (assumes emh: "emh \<in> mheads G accC statT sig" and
   7.391 +  assumes emh: "emh \<in> mheads G accC statT sig" and
   7.392           dynM: "dynlookup G statT dynC sig = Some dynM" and
   7.393      dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
   7.394      isT_statT: "isrtype G statT" and
   7.395             wf: "wf_prog G"
   7.396 - ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.397 +  shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.398  proof -
   7.399    from emh wf
   7.400    have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
   7.401 @@ -2835,11 +2839,11 @@
   7.402  qed
   7.403  
   7.404  lemma dynlookup_access:
   7.405 - (assumes emh: "emh \<in> mheads G accC statT sig" and
   7.406 +  assumes emh: "emh \<in> mheads G accC statT sig" and
   7.407      dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
   7.408      isT_statT: "isrtype G statT" and
   7.409             wf: "wf_prog G"
   7.410 - ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
   7.411 +  shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 
   7.412              G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
   7.413  proof - 
   7.414    from dynC_prop isT_statT wf
   7.415 @@ -2855,10 +2859,10 @@
   7.416  qed
   7.417  
   7.418  lemma stat_overrides_Package_old: 
   7.419 -(assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
   7.420 +  assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 
   7.421            accmodi_new: "accmodi new = Package" and
   7.422                     wf: "wf_prog G "
   7.423 -) "accmodi old = Package"
   7.424 +  shows "accmodi old = Package"
   7.425  proof -
   7.426    from stat_override wf 
   7.427    have "accmodi old \<le> accmodi new"
   7.428 @@ -2916,12 +2920,12 @@
   7.429  since methods can break the package bounds due to overriding
   7.430  *}
   7.431  lemma dyn_accessible_instance_field_Protected:
   7.432 - (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
   7.433 +  assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
   7.434               prot: "accmodi f = Protected" and
   7.435              field: "is_field f" and
   7.436     instance_field: "\<not> is_static f" and
   7.437            outside: "pid (declclass f) \<noteq> pid accC"
   7.438 - ) "G\<turnstile> C \<preceq>\<^sub>C accC"
   7.439 +  shows "G\<turnstile> C \<preceq>\<^sub>C accC"
   7.440  proof -
   7.441    from dyn_acc prot field instance_field outside
   7.442    show ?thesis
   7.443 @@ -2941,12 +2945,12 @@
   7.444  qed
   7.445     
   7.446  lemma dyn_accessible_static_field_Protected:
   7.447 - (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
   7.448 +  assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
   7.449               prot: "accmodi f = Protected" and
   7.450              field: "is_field f" and
   7.451       static_field: "is_static f" and
   7.452            outside: "pid (declclass f) \<noteq> pid accC"
   7.453 - ) "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
   7.454 +  shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f  \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
   7.455  proof -
   7.456    from dyn_acc prot field static_field outside
   7.457    show ?thesis
     8.1 --- a/src/HOL/Finite_Set.thy	Mon Feb 25 20:46:09 2002 +0100
     8.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 25 20:48:14 2002 +0100
     8.3 @@ -265,10 +265,10 @@
     8.4    apply simp
     8.5    done
     8.6  
     8.7 -lemma finite_lessThan [iff]: (fixes k :: nat) "finite {..k(}"
     8.8 +lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
     8.9    by (induct k) (simp_all add: lessThan_Suc)
    8.10  
    8.11 -lemma finite_atMost [iff]: (fixes k :: nat) "finite {..k}"
    8.12 +lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
    8.13    by (induct k) (simp_all add: atMost_Suc)
    8.14  
    8.15  lemma bounded_nat_set_is_finite:
    8.16 @@ -814,10 +814,12 @@
    8.17      apply auto
    8.18    done
    8.19  
    8.20 -lemma setsum_UN_disjoint: (fixes f :: "'a => 'b::plus_ac0")
    8.21 -  "finite I ==> (ALL i:I. finite (A i)) ==>
    8.22 -      (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
    8.23 -    setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
    8.24 +lemma setsum_UN_disjoint:
    8.25 +  fixes f :: "'a => 'b::plus_ac0"
    8.26 +  shows
    8.27 +    "finite I ==> (ALL i:I. finite (A i)) ==>
    8.28 +        (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
    8.29 +      setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
    8.30    apply (induct set: Finites)
    8.31     apply simp
    8.32    apply atomize
    8.33 @@ -939,7 +941,7 @@
    8.34    apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
    8.35    done
    8.36  
    8.37 -theorem n_subsets: "finite A ==> card {B. B <= A & card(B) = k} = (card A choose k)"
    8.38 +theorem n_subsets: "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
    8.39    by (simp add: n_sub_lemma)
    8.40  
    8.41  end
     9.1 --- a/src/HOL/HOL.thy	Mon Feb 25 20:46:09 2002 +0100
     9.2 +++ b/src/HOL/HOL.thy	Mon Feb 25 20:48:14 2002 +0100
     9.3 @@ -201,7 +201,10 @@
     9.4  subsubsection {* Intuitionistic Reasoning *}
     9.5  
     9.6  lemma impE':
     9.7 -  (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
     9.8 +  assumes 1: "P --> Q"
     9.9 +    and 2: "Q ==> R"
    9.10 +    and 3: "P --> Q ==> P"
    9.11 +  shows R
    9.12  proof -
    9.13    from 3 and 1 have P .
    9.14    with 1 have Q by (rule impE)
    9.15 @@ -209,13 +212,18 @@
    9.16  qed
    9.17  
    9.18  lemma allE':
    9.19 -  (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
    9.20 +  assumes 1: "ALL x. P x"
    9.21 +    and 2: "P x ==> ALL x. P x ==> Q"
    9.22 +  shows Q
    9.23  proof -
    9.24    from 1 have "P x" by (rule spec)
    9.25    from this and 1 show Q by (rule 2)
    9.26  qed
    9.27  
    9.28 -lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
    9.29 +lemma notE':
    9.30 +  assumes 1: "~ P"
    9.31 +    and 2: "~ P ==> P"
    9.32 +  shows R
    9.33  proof -
    9.34    from 2 and 1 have P .
    9.35    with 1 show R by (rule notE)
    9.36 @@ -309,7 +317,8 @@
    9.37  lemma eta_contract_eq: "(%s. f s) = f" ..
    9.38  
    9.39  lemma simp_thms:
    9.40 -  (not_not: "(~ ~ P) = P" and
    9.41 +  shows not_not: "(~ ~ P) = P"
    9.42 +  and
    9.43      "(P ~= Q) = (P = (~Q))"
    9.44      "(P | ~P) = True"    "(~P | P) = True"
    9.45      "((~P) = (~Q)) = (P=Q)"
    9.46 @@ -333,7 +342,7 @@
    9.47      "!!P. (EX x. x=t & P(x)) = P(t)"
    9.48      "!!P. (EX x. t=x & P(x)) = P(t)"
    9.49      "!!P. (ALL x. x=t --> P(x)) = P(t)"
    9.50 -    "!!P. (ALL x. t=x --> P(x)) = P(t)")
    9.51 +    "!!P. (ALL x. t=x --> P(x)) = P(t)"
    9.52    by (blast, blast, blast, blast, blast, rules+)
    9.53   
    9.54  lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
    9.55 @@ -360,19 +369,19 @@
    9.56    by (rules | blast)+
    9.57  
    9.58  lemma eq_ac:
    9.59 - (eq_commute: "(a=b) = (b=a)" and
    9.60 -  eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
    9.61 -  eq_assoc: "((P=Q)=R) = (P=(Q=R))") by (rules, blast+)
    9.62 +  shows eq_commute: "(a=b) = (b=a)"
    9.63 +    and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
    9.64 +    and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
    9.65  lemma neq_commute: "(a~=b) = (b~=a)" by rules
    9.66  
    9.67  lemma conj_comms:
    9.68 - (conj_commute: "(P&Q) = (Q&P)" and
    9.69 -  conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by rules+
    9.70 +  shows conj_commute: "(P&Q) = (Q&P)"
    9.71 +    and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
    9.72  lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
    9.73  
    9.74  lemma disj_comms:
    9.75 - (disj_commute: "(P|Q) = (Q|P)" and
    9.76 -  disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by rules+
    9.77 +  shows disj_commute: "(P|Q) = (Q|P)"
    9.78 +    and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
    9.79  lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
    9.80  
    9.81  lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
    10.1 --- a/src/HOL/Induct/Term.thy	Mon Feb 25 20:46:09 2002 +0100
    10.2 +++ b/src/HOL/Induct/Term.thy	Mon Feb 25 20:48:14 2002 +0100
    10.3 @@ -42,9 +42,9 @@
    10.4  text {* \medskip Alternative induction rule *}
    10.5  
    10.6  lemma
    10.7 -  (assumes var: "!!v. P (Var v)"
    10.8 -    and app: "!!f ts. list_all P ts ==> P (App f ts)")
    10.9 -  term_induct2: "P t"
   10.10 +  assumes var: "!!v. P (Var v)"
   10.11 +    and app: "!!f ts. list_all P ts ==> P (App f ts)"
   10.12 +  shows term_induct2: "P t"
   10.13  and "list_all P ts"
   10.14    apply (induct t and ts)
   10.15       apply (rule var)
    11.1 --- a/src/HOL/Set.thy	Mon Feb 25 20:46:09 2002 +0100
    11.2 +++ b/src/HOL/Set.thy	Mon Feb 25 20:48:14 2002 +0100
    11.3 @@ -212,7 +212,7 @@
    11.4  lemma CollectD: "a : {x. P(x)} ==> P(a)"
    11.5    by simp
    11.6  
    11.7 -lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B"
    11.8 +lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
    11.9    apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
   11.10     apply (rule Collect_mem_eq)
   11.11    apply (rule Collect_mem_eq)
    12.1 --- a/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:46:09 2002 +0100
    12.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Feb 25 20:48:14 2002 +0100
    12.3 @@ -58,9 +58,9 @@
    12.4    done
    12.5  
    12.6  theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
    12.7 -  (assumes a: "(a, b) : r^*"
    12.8 -    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
    12.9 -  "P b"
   12.10 +  assumes a: "(a, b) : r^*"
   12.11 +    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z"
   12.12 +  shows "P b"
   12.13  proof -
   12.14    from a have "a = a --> P b"
   12.15      by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
   12.16 @@ -151,14 +151,16 @@
   12.17    done
   12.18  
   12.19  theorem rtrancl_converseD:
   12.20 -  (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
   12.21 +  assumes r: "(x, y) \<in> (r^-1)^*"
   12.22 +  shows "(y, x) \<in> r^*"
   12.23  proof -
   12.24    from r show ?thesis
   12.25      by induct (rules intro: rtrancl_trans dest!: converseD)+
   12.26  qed
   12.27  
   12.28  theorem rtrancl_converseI:
   12.29 -  (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
   12.30 +  assumes r: "(y, x) \<in> r^*"
   12.31 +  shows "(x, y) \<in> (r^-1)^*"
   12.32  proof -
   12.33    from r show ?thesis
   12.34      by induct (rules intro: rtrancl_trans converseI)+
   12.35 @@ -168,9 +170,9 @@
   12.36    by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
   12.37  
   12.38  theorem converse_rtrancl_induct:
   12.39 -  (assumes major: "(a, b) : r^*"
   12.40 -   and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
   12.41 -    "P a"
   12.42 +  assumes major: "(a, b) : r^*"
   12.43 +    and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
   12.44 +  shows "P a"
   12.45  proof -
   12.46    from rtrancl_converseI [OF major]
   12.47    show ?thesis
    13.1 --- a/src/HOL/ex/Locales.thy	Mon Feb 25 20:46:09 2002 +0100
    13.2 +++ b/src/HOL/ex/Locales.thy	Mon Feb 25 20:48:14 2002 +0100
    13.3 @@ -143,8 +143,8 @@
    13.4  *}
    13.5  
    13.6  theorem (in group_context)
    13.7 -  (assumes eq: "e \<cdot> x = x")
    13.8 -  one_equality: "\<one> = e"
    13.9 +  assumes eq: "e \<cdot> x = x"
   13.10 +  shows one_equality: "\<one> = e"
   13.11  proof -
   13.12    have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
   13.13    also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
   13.14 @@ -155,8 +155,8 @@
   13.15  qed
   13.16  
   13.17  theorem (in group_context)
   13.18 -  (assumes eq: "x' \<cdot> x = \<one>")
   13.19 -  inv_equality: "x\<inv> = x'"
   13.20 +  assumes eq: "x' \<cdot> x = \<one>"
   13.21 +  shows inv_equality: "x\<inv> = x'"
   13.22  proof -
   13.23    have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
   13.24    also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
   13.25 @@ -214,8 +214,8 @@
   13.26  qed
   13.27  
   13.28  theorem (in group_context)
   13.29 -  (assumes eq: "x\<inv> = y\<inv>")
   13.30 -  inv_inject: "x = y"
   13.31 +  assumes eq: "x\<inv> = y\<inv>"
   13.32 +  shows inv_inject: "x = y"
   13.33  proof -
   13.34    have "x = x \<cdot> \<one>" by (simp only: right_one)
   13.35    also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
   13.36 @@ -335,8 +335,9 @@
   13.37    versions of the @{text group} locale above.
   13.38  *}
   13.39  
   13.40 -lemma (uses group G + group H)
   13.41 -  "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
   13.42 +lemma
   13.43 +  uses group G + group H
   13.44 +  shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
   13.45    "x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
   13.46    "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
   13.47  
    14.1 --- a/src/ZF/Induct/Tree_Forest.thy	Mon Feb 25 20:46:09 2002 +0100
    14.2 +++ b/src/ZF/Induct/Tree_Forest.thy	Mon Feb 25 20:48:14 2002 +0100
    14.3 @@ -53,9 +53,11 @@
    14.4    apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
    14.5    done
    14.6  
    14.7 -lemma (notes rews = tree_forest.con_defs tree_def forest_def)
    14.8 -  tree_forest_unfold: "tree_forest(A) =
    14.9 -    (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
   14.10 +lemma
   14.11 +  notes rews = tree_forest.con_defs tree_def forest_def
   14.12 +  shows
   14.13 +    tree_forest_unfold: "tree_forest(A) =
   14.14 +      (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
   14.15      -- {* NOT useful, but interesting \dots *}
   14.16    apply (unfold tree_def forest_def)
   14.17    apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
   14.18 @@ -169,9 +171,10 @@
   14.19    \medskip @{text map}.
   14.20  *}
   14.21  
   14.22 -lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
   14.23 -    map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
   14.24 -  and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
   14.25 +lemma
   14.26 +  assumes h_type: "!!x. x \<in> A ==> h(x): B"
   14.27 +  shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
   14.28 +    and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
   14.29    apply (induct rule: tree_forest.mutual_induct)
   14.30      apply (insert h_type)
   14.31      apply simp_all