--- a/src/HOL/Isar_examples/Hoare.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Tue Oct 30 17:37:25 2001 +0100
@@ -166,24 +166,18 @@
fix s s' assume s: "s : P"
assume "Sem (While b X c) s s'"
then obtain n where iter: "iter n b (Sem c) s s'" by auto
-
have "!!s. iter n b (Sem c) s s' ==> s : P ==> s' : P Int -b"
- (is "PROP ?P n")
proof (induct n)
- fix s assume s: "s : P"
- {
- assume "iter 0 b (Sem c) s s'"
- with s show "?thesis s" by auto
- next
- fix n assume hyp: "PROP ?P n"
- assume "iter (Suc n) b (Sem c) s s'"
- then obtain s'' where b: "s : b" and sem: "Sem c s s''"
- and iter: "iter n b (Sem c) s'' s'"
- by auto
- from s b have "s : P Int b" by simp
- with body sem have "s'' : P" ..
- with iter show "?thesis s" by (rule hyp)
- }
+ case (0 s)
+ thus ?case by auto
+ next
+ case (Suc n s)
+ then obtain s'' where b: "s : b" and sem: "Sem c s s''"
+ and iter: "iter n b (Sem c) s'' s'"
+ by auto
+ from Suc and b have "s : P Int b" by simp
+ with body sem have "s'' : P" ..
+ with iter show ?case by (rule Suc)
qed
from this iter s show "s' : P Int -b" .
qed
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Tue Oct 30 17:37:25 2001 +0100
@@ -37,19 +37,20 @@
assume "t : ?T"
thus "t Int u = {} ==> t Un u : ?T" (is "PROP ?P t")
proof (induct t)
- from u show "{} Un u : ?T" by simp
+ case empty
+ with u show "{} Un u : ?T" by simp
next
- fix a t
- assume "a : A" and hyp: "PROP ?P t"
- and at: "a <= - t" and atu: "(a Un t) Int u = {}"
+ case (Un a t)
show "(a Un t) Un u : ?T"
proof -
have "a Un (t Un u) : ?T"
proof (rule tiling.Un)
show "a : A" .
- from atu have "t Int u = {}" by blast
- thus "t Un u: ?T" by (rule hyp)
- from at atu show "a <= - (t Un u)" by blast
+ have atu: "(a Un t) Int u = {}" .
+ hence "t Int u = {}" by blast
+ thus "t Un u: ?T" by (rule Un)
+ have "a <= - t" .
+ with atu show "a <= - (t Un u)" by blast
qed
also have "a Un (t Un u) = (a Un t) Un u"
by (simp only: Un_assoc)
@@ -129,13 +130,13 @@
lemma dominoes_tile_row:
"{i} <*> below (2 * n) : tiling domino"
- (is "?P n" is "?B n : ?T")
+ (is "?B n : ?T")
proof (induct n)
- show "?P 0" by (simp add: below_0 tiling.empty)
-
- fix n assume hyp: "?P n"
+ case 0
+ show ?case by (simp add: below_0 tiling.empty)
+next
+ case (Suc n)
let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
-
have "?B (Suc n) = ?a Un ?B n"
by (auto simp add: Sigma_Suc Un_assoc)
also have "... : ?T"
@@ -144,29 +145,29 @@
by (rule domino.horiz)
also have "{(i, 2 * n), (i, 2 * n + 1)} = ?a" by blast
finally show "... : domino" .
- from hyp show "?B n : ?T" .
+ show "?B n : ?T" by (rule Suc)
show "?a <= - ?B n" by blast
qed
- finally show "?P (Suc n)" .
+ finally show ?case .
qed
lemma dominoes_tile_matrix:
"below m <*> below (2 * n) : tiling domino"
- (is "?P m" is "?B m : ?T")
+ (is "?B m : ?T")
proof (induct m)
- show "?P 0" by (simp add: below_0 tiling.empty)
-
- fix m assume hyp: "?P m"
+ case 0
+ show ?case by (simp add: below_0 tiling.empty)
+next
+ case (Suc m)
let ?t = "{m} <*> below (2 * n)"
-
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
also have "... : ?T"
proof (rule tiling_Un)
show "?t : ?T" by (rule dominoes_tile_row)
- from hyp show "?B m : ?T" .
+ show "?B m : ?T" by (rule Suc)
show "?t Int ?B m = {}" by blast
qed
- finally show "?P (Suc m)" .
+ finally show ?case .
qed
lemma domino_singleton:
@@ -213,19 +214,18 @@
lemma tiling_domino_01:
"t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
- (is "t : ?T ==> ?P t")
+ (is "t : ?T ==> _")
proof -
assume "t : ?T"
- thus "?P t"
+ thus ?thesis
proof induct
- show "?P {}" by (simp add: evnodd_def)
-
- fix a t
+ case empty
+ show ?case by (simp add: evnodd_def)
+ next
+ case (Un a t)
let ?e = evnodd
- assume "a : domino" and "t : ?T"
- and hyp: "card (?e t 0) = card (?e t 1)"
- and at: "a <= - t"
-
+ have hyp: "card (?e t 0) = card (?e t 1)" .
+ have at: "a <= - t" .
have card_suc:
"!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"
proof -
@@ -250,7 +250,7 @@
also from hyp have "card (?e t 0) = card (?e t 1)" .
also from card_suc have "Suc ... = card (?e (a Un t) 1)"
by simp
- finally show "?P (a Un t)" .
+ finally show ?case .
qed
qed
--- a/src/HOL/Isar_examples/W_correct.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Isar_examples/W_correct.thy Tue Oct 30 17:37:25 2001 +0100
@@ -46,8 +46,8 @@
proof -
assume "a |- e :: t"
thus ?thesis (is "?P a e t")
- proof (induct (open) a e t)
- case Var
+ proof induct
+ case (Var a n)
hence "n < length (map ($ s) a)" by simp
hence "map ($ s) a |- Var n :: map ($ s) a ! n"
by (rule has_type.Var)
@@ -57,7 +57,7 @@
by (simp only: app_subst_list)
finally show "?P a (Var n) (a ! n)" .
next
- case Abs
+ case (Abs a e t1 t2)
hence "$ s t1 # map ($ s) a |- e :: $ s t2"
by (simp add: app_subst_list)
hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
@@ -66,7 +66,7 @@
by (simp add: app_subst_list)
next
case App
- thus "?P a (App e1 e2) t1" by (simp add: has_type.App)
+ thus ?case by (simp add: has_type.App)
qed
qed
--- a/src/HOL/Lambda/Type.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Lambda/Type.thy Tue Oct 30 17:37:25 2001 +0100
@@ -95,11 +95,11 @@
subsection {* n-ary function types *}
-lemma list_app_typeD [rule_format]:
- "\<forall>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<longrightarrow> (\<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts)"
- apply (induct_tac ts)
+lemma list_app_typeD:
+ "\<And>t T. e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+ apply (induct ts)
apply simp
- apply (intro strip)
+ apply atomize
apply simp
apply (erule_tac x = "t \<^sub>\<degree> a" in allE)
apply (erule_tac x = T in allE)
@@ -115,12 +115,11 @@
"e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T \<Longrightarrow> (\<And>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> C) \<Longrightarrow> C"
by (insert list_app_typeD) fast
-lemma list_app_typeI [rule_format]:
- "\<forall>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<longrightarrow> e \<tturnstile> ts : Ts \<longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
- apply (induct_tac ts)
- apply (intro strip)
+lemma list_app_typeI:
+ "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<^sub>\<degree>\<^sub>\<degree> ts : T"
+ apply (induct ts)
apply simp
- apply (intro strip)
+ apply atomize
apply (case_tac Ts)
apply simp
apply simp
@@ -134,15 +133,13 @@
apply blast
done
-lemma lists_typings [rule_format]:
- "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
- apply (induct_tac ts)
- apply (intro strip)
+lemma lists_typings:
+ "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+ apply (induct ts)
apply (case_tac Ts)
apply simp
apply (rule lists.Nil)
apply simp
- apply (intro strip)
apply (case_tac Ts)
apply simp
apply simp
@@ -192,11 +189,10 @@
by induct auto
qed
-lemma lift_typings [rule_format]:
- "\<forall>Ts. e \<tturnstile> ts : Ts \<longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
- apply (induct_tac ts)
+lemma lift_typings:
+ "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
+ apply (induct ts)
apply simp
- apply (intro strip)
apply (case_tac Ts)
apply auto
done
--- a/src/HOL/Library/List_Prefix.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/Library/List_Prefix.thy Tue Oct 30 17:37:25 2001 +0100
@@ -151,27 +151,25 @@
theorem parallel_decomp:
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs"
- (is "PROP ?P xs" concl is "?E xs")
proof (induct xs rule: rev_induct)
- assume "[] \<parallel> ys" hence False by auto
- thus "?E []" ..
+ case Nil
+ hence False by auto
+ thus ?case ..
next
- fix x xs
- assume hyp: "PROP ?P xs"
- assume asm: "xs @ [x] \<parallel> ys"
- show "?E (xs @ [x])"
+ case (snoc x xs)
+ show ?case
proof (rule prefix_cases)
assume le: "xs \<le> ys"
then obtain ys' where ys: "ys = xs @ ys'" ..
show ?thesis
proof (cases ys')
assume "ys' = []" with ys have "xs = ys" by simp
- with asm have "[x] \<parallel> []" by auto
+ with snoc have "[x] \<parallel> []" by auto
hence False by blast
thus ?thesis ..
next
fix c cs assume ys': "ys' = c # cs"
- with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
+ with snoc ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:)
hence "x \<noteq> c" by auto
moreover have "xs @ [x] = xs @ x # []" by simp
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:)
@@ -179,11 +177,11 @@
qed
next
assume "ys < xs" hence "ys \<le> xs @ [x]" by (simp add: strict_prefix_def)
- with asm have False by blast
+ with snoc have False by blast
thus ?thesis ..
next
assume "xs \<parallel> ys"
- with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
+ with snoc obtain as b bs c cs where neq: "(b::'a) \<noteq> c"
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs"
by blast
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp
--- a/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 30 17:33:56 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Tue Oct 30 17:37:25 2001 +0100
@@ -193,11 +193,11 @@
(*####theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
proof -
assume "G\<turnstile>S\<preceq>U"
- thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
- proof (induct (*cases*) (open) (*?P S U*) rule: widen.induct [consumes 1])
+ thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" ( *(is "PROP ?P S U")* )
+ proof (induct ( *cases* ) (open) ( *?P S U* ) rule: widen.induct [consumes 1])
case refl
fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
- (* fix T' show "PROP ?P T T".*)
+ ( * fix T' show "PROP ?P T T".* )
next
case subcls
fix T assume "G\<turnstile>Class D\<preceq>T"
@@ -215,24 +215,19 @@
theorem widen_trans: "\<lbrakk>G\<turnstile>S\<preceq>U; G\<turnstile>U\<preceq>T\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
proof -
assume "G\<turnstile>S\<preceq>U"
- thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T" (*(is "PROP ?P S U")*)
- proof (induct (*cases*) (open) (*?P S U*)) (* rule: widen.induct *)
- case refl
- fix T' assume "G\<turnstile>T\<preceq>T'" thus "G\<turnstile>T\<preceq>T'".
- (* fix T' show "PROP ?P T T".*)
+ thus "\<And>T. G\<turnstile>U\<preceq>T \<Longrightarrow> G\<turnstile>S\<preceq>T"
+ proof induct
+ case (refl T T')
+ thus "G\<turnstile>T\<preceq>T'" .
next
- case subcls
- fix T assume "G\<turnstile>Class D\<preceq>T"
+ case (subcls C D T)
then obtain E where "T = Class E" by (blast dest: widen_Class)
- from prems show "G\<turnstile>Class C\<preceq>T" proof (auto elim: rtrancl_trans) qed
+ with subcls show "G\<turnstile>Class C\<preceq>T" by (auto elim: rtrancl_trans)
next
- case null
- fix RT assume "G\<turnstile>RefT R\<preceq>RT"
+ case (null R RT)
then obtain rt where "RT = RefT rt" by (blast dest: widen_RefT)
thus "G\<turnstile>NT\<preceq>RT" by auto
qed
qed
-
-
end