--- a/src/FOL/IFOL.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/FOL/IFOL.thy Mon Feb 25 20:48:14 2002 +0100
@@ -126,7 +126,10 @@
subsection {* Intuitionistic Reasoning *}
lemma impE':
- (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+ assumes 1: "P --> Q"
+ and 2: "Q ==> R"
+ and 3: "P --> Q ==> P"
+ shows R
proof -
from 3 and 1 have P .
with 1 have Q by (rule impE)
@@ -134,13 +137,18 @@
qed
lemma allE':
- (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
+ assumes 1: "ALL x. P(x)"
+ and 2: "P(x) ==> ALL x. P(x) ==> Q"
+ shows Q
proof -
from 1 have "P(x)" by (rule spec)
from this and 1 show Q by (rule 2)
qed
-lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+lemma notE':
+ assumes 1: "~ P"
+ and 2: "~ P ==> P"
+ shows R
proof -
from 2 and 1 have P .
with 1 show R by (rule notE)
--- a/src/HOL/Bali/AxSound.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/AxSound.thy Mon Feb 25 20:48:14 2002 +0100
@@ -247,11 +247,11 @@
done
corollary evaln_type_sound:
- (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
- wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
- conf_s0: "s0\<Colon>\<preceq>(G,L)" and
- wf: "wf_prog G"
- ) "s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and>
+ assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
+ wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
+ conf_s0: "s0\<Colon>\<preceq>(G,L)" and
+ wf: "wf_prog G"
+ shows "s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and>
(error_free s0 = error_free s1)"
proof -
from evaln wt conf_s0 wf
--- a/src/HOL/Bali/Decl.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/Decl.thy Mon Feb 25 20:48:14 2002 +0100
@@ -723,12 +723,12 @@
qed
lemma ws_interface_induct [consumes 2, case_names Step]:
- (assumes is_if_I: "is_iface G I" and
+ assumes is_if_I: "is_iface G I" and
ws: "ws_prog G" and
hyp_sub: "\<And>I i. \<lbrakk>iface G I = Some i;
\<forall> J \<in> set (isuperIfs i).
(I,J)\<in>subint1 G \<and> P J \<and> is_iface G J\<rbrakk> \<Longrightarrow> P I"
- ) "P I"
+ shows "P I"
proof -
from is_if_I ws
show "P I"
--- a/src/HOL/Bali/DeclConcepts.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Mon Feb 25 20:48:14 2002 +0100
@@ -1007,10 +1007,10 @@
split: memberdecl.splits)
lemma unique_member_of:
- (assumes n: "G\<turnstile>n member_of C" and
+ assumes n: "G\<turnstile>n member_of C" and
m: "G\<turnstile>m member_of C" and
eqid: "memberid n = memberid m"
- ) "n=m"
+ shows "n=m"
proof -
from n m eqid
show "n=m"
@@ -1173,9 +1173,9 @@
by (cases "accmodi m") (auto simp add: permits_acc_def)
lemma dyn_accessible_from_static_declC:
- (assumes acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
+ assumes acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and
static: "is_static m"
- ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
+ shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
proof -
from acc_C static
show "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
@@ -1304,11 +1304,11 @@
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
lemma member_of_inheritance:
- (assumes m: "G\<turnstile>m member_of D" and
+ assumes m: "G\<turnstile>m member_of D" and
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and
ws: "ws_prog G"
- ) "G\<turnstile>m member_of C"
+ shows "G\<turnstile>m member_of C"
proof -
from m subclseq_D_C subclseq_C_m
show ?thesis
@@ -1352,13 +1352,13 @@
qed
lemma member_of_subcls:
- (assumes old: "G\<turnstile>old member_of C" and
+ assumes old: "G\<turnstile>old member_of C" and
new: "G\<turnstile>new member_of D" and
eqid: "memberid new = memberid old" and
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and
subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and
ws: "ws_prog G"
- ) "G\<turnstile>D \<prec>\<^sub>C C"
+ shows "G\<turnstile>D \<prec>\<^sub>C C"
proof -
from old
have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old"
@@ -1423,10 +1423,10 @@
lemma inherited_field_access:
- (assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
+ assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and
is_field: "is_field membr" and
subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC"
- ) "G\<turnstile>membr in dynC dyn_accessible_from accC"
+ shows "G\<turnstile>membr in dynC dyn_accessible_from accC"
proof -
from stat_acc is_field subclseq
show ?thesis
@@ -1437,11 +1437,11 @@
qed
lemma accessible_inheritance:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+ assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
member_dynC: "G\<turnstile>m member_of dynC" and
dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)"
- ) "G\<turnstile>m of dynC accessible_from accC"
+ shows "G\<turnstile>m of dynC accessible_from accC"
proof -
from stat_acc
have member_statC: "G\<turnstile>m member_of statC"
@@ -1664,13 +1664,13 @@
done
lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
- (assumes im: "im \<in> imethds G I sig" and
+ assumes im: "im \<in> imethds G I sig" and
ifI: "iface G I = Some i" and
ws: "ws_prog G" and
hyp_new: "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig
= Some im \<Longrightarrow> P" and
hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
- ) "P"
+ shows P
proof -
from ifI ws im hyp_new hyp_inh
show "P"
@@ -1756,9 +1756,9 @@
by (auto dest: methd_declC method_declared_inI)
lemma member_methd:
- (assumes member_of: "G\<turnstile>Methd sig m member_of C" and
+ assumes member_of: "G\<turnstile>Methd sig m member_of C" and
ws: "ws_prog G"
- ) "methd G C sig = Some m"
+ shows "methd G C sig = Some m"
proof -
from member_of
have iscls_C: "is_class G C"
@@ -2013,13 +2013,13 @@
by (auto simp add: dynmethd_rec)
lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
- (assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
+ assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
is_cls_dynC: "is_class G dynC" and
ws: "ws_prog G" and
hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
- ) "P"
+ shows P
proof -
from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
from clsDynC ws dynM hyp_static hyp_override
@@ -2037,13 +2037,12 @@
qed
lemma no_override_in_Object:
- (assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
+ assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
is_cls_dynC: "is_class G dynC" and
ws: "ws_prog G" and
statM: "methd G statC sig = Some statM" and
neq_dynM_statM: "dynM\<noteq>statM"
- )
- "dynC \<noteq> Object"
+ shows "dynC \<noteq> Object"
proof -
from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
from clsDynC ws dynM statM neq_dynM_statM
@@ -2063,7 +2062,7 @@
lemma dynmethd_Some_rec_cases [consumes 3,
case_names Static Override Recursion]:
-(assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
+ assumes dynM: "dynmethd G statC dynC sig = Some dynM" and
clsDynC: "class G dynC = Some c" and
ws: "ws_prog G" and
hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
@@ -2072,8 +2071,8 @@
G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
- dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
- ) "P"
+ dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
+ shows P
proof -
from clsDynC have "is_class G dynC" by simp
note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
@@ -2139,12 +2138,12 @@
qed
lemma methd_Some_dynmethd_Some:
- (assumes statM: "methd G statC sig = Some statM" and
+ assumes statM: "methd G statC sig = Some statM" and
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
is_cls_statC: "is_class G statC" and
ws: "ws_prog G"
- ) "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
- (is "?P dynC")
+ shows "\<exists> dynM. dynmethd G statC dynC sig = Some dynM"
+ (is "?P dynC")
proof -
from subclseq is_cls_statC
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
@@ -2185,7 +2184,7 @@
qed
lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
- (assumes statM: "methd G statC sig = Some statM" and
+ assumes statM: "methd G statC sig = Some statM" and
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
is_cls_statC: "is_class G statC" and
ws: "ws_prog G" and
@@ -2193,7 +2192,7 @@
hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
dynM\<noteq>statM;
G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
- ) "P"
+ shows P
proof -
from subclseq is_cls_statC
have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
@@ -2215,13 +2214,13 @@
qed
lemma ws_dynmethd:
- (assumes statM: "methd G statC sig = Some statM" and
+ assumes statM: "methd G statC sig = Some statM" and
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
is_cls_statC: "is_class G statC" and
ws: "ws_prog G"
- )
- "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
- is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
+ shows
+ "\<exists> dynM. dynmethd G statC dynC sig = Some dynM \<and>
+ is_static dynM = is_static statM \<and> G\<turnstile>resTy dynM\<preceq>resTy statM"
proof -
from statM subclseq is_cls_statC ws
show ?thesis
--- a/src/HOL/Bali/Evaln.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy Mon Feb 25 20:48:14 2002 +0100
@@ -324,12 +324,12 @@
done
lemma evaln_eval:
- (assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
+ assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
conf_s0: "s0\<Colon>\<preceq>(G, L)" and
wf: "wf_prog G"
- ) "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
+ shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
proof -
from evaln
show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
@@ -477,8 +477,9 @@
next
case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT
v vs L accC T)
- (* Repeats large parts of the type soundness proof. One should factor
- out some lemmata about the relations and conformance of s2, s3 and s3'*)
+ txt {* Repeats large parts of the type soundness proof. One should factor
+ out some lemmata about the relations and conformance of @{text
+ s2}, @{text s3} and @{text s3'} *}
have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
have invDeclC: "invDeclC
@@ -934,8 +935,7 @@
show ?thesis
by simp
qed
- from cls this
- show ?case
+ with cls show ?case
by (rule eval.Init)
qed
qed
@@ -994,13 +994,14 @@
show ?thesis .
qed
+text {* *} (* FIXME *)
lemma eval_evaln:
- (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
- wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
- conf_s0: "s0\<Colon>\<preceq>(G, L)" and
- wf: "wf_prog G"
- ) "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
+ assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
+ wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
+ conf_s0: "s0\<Colon>\<preceq>(G, L)" and
+ wf: "wf_prog G"
+ shows "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
proof -
from eval
show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
@@ -1185,7 +1186,7 @@
with xcpt_s2 conf_s2 wf
have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
by (auto dest: Try_lemma)
- (* FIXME extract lemma for this conformance, also usefull for
+ (* FIXME extract lemma for this conformance, also useful for
eval_type_sound and evaln_eval *)
from this wt_c2
obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
--- a/src/HOL/Bali/TypeSafe.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/TypeSafe.thy Mon Feb 25 20:48:14 2002 +0100
@@ -10,9 +10,9 @@
section "error free"
lemma error_free_halloc:
- (assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
+ assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
error_free_s0: "error_free s0"
- ) "error_free s1"
+ shows "error_free s1"
proof -
from halloc error_free_s0
obtain abrupt0 store0 abrupt1 store1
@@ -37,8 +37,8 @@
qed
lemma error_free_sxalloc:
- (assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0")
- "error_free s1"
+ assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
+ shows "error_free s1"
proof -
from sxalloc error_free_s0
obtain abrupt0 store0 abrupt1 store1
@@ -857,17 +857,17 @@
(* #### stat raus und gleich is_static f schreiben *)
theorem dynamic_field_access_ok:
- (assumes wf: "wf_prog G" and
- not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
- conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
- conform_s: "s\<Colon>\<preceq>(G, L)" and
- normal_s: "normal s" and
- wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
- f: "accfield G accC statC fn = Some f" and
- dynC: "if stat then dynC=declclass f
- else dynC=obj_class (lookup_obj (store s) a)" and
- stat: "if stat then (is_static f) else (\<not> is_static f)"
- ) "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and>
+ assumes wf: "wf_prog G" and
+ not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
+ conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
+ conform_s: "s\<Colon>\<preceq>(G, L)" and
+ normal_s: "normal s" and
+ wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
+ f: "accfield G accC statC fn = Some f" and
+ dynC: "if stat then dynC=declclass f
+ else dynC=obj_class (lookup_obj (store s) a)" and
+ stat: "if stat then (is_static f) else (\<not> is_static f)"
+ shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f) \<and>
G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
proof (cases "stat")
case True
@@ -1017,7 +1017,7 @@
*)
lemma error_free_field_access:
- (assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
+ assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
@@ -1025,7 +1025,7 @@
conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
wf: "wf_prog G"
- ) "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
+ shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
proof -
from fvar
have store_s2': "store s2'=store s2"
@@ -1066,12 +1066,12 @@
qed
lemma call_access_ok:
-(assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
- and wf: "wf_prog G"
- and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
- and statM: "(statDeclT,statM) \<in> mheads G accC statT sig"
- and invC: "invC = invocation_class (invmode statM e) s a statT"
-)"\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
+ assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
+ and wf: "wf_prog G"
+ and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
+ and statM: "(statDeclT,statM) \<in> mheads G accC statT sig"
+ and invC: "invC = invocation_class (invmode statM e) s a statT"
+ shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
proof -
from wt_e wf have type_statT: "is_type G (RefT statT)"
@@ -1123,7 +1123,7 @@
qed
lemma error_free_call_access:
- (assumes
+ assumes
eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and
statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr>
@@ -1138,7 +1138,7 @@
invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2)
a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
wf: "wf_prog G"
- )"check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
+ shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
= s3"
proof (cases "normal s2")
case False
@@ -1198,11 +1198,11 @@
section "main proof of type safety"
lemma eval_type_sound:
- (assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
- wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
- wf: "wf_prog G" and
- conf_s0: "s0\<Colon>\<preceq>(G,L)"
- ) "s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and>
+ assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
+ wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and
+ wf: "wf_prog G" and
+ conf_s0: "s0\<Colon>\<preceq>(G,L)"
+ shows "s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and>
(error_free s0 = error_free s1)"
proof -
from eval
--- a/src/HOL/Bali/WellForm.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Bali/WellForm.thy Mon Feb 25 20:48:14 2002 +0100
@@ -718,7 +718,8 @@
qed
lemma wf_prog_hidesD:
- (assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G")
+ assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G"
+ shows
"accmodi old \<le> accmodi new \<and>
is_static old"
proof -
@@ -759,7 +760,8 @@
@{text wf_prog_dyn_override_prop}.
*}
lemma wf_prog_stat_overridesD:
- (assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G")
+ assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
+ shows
"G\<turnstile>resTy new\<preceq>resTy old \<and>
accmodi old \<le> accmodi new \<and>
\<not> is_static old"
@@ -790,8 +792,8 @@
qed
lemma static_to_dynamic_overriding:
- (assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G")
- "G\<turnstile>new overrides old"
+ assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G"
+ shows "G\<turnstile>new overrides old"
proof -
from stat_override
show ?thesis (is "?Overrides new old")
@@ -827,14 +829,14 @@
qed
lemma non_Package_instance_method_inheritance:
-(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
- accmodi_old: "accmodi old \<noteq> Package" and
- instance_method: "\<not> is_static old" and
- subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
- old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
- wf: "wf_prog G"
-) "G\<turnstile>Method old member_of C \<or>
- (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
+ assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
+ accmodi_old: "accmodi old \<noteq> Package" and
+ instance_method: "\<not> is_static old" and
+ subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
+ old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
+ wf: "wf_prog G"
+ shows "G\<turnstile>Method old member_of C \<or>
+ (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
proof -
from wf have ws: "ws_prog G" by auto
from old_declared have iscls_declC_old: "is_class G (declclass old)"
@@ -989,17 +991,17 @@
lemma non_Package_instance_method_inheritance_cases [consumes 6,
case_names Inheritance Overriding]:
-(assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
- accmodi_old: "accmodi old \<noteq> Package" and
- instance_method: "\<not> is_static old" and
- subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
- old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
- wf: "wf_prog G" and
- inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
- overriding: "\<And> new.
+ assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
+ accmodi_old: "accmodi old \<noteq> Package" and
+ instance_method: "\<not> is_static old" and
+ subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
+ old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
+ wf: "wf_prog G" and
+ inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
+ overriding: "\<And> new.
\<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
\<Longrightarrow> P"
-) "P"
+ shows P
proof -
from old_inheritable accmodi_old instance_method subcls old_declared wf
inheritance overriding
@@ -1008,10 +1010,10 @@
qed
lemma dynamic_to_static_overriding:
-(assumes dyn_override: "G\<turnstile> new overrides old" and
- accmodi_old: "accmodi old \<noteq> Package" and
- wf: "wf_prog G"
-) "G\<turnstile> new overrides\<^sub>S old"
+ assumes dyn_override: "G\<turnstile> new overrides old" and
+ accmodi_old: "accmodi old \<noteq> Package" and
+ wf: "wf_prog G"
+ shows "G\<turnstile> new overrides\<^sub>S old"
proof -
from dyn_override accmodi_old
show ?thesis (is "?Overrides new old")
@@ -1101,9 +1103,9 @@
qed
lemma wf_prog_dyn_override_prop:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
+ assumes dyn_override: "G \<turnstile> new overrides old" and
wf: "wf_prog G"
- ) "accmodi old \<le> accmodi new"
+ shows "accmodi old \<le> accmodi new"
proof (cases "accmodi old = Package")
case True
note old_Package = this
@@ -1130,10 +1132,10 @@
qed
lemma overrides_Package_old:
-(assumes dyn_override: "G \<turnstile> new overrides old" and
- accmodi_new: "accmodi new = Package" and
- wf: "wf_prog G "
-) "accmodi old = Package"
+ assumes dyn_override: "G \<turnstile> new overrides old" and
+ accmodi_new: "accmodi new = Package" and
+ wf: "wf_prog G "
+ shows "accmodi old = Package"
proof (cases "accmodi old")
case Private
with dyn_override show ?thesis
@@ -1166,11 +1168,11 @@
qed
lemma dyn_override_Package:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
- accmodi_old: "accmodi old = Package" and
- accmodi_new: "accmodi new = Package" and
+ assumes dyn_override: "G \<turnstile> new overrides old" and
+ accmodi_old: "accmodi old = Package" and
+ accmodi_new: "accmodi new = Package" and
wf: "wf_prog G"
- ) "pid (declclass old) = pid (declclass new)"
+ shows "pid (declclass old) = pid (declclass new)"
proof -
from dyn_override accmodi_old accmodi_new
show ?thesis (is "?EqPid old new")
@@ -1195,11 +1197,11 @@
qed
lemma dyn_override_Package_escape:
- (assumes dyn_override: "G \<turnstile> new overrides old" and
- accmodi_old: "accmodi old = Package" and
- outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
+ assumes dyn_override: "G \<turnstile> new overrides old" and
+ accmodi_old: "accmodi old = Package" and
+ outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
wf: "wf_prog G"
- ) "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
+ shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
pid (declclass old) = pid (declclass inter) \<and>
Protected \<le> accmodi inter"
proof -
@@ -1373,10 +1375,11 @@
qed
lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
-(assumes methd_C: "methd G C sig = Some m" and
- ws: "ws_prog G" and
- clsC: "class G C = Some c" and
- neq_C_Obj: "C\<noteq>Object" )
+ assumes methd_C: "methd G C sig = Some m" and
+ ws: "ws_prog G" and
+ clsC: "class G C = Some c" and
+ neq_C_Obj: "C\<noteq>Object"
+ shows
"\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P;
\<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P
\<rbrakk> \<Longrightarrow> P"
@@ -1406,8 +1409,9 @@
lemma methd_member_of:
- (assumes wf: "wf_prog G")
- "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C"
+ assumes wf: "wf_prog G"
+ shows
+ "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C"
(is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C")
proof -
from wf have ws: "ws_prog G" ..
@@ -1452,13 +1456,13 @@
intro: filter_tab_SomeI override_find_right table_of_map_SomeI)
lemma wf_prog_staticD:
- (assumes wf: "wf_prog G" and
+ assumes wf: "wf_prog G" and
clsC: "class G C = Some c" and
neq_C_Obj: "C \<noteq> Object" and
old: "methd G (super c) sig = Some old" and
accmodi_old: "Protected \<le> accmodi old" and
new: "table_of (methods c) sig = Some new"
- ) "is_static new = is_static old"
+ shows "is_static new = is_static old"
proof -
from clsC wf
have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
@@ -1508,13 +1512,13 @@
qed
lemma inheritable_instance_methd:
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+ assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected \<le> accmodi old" and
not_static_old: "\<not> is_static old"
- )
+ shows
"\<exists>new. methd G C sig = Some new \<and>
(new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)"
(is "(\<exists>new. (?Constraint C new old))")
@@ -1644,7 +1648,7 @@
lemma inheritable_instance_methd_cases [consumes 6
, case_names Inheritance Overriding]:
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+ assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
@@ -1654,7 +1658,7 @@
overriding: "\<And> new. \<lbrakk>methd G C sig = Some new;
G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P"
- ) "P"
+ shows P
proof -
from subclseq_C_D is_cls_D wf old accmodi_old not_static_old
show ?thesis
@@ -1662,13 +1666,13 @@
qed
lemma inheritable_instance_methd_props:
- (assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
+ assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected \<le> accmodi old" and
not_static_old: "\<not> is_static old"
- )
+ shows
"\<exists>new. methd G C sig = Some new \<and>
\<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new"
(is "(\<exists>new. (?Constraint C new old))")
@@ -1976,11 +1980,11 @@
*)
lemma dynmethd_Object:
- (assumes statM: "methd G Object sig = Some statM" and
+ assumes statM: "methd G Object sig = Some statM" and
private: "accmodi statM = Private" and
is_cls_C: "is_class G C" and
wf: "wf_prog G"
- ) "dynmethd G Object C sig = Some statM"
+ shows "dynmethd G Object C sig = Some statM"
proof -
from is_cls_C wf
have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object"
@@ -2002,12 +2006,12 @@
qed
lemma wf_imethds_hiding_objmethdsD:
- (assumes old: "methd G Object sig = Some old" and
- is_if_I: "is_iface G I" and
- wf: "wf_prog G" and
- not_private: "accmodi old \<noteq> Private" and
- new: "new \<in> imethds G I sig"
- ) "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
+ assumes old: "methd G Object sig = Some old" and
+ is_if_I: "is_iface G I" and
+ wf: "wf_prog G" and
+ not_private: "accmodi old \<noteq> Private" and
+ new: "new \<in> imethds G I sig"
+ shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new")
proof -
from wf have ws: "ws_prog G" by simp
{
@@ -2102,10 +2106,10 @@
"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)"
lemma valid_lookup_cls_is_class:
- (assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
+ assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and
ty_statT: "isrtype G statT" and
wf: "wf_prog G"
- ) "is_class G dynC"
+ shows "is_class G dynC"
proof (cases statT)
case NullT
with dynC ty_statT show ?thesis
@@ -2503,10 +2507,10 @@
static_to_dynamic_overriding)
lemma static_to_dynamic_accessible_from:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+ assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
wf: "wf_prog G"
- ) "G\<turnstile>m in dynC dyn_accessible_from accC"
+ shows "G\<turnstile>m in dynC dyn_accessible_from accC"
proof -
from stat_acc subclseq
show ?thesis (is "?Dyn_accessible m")
@@ -2528,10 +2532,10 @@
qed
lemma static_to_dynamic_accessible_from_static:
- (assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
+ assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and
static: "is_static m" and
wf: "wf_prog G"
- ) "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
+ shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC"
proof -
from stat_acc wf
have "G\<turnstile>m in statC dyn_accessible_from accC"
@@ -2542,10 +2546,10 @@
qed
lemma dynmethd_member_in:
- (assumes m: "dynmethd G statC dynC sig = Some m" and
+ assumes m: "dynmethd G statC dynC sig = Some m" and
iscls_statC: "is_class G statC" and
wf: "wf_prog G"
- ) "G\<turnstile>Methd sig m member_in dynC"
+ shows "G\<turnstile>Methd sig m member_in dynC"
proof -
from m
have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
@@ -2563,11 +2567,11 @@
qed
lemma dynmethd_access_prop:
- (assumes statM: "methd G statC sig = Some statM" and
- stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
- dynM: "dynmethd G statC dynC sig = Some dynM" and
- wf: "wf_prog G"
- ) "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
+ assumes statM: "methd G statC sig = Some statM" and
+ stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and
+ dynM: "dynmethd G statC dynC sig = Some dynM" and
+ wf: "wf_prog G"
+ shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from wf have ws: "ws_prog G" ..
from dynM
@@ -2638,12 +2642,12 @@
qed
lemma implmt_methd_access:
-(fixes accC::qtname
- assumes iface_methd: "imethds G I sig \<noteq> {}" and
+ fixes accC::qtname
+ assumes iface_methd: "imethds G I sig \<noteq> {}" and
implements: "G\<turnstile>dynC\<leadsto>I" and
isif_I: "is_iface G I" and
wf: "wf_prog G"
- ) "\<exists> dynM. methd G dynC sig = Some dynM \<and>
+ shows "\<exists> dynM. methd G dynC sig = Some dynM \<and>
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from implements
@@ -2668,12 +2672,12 @@
qed
corollary implmt_dynimethd_access:
-(fixes accC::qtname
- assumes iface_methd: "imethds G I sig \<noteq> {}" and
+ fixes accC::qtname
+ assumes iface_methd: "imethds G I sig \<noteq> {}" and
implements: "G\<turnstile>dynC\<leadsto>I" and
isif_I: "is_iface G I" and
wf: "wf_prog G"
- ) "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and>
+ shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and>
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from iface_methd
@@ -2686,12 +2690,12 @@
qed
lemma dynlookup_access_prop:
- (assumes emh: "emh \<in> mheads G accC statT sig" and
+ assumes emh: "emh \<in> mheads G accC statT sig" and
dynM: "dynlookup G statT dynC sig = Some dynM" and
dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and
isT_statT: "isrtype G statT" and
wf: "wf_prog G"
- ) "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
+ shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from emh wf
have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)"
@@ -2835,11 +2839,11 @@
qed
lemma dynlookup_access:
- (assumes emh: "emh \<in> mheads G accC statT sig" and
+ assumes emh: "emh \<in> mheads G accC statT sig" and
dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and
isT_statT: "isrtype G statT" and
wf: "wf_prog G"
- ) "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and>
+ shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and>
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from dynC_prop isT_statT wf
@@ -2855,10 +2859,10 @@
qed
lemma stat_overrides_Package_old:
-(assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and
+ assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and
accmodi_new: "accmodi new = Package" and
wf: "wf_prog G "
-) "accmodi old = Package"
+ shows "accmodi old = Package"
proof -
from stat_override wf
have "accmodi old \<le> accmodi new"
@@ -2916,12 +2920,12 @@
since methods can break the package bounds due to overriding
*}
lemma dyn_accessible_instance_field_Protected:
- (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
+ assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
prot: "accmodi f = Protected" and
field: "is_field f" and
instance_field: "\<not> is_static f" and
outside: "pid (declclass f) \<noteq> pid accC"
- ) "G\<turnstile> C \<preceq>\<^sub>C accC"
+ shows "G\<turnstile> C \<preceq>\<^sub>C accC"
proof -
from dyn_acc prot field instance_field outside
show ?thesis
@@ -2941,12 +2945,12 @@
qed
lemma dyn_accessible_static_field_Protected:
- (assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
+ assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and
prot: "accmodi f = Protected" and
field: "is_field f" and
static_field: "is_static f" and
outside: "pid (declclass f) \<noteq> pid accC"
- ) "G\<turnstile> accC \<preceq>\<^sub>C declclass f \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
+ shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f"
proof -
from dyn_acc prot field static_field outside
show ?thesis
--- a/src/HOL/Finite_Set.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Finite_Set.thy Mon Feb 25 20:48:14 2002 +0100
@@ -265,10 +265,10 @@
apply simp
done
-lemma finite_lessThan [iff]: (fixes k :: nat) "finite {..k(}"
+lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..k(}"
by (induct k) (simp_all add: lessThan_Suc)
-lemma finite_atMost [iff]: (fixes k :: nat) "finite {..k}"
+lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}"
by (induct k) (simp_all add: atMost_Suc)
lemma bounded_nat_set_is_finite:
@@ -814,10 +814,12 @@
apply auto
done
-lemma setsum_UN_disjoint: (fixes f :: "'a => 'b::plus_ac0")
- "finite I ==> (ALL i:I. finite (A i)) ==>
- (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
- setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
+lemma setsum_UN_disjoint:
+ fixes f :: "'a => 'b::plus_ac0"
+ shows
+ "finite I ==> (ALL i:I. finite (A i)) ==>
+ (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
+ setsum f (UNION I A) = setsum (\<lambda>i. setsum f (A i)) I"
apply (induct set: Finites)
apply simp
apply atomize
@@ -939,7 +941,7 @@
apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
done
-theorem n_subsets: "finite A ==> card {B. B <= A & card(B) = k} = (card A choose k)"
+theorem n_subsets: "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
by (simp add: n_sub_lemma)
end
--- a/src/HOL/HOL.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/HOL.thy Mon Feb 25 20:48:14 2002 +0100
@@ -201,7 +201,10 @@
subsubsection {* Intuitionistic Reasoning *}
lemma impE':
- (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
+ assumes 1: "P --> Q"
+ and 2: "Q ==> R"
+ and 3: "P --> Q ==> P"
+ shows R
proof -
from 3 and 1 have P .
with 1 have Q by (rule impE)
@@ -209,13 +212,18 @@
qed
lemma allE':
- (assumes 1: "ALL x. P x" and 2: "P x ==> ALL x. P x ==> Q") Q
+ assumes 1: "ALL x. P x"
+ and 2: "P x ==> ALL x. P x ==> Q"
+ shows Q
proof -
from 1 have "P x" by (rule spec)
from this and 1 show Q by (rule 2)
qed
-lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
+lemma notE':
+ assumes 1: "~ P"
+ and 2: "~ P ==> P"
+ shows R
proof -
from 2 and 1 have P .
with 1 show R by (rule notE)
@@ -309,7 +317,8 @@
lemma eta_contract_eq: "(%s. f s) = f" ..
lemma simp_thms:
- (not_not: "(~ ~ P) = P" and
+ shows not_not: "(~ ~ P) = P"
+ and
"(P ~= Q) = (P = (~Q))"
"(P | ~P) = True" "(~P | P) = True"
"((~P) = (~Q)) = (P=Q)"
@@ -333,7 +342,7 @@
"!!P. (EX x. x=t & P(x)) = P(t)"
"!!P. (EX x. t=x & P(x)) = P(t)"
"!!P. (ALL x. x=t --> P(x)) = P(t)"
- "!!P. (ALL x. t=x --> P(x)) = P(t)")
+ "!!P. (ALL x. t=x --> P(x)) = P(t)"
by (blast, blast, blast, blast, blast, rules+)
lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
@@ -360,19 +369,19 @@
by (rules | blast)+
lemma eq_ac:
- (eq_commute: "(a=b) = (b=a)" and
- eq_left_commute: "(P=(Q=R)) = (Q=(P=R))" and
- eq_assoc: "((P=Q)=R) = (P=(Q=R))") by (rules, blast+)
+ shows eq_commute: "(a=b) = (b=a)"
+ and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
+ and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (rules, blast+)
lemma neq_commute: "(a~=b) = (b~=a)" by rules
lemma conj_comms:
- (conj_commute: "(P&Q) = (Q&P)" and
- conj_left_commute: "(P&(Q&R)) = (Q&(P&R))") by rules+
+ shows conj_commute: "(P&Q) = (Q&P)"
+ and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by rules+
lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by rules
lemma disj_comms:
- (disj_commute: "(P|Q) = (Q|P)" and
- disj_left_commute: "(P|(Q|R)) = (Q|(P|R))") by rules+
+ shows disj_commute: "(P|Q) = (Q|P)"
+ and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by rules+
lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by rules
lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by rules
--- a/src/HOL/Induct/Term.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Induct/Term.thy Mon Feb 25 20:48:14 2002 +0100
@@ -42,9 +42,9 @@
text {* \medskip Alternative induction rule *}
lemma
- (assumes var: "!!v. P (Var v)"
- and app: "!!f ts. list_all P ts ==> P (App f ts)")
- term_induct2: "P t"
+ assumes var: "!!v. P (Var v)"
+ and app: "!!f ts. list_all P ts ==> P (App f ts)"
+ shows term_induct2: "P t"
and "list_all P ts"
apply (induct t and ts)
apply (rule var)
--- a/src/HOL/Set.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Set.thy Mon Feb 25 20:48:14 2002 +0100
@@ -212,7 +212,7 @@
lemma CollectD: "a : {x. P(x)} ==> P(a)"
by simp
-lemma set_ext: (assumes prem: "(!!x. (x:A) = (x:B))") "A = B"
+lemma set_ext: assumes prem: "(!!x. (x:A) = (x:B))" shows "A = B"
apply (rule prem [THEN ext, THEN arg_cong, THEN box_equals])
apply (rule Collect_mem_eq)
apply (rule Collect_mem_eq)
--- a/src/HOL/Transitive_Closure.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/Transitive_Closure.thy Mon Feb 25 20:48:14 2002 +0100
@@ -58,9 +58,9 @@
done
theorem rtrancl_induct [consumes 1, induct set: rtrancl]:
- (assumes a: "(a, b) : r^*"
- and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
- "P b"
+ assumes a: "(a, b) : r^*"
+ and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z"
+ shows "P b"
proof -
from a have "a = a --> P b"
by (induct "%x y. x = a --> P y" a b) (rules intro: cases)+
@@ -151,14 +151,16 @@
done
theorem rtrancl_converseD:
- (assumes r: "(x, y) \<in> (r^-1)^*") "(y, x) \<in> r^*"
+ assumes r: "(x, y) \<in> (r^-1)^*"
+ shows "(y, x) \<in> r^*"
proof -
from r show ?thesis
by induct (rules intro: rtrancl_trans dest!: converseD)+
qed
theorem rtrancl_converseI:
- (assumes r: "(y, x) \<in> r^*") "(x, y) \<in> (r^-1)^*"
+ assumes r: "(y, x) \<in> r^*"
+ shows "(x, y) \<in> (r^-1)^*"
proof -
from r show ?thesis
by induct (rules intro: rtrancl_trans converseI)+
@@ -168,9 +170,9 @@
by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
theorem converse_rtrancl_induct:
- (assumes major: "(a, b) : r^*"
- and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y")
- "P a"
+ assumes major: "(a, b) : r^*"
+ and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y"
+ shows "P a"
proof -
from rtrancl_converseI [OF major]
show ?thesis
--- a/src/HOL/ex/Locales.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/HOL/ex/Locales.thy Mon Feb 25 20:48:14 2002 +0100
@@ -143,8 +143,8 @@
*}
theorem (in group_context)
- (assumes eq: "e \<cdot> x = x")
- one_equality: "\<one> = e"
+ assumes eq: "e \<cdot> x = x"
+ shows one_equality: "\<one> = e"
proof -
have "\<one> = x \<cdot> x\<inv>" by (simp only: right_inv)
also have "\<dots> = (e \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
@@ -155,8 +155,8 @@
qed
theorem (in group_context)
- (assumes eq: "x' \<cdot> x = \<one>")
- inv_equality: "x\<inv> = x'"
+ assumes eq: "x' \<cdot> x = \<one>"
+ shows inv_equality: "x\<inv> = x'"
proof -
have "x\<inv> = \<one> \<cdot> x\<inv>" by (simp only: left_one)
also have "\<dots> = (x' \<cdot> x) \<cdot> x\<inv>" by (simp only: eq)
@@ -214,8 +214,8 @@
qed
theorem (in group_context)
- (assumes eq: "x\<inv> = y\<inv>")
- inv_inject: "x = y"
+ assumes eq: "x\<inv> = y\<inv>"
+ shows inv_inject: "x = y"
proof -
have "x = x \<cdot> \<one>" by (simp only: right_one)
also have "\<dots> = x \<cdot> (y\<inv> \<cdot> y)" by (simp only: left_inv)
@@ -335,8 +335,9 @@
versions of the @{text group} locale above.
*}
-lemma (uses group G + group H)
- "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
+lemma
+ uses group G + group H
+ shows "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" and
"x \<cdot>\<^sub>2 y \<cdot>\<^sub>2 \<one>\<^sub>2 = prod H (prod H x y) (one H)" and
"x \<cdot> \<one>\<^sub>2 = prod G x (one H)" by (rule refl)+
--- a/src/ZF/Induct/Tree_Forest.thy Mon Feb 25 20:46:09 2002 +0100
+++ b/src/ZF/Induct/Tree_Forest.thy Mon Feb 25 20:48:14 2002 +0100
@@ -53,9 +53,11 @@
apply (auto intro!: equalityI tree_forest.intros elim: tree_forest.cases)
done
-lemma (notes rews = tree_forest.con_defs tree_def forest_def)
- tree_forest_unfold: "tree_forest(A) =
- (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
+lemma
+ notes rews = tree_forest.con_defs tree_def forest_def
+ shows
+ tree_forest_unfold: "tree_forest(A) =
+ (A \<times> forest(A)) + ({0} + tree(A) \<times> forest(A))"
-- {* NOT useful, but interesting \dots *}
apply (unfold tree_def forest_def)
apply (fast intro!: tree_forest.intros [unfolded rews, THEN PartD1]
@@ -169,9 +171,10 @@
\medskip @{text map}.
*}
-lemma (assumes h_type: "!!x. x \<in> A ==> h(x): B")
- map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
- and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
+lemma
+ assumes h_type: "!!x. x \<in> A ==> h(x): B"
+ shows map_tree_type: "t \<in> tree(A) ==> map(h,t) \<in> tree(B)"
+ and map_forest_type: "f \<in> forest(A) ==> map(h,f) \<in> forest(B)"
apply (induct rule: tree_forest.mutual_induct)
apply (insert h_type)
apply simp_all