--- a/src/HOL/Isar_examples/Fibonacci.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/Fibonacci.thy Wed Nov 23 22:26:13 2005 +0100
@@ -124,7 +124,7 @@
qed
lemma gcd_fib_mod:
- assumes m: "0 < m"
+ assumes "0 < m"
shows "gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)"
proof (induct n rule: nat_less_induct)
case (1 n) note hyp = this
@@ -137,7 +137,7 @@
case True then show ?thesis by simp
next
case False then have "m <= n" by simp
- from m and False have "n - m < n" by simp
+ from `0 < m` and False have "n - m < n" by simp
with hyp have "gcd (fib m, fib ((n - m) mod m))
= gcd (fib m, fib (n - m))" by simp
also have "... = gcd (fib m, fib n)"
--- a/src/HOL/Isar_examples/Hoare.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy Wed Nov 23 22:26:13 2005 +0100
@@ -160,14 +160,15 @@
semantics of \texttt{WHILE}.
*}
-theorem while: "|- (P Int b) c P ==> |- P (While b X c) (P Int -b)"
+theorem while:
+ assumes body: "|- (P Int b) c P"
+ shows "|- P (While b X c) (P Int -b)"
proof
- assume body: "|- (P Int b) c P"
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"
- proof (induct n)
+ then obtain n where "iter n b (Sem c) s s'" by auto
+ from this and s show "s' : P Int -b"
+ proof (induct n fixing: s)
case (0 s)
thus ?case by auto
next
@@ -179,7 +180,6 @@
with body sem have "s'' : P" ..
with iter show ?case by (rule Suc)
qed
- from this iter s show "s' : P Int -b" .
qed
@@ -424,8 +424,8 @@
\<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
by (auto simp: Valid_def)
-lemma iter_aux: "
- \<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
+lemma iter_aux:
+ "\<forall>s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
(\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)"
apply(induct n)
apply clarsimp
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Nov 23 22:26:13 2005 +0100
@@ -169,24 +169,21 @@
qed
lemma domino_singleton:
- assumes "d : domino" and "b < 2"
- shows "EX i j. evnodd d b = {(i, j)}"
-proof -
- from `d : domino`
- show ?thesis (is "?P d")
- proof induct
- from `b < 2` have b_cases: "b = 0 | b = 1" by arith
- fix i j
- note [simp] = evnodd_empty evnodd_insert mod_Suc
- from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
- from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
- qed
+ assumes d: "d : domino" and "b < 2"
+ shows "EX i j. evnodd d b = {(i, j)}" (is "?P d")
+ using d
+proof induct
+ from `b < 2` have b_cases: "b = 0 | b = 1" by arith
+ fix i j
+ note [simp] = evnodd_empty evnodd_insert mod_Suc
+ from b_cases show "?P {(i, j), (i, j + 1)}" by rule auto
+ from b_cases show "?P {(i, j), (i + 1, j)}" by rule auto
qed
lemma domino_finite:
- assumes "d: domino"
+ assumes d: "d: domino"
shows "finite d"
- using prems
+ using d
proof induct
fix i j :: nat
show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
@@ -197,9 +194,9 @@
subsection {* Tilings of dominoes *}
lemma tiling_domino_finite:
- assumes "t : tiling domino" (is "t : ?T")
+ assumes t: "t : tiling domino" (is "t : ?T")
shows "finite t" (is "?F t")
- using `t : ?T`
+ using t
proof induct
show "?F {}" by (rule Finites.emptyI)
fix a t assume "?F t"
@@ -208,9 +205,9 @@
qed
lemma tiling_domino_01:
- assumes "t : tiling domino" (is "t : ?T")
+ assumes t: "t : tiling domino" (is "t : ?T")
shows "card (evnodd t 0) = card (evnodd t 1)"
- using `t : ?T`
+ using t
proof induct
case empty
show ?case by (simp add: evnodd_def)
--- a/src/HOL/Lambda/Commutation.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Commutation.thy Wed Nov 23 22:26:13 2005 +0100
@@ -197,11 +197,11 @@
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
shows "\<And>b c. (a, b) \<in> R\<^sup>* \<Longrightarrow> (a, c) \<in> R\<^sup>* \<Longrightarrow>
\<exists>d. (b, d) \<in> R\<^sup>* \<and> (c, d) \<in> R\<^sup>*"
-using wf
+ using wf
proof induct
case (less x b c)
- have IH: "\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
- \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*" by(rule less)
+ note IH = `\<And>y b c. \<lbrakk>(y,x) \<in> R\<inverse>; (y,b) \<in> R\<^sup>*; (y,c) \<in> R\<^sup>*\<rbrakk>
+ \<Longrightarrow> \<exists>d. (b,d) \<in> R\<^sup>* \<and> (c,d) \<in> R\<^sup>*`
have xc: "(x, c) \<in> R\<^sup>*" .
have xb: "(x, b) \<in> R\<^sup>*" .
thus ?case
@@ -223,11 +223,11 @@
assume y'c: "(y', c) \<in> R\<^sup>*"
assume xy': "(x, y') \<in> R"
with xy obtain u where u: "(y, u) \<in> R\<^sup>*" "(y', u) \<in> R\<^sup>*"
- by (blast dest:lc)
+ by (blast dest: lc)
from yb u y'c show ?thesis
- by(blast del: rtrancl_refl
- intro:rtrancl_trans
- dest:IH[OF xy[symmetric]] IH[OF xy'[symmetric]])
+ by (blast del: rtrancl_refl
+ intro: rtrancl_trans
+ dest: IH [OF xy [symmetric]] IH [OF xy' [symmetric]])
qed
qed
qed
--- a/src/HOL/Lambda/Eta.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Eta.thy Wed Nov 23 22:26:13 2005 +0100
@@ -45,24 +45,20 @@
subsection "Properties of eta, subst and free"
-lemma subst_not_free [rule_format, simp]:
- "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
- apply (induct_tac s)
- apply (simp_all add: subst_Var)
- done
+lemma subst_not_free [simp]: "\<not> free s i \<Longrightarrow> s[t/i] = s[u/i]"
+ by (induct s fixing: i t u) (simp_all add: subst_Var)
lemma free_lift [simp]:
- "\<forall>i k. free (lift t k) i =
- (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
- apply (induct_tac t)
+ "free (lift t k) i = (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
+ apply (induct t fixing: i k)
apply (auto cong: conj_cong)
apply arith
done
lemma free_subst [simp]:
- "\<forall>i k t. free (s[t/k]) i =
+ "free (s[t/k]) i =
(free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
- apply (induct_tac s)
+ apply (induct s fixing: i k t)
prefer 2
apply simp
apply blast
@@ -71,25 +67,19 @@
apply (simp add: diff_Suc subst_Var split: nat.split)
done
-lemma free_eta [rule_format]:
- "s -e> t ==> \<forall>i. free t i = free s i"
- apply (erule eta.induct)
- apply (simp_all cong: conj_cong)
- done
+lemma free_eta: "s -e> t ==> (!!i. free t i = free s i)"
+ by (induct set: eta) (simp_all cong: conj_cong)
lemma not_free_eta:
"[| s -e> t; \<not> free s i |] ==> \<not> free t i"
- apply (simp add: free_eta)
- done
+ by (simp add: free_eta)
-lemma eta_subst [rule_format, simp]:
- "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
- apply (erule eta.induct)
- apply (simp_all add: subst_subst [symmetric])
- done
+lemma eta_subst [simp]:
+ "s -e> t ==> (!!u i. s[u/i] -e> t[u/i])"
+ by (induct set: eta) (simp_all add: subst_subst [symmetric])
-theorem lift_subst_dummy: "\<And>i dummy. \<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
- by (induct s) simp_all
+theorem lift_subst_dummy: "\<not> free s i \<Longrightarrow> lift (s[dummy/i]) i = s"
+ by (induct s fixing: i dummy) simp_all
subsection "Confluence of eta"
@@ -114,56 +104,40 @@
subsection "Congruence rules for eta*"
lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl)
+ (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
lemma rtrancl_eta_AppL: "s -e>> s' ==> s \<degree> t -e>> s' \<degree> t"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl)
+ (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
lemma rtrancl_eta_AppR: "t -e>> t' ==> s \<degree> t -e>> s \<degree> t'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
lemma rtrancl_eta_App:
"[| s -e>> s'; t -e>> t' |] ==> s \<degree> t -e>> s' \<degree> t'"
- apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
- done
+ by (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
subsection "Commutation of beta and eta"
-lemma free_beta [rule_format]:
- "s -> t ==> \<forall>i. free t i --> free s i"
- apply (erule beta.induct)
- apply simp_all
- done
+lemma free_beta:
+ "s -> t ==> (!!i. free t i \<Longrightarrow> free s i)"
+ by (induct set: beta) auto
-lemma beta_subst [rule_format, intro]:
- "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
- apply (erule beta.induct)
- apply (simp_all add: subst_subst [symmetric])
- done
+lemma beta_subst [intro]: "s -> t ==> (!!u i. s[u/i] -> t[u/i])"
+ by (induct set: beta) (simp_all add: subst_subst [symmetric])
-lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
- apply (induct_tac t)
- apply (auto elim!: linorder_neqE simp: subst_Var)
- done
+lemma subst_Var_Suc [simp]: "t[Var i/i] = t[Var(i)/i + 1]"
+ by (induct t fixing: i) (auto elim!: linorder_neqE simp: subst_Var)
-lemma eta_lift [rule_format, simp]:
- "s -e> t ==> \<forall>i. lift s i -e> lift t i"
- apply (erule eta.induct)
- apply simp_all
- done
+lemma eta_lift [simp]: "s -e> t ==> (!!i. lift s i -e> lift t i)"
+ by (induct set: eta) simp_all
-lemma rtrancl_eta_subst [rule_format]:
- "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
- apply (induct_tac u)
+lemma rtrancl_eta_subst: "s -e> t \<Longrightarrow> u[s/i] -e>> u[t/i]"
+ apply (induct u fixing: s t i)
apply (simp_all add: subst_Var)
- apply (blast)
+ apply blast
apply (blast intro: rtrancl_eta_App)
apply (blast intro!: rtrancl_eta_Abs eta_lift)
done
@@ -191,11 +165,10 @@
text {* @{term "Abs (lift s 0 \<degree> Var 0) -e> s"} *}
-lemma not_free_iff_lifted [rule_format]:
- "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
- apply (induct_tac s)
+lemma not_free_iff_lifted:
+ "(\<not> free s i) = (\<exists>t. s = lift t i)"
+ apply (induct s fixing: i)
apply simp
- apply clarify
apply (rule iffI)
apply (erule linorder_neqE)
apply (rule_tac x = "Var nat" in exI)
@@ -214,7 +187,6 @@
apply simp
apply (erule thin_rl)
apply (erule thin_rl)
- apply (rule allI)
apply (rule iffI)
apply (elim conjE exE)
apply (rename_tac u1 u2)
@@ -229,7 +201,6 @@
apply simp
apply simp
apply (erule thin_rl)
- apply (rule allI)
apply (rule iffI)
apply (erule exE)
apply (rule_tac x = "Abs t" in exI)
@@ -246,8 +217,7 @@
theorem explicit_is_implicit:
"(\<forall>s u. (\<not> free s 0) --> R (Abs (s \<degree> Var 0)) (s[u/0])) =
(\<forall>s. R (Abs (lift s 0 \<degree> Var 0)) s)"
- apply (auto simp add: not_free_iff_lifted)
- done
+ by (auto simp add: not_free_iff_lifted)
subsection {* Parallel eta-reduction *}
@@ -270,22 +240,23 @@
app [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> s' \<Longrightarrow> t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> s \<degree> t \<Rightarrow>\<^sub>\<eta> s' \<degree> t'"
abs [simp, intro]: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> Abs s \<Rightarrow>\<^sub>\<eta> Abs t"
-lemma free_par_eta [simp]: assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
- shows "\<And>i. free t i = free s i" using eta
- by induct (simp_all cong: conj_cong)
+lemma free_par_eta [simp]:
+ assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
+ shows "free t i = free s i" using eta
+ by (induct fixing: i) (simp_all cong: conj_cong)
lemma par_eta_refl [simp]: "t \<Rightarrow>\<^sub>\<eta> t"
by (induct t) simp_all
lemma par_eta_lift [simp]:
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
- shows "\<And>i. lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
- by induct simp_all
+ shows "lift s i \<Rightarrow>\<^sub>\<eta> lift t i" using eta
+ by (induct fixing: i) simp_all
lemma par_eta_subst [simp]:
assumes eta: "s \<Rightarrow>\<^sub>\<eta> t"
- shows "\<And>u u' i. u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
- by induct (simp_all add: subst_subst [symmetric] subst_Var)
+ shows "u \<Rightarrow>\<^sub>\<eta> u' \<Longrightarrow> s[u/i] \<Rightarrow>\<^sub>\<eta> t[u'/i]" using eta
+ by (induct fixing: u u' i) (simp_all add: subst_subst [symmetric] subst_Var)
theorem eta_subset_par_eta: "eta \<subseteq> par_eta"
apply (rule subsetI)
@@ -320,16 +291,16 @@
eta_expand_Suc: "eta_expand (Suc n) t = Abs (lift (eta_expand n t) 0 \<degree> Var 0)"
lemma eta_expand_Suc':
- "\<And>t. eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
- by (induct n) simp_all
+ "eta_expand (Suc n) t = eta_expand n (Abs (lift t 0 \<degree> Var 0))"
+ by (induct n fixing: t) simp_all
theorem lift_eta_expand: "lift (eta_expand k t) i = eta_expand k (lift t i)"
by (induct k) (simp_all add: lift_lift)
theorem eta_expand_beta:
assumes u: "u => u'"
- shows "\<And>t t'. t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
-proof (induct k)
+ shows "t => t' \<Longrightarrow> eta_expand k (Abs t) \<degree> u => t'[u'/0]"
+proof (induct k fixing: t t')
case 0 with u show ?case by simp
next
case (Suc k)
@@ -343,8 +314,8 @@
shows "eta_expand k t => eta_expand k t'"
by (induct k) (simp_all add: t)
-theorem eta_expand_eta: "\<And>t t'. t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
-proof (induct k)
+theorem eta_expand_eta: "t \<Rightarrow>\<^sub>\<eta> t' \<Longrightarrow> eta_expand k t \<Rightarrow>\<^sub>\<eta> t'"
+proof (induct k fixing: t t')
case 0
show ?case by simp
next
@@ -358,9 +329,9 @@
subsection {* Elimination rules for parallel eta reduction *}
theorem par_eta_elim_app: assumes eta: "t \<Rightarrow>\<^sub>\<eta> u"
- shows "\<And>u1' u2'. u = u1' \<degree> u2' \<Longrightarrow>
+ shows "u = u1' \<degree> u2' \<Longrightarrow>
\<exists>u1 u2 k. t = eta_expand k (u1 \<degree> u2) \<and> u1 \<Rightarrow>\<^sub>\<eta> u1' \<and> u2 \<Rightarrow>\<^sub>\<eta> u2'" using eta
-proof induct
+proof (induct fixing: u1' u2')
case (app s s' t t')
have "s \<degree> t = eta_expand 0 (s \<degree> t)" by simp
with app show ?case by blast
@@ -388,9 +359,9 @@
qed
theorem par_eta_elim_abs: assumes eta: "t \<Rightarrow>\<^sub>\<eta> t'"
- shows "\<And>u'. t' = Abs u' \<Longrightarrow>
+ shows "t' = Abs u' \<Longrightarrow>
\<exists>u k. t = eta_expand k (Abs u) \<and> u \<Rightarrow>\<^sub>\<eta> u'" using eta
-proof induct
+proof (induct fixing: u')
case (abs s t)
have "Abs s = eta_expand 0 (Abs s)" by simp
with abs show ?case by blast
@@ -420,8 +391,9 @@
Based on a proof by Masako Takahashi \cite{Takahashi-IandC}.
*}
-theorem par_eta_beta: "\<And>s u. s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
-proof (induct t rule: measure_induct [of size, rule_format])
+theorem par_eta_beta: "s \<Rightarrow>\<^sub>\<eta> t \<Longrightarrow> t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' \<Rightarrow>\<^sub>\<eta> u"
+proof (induct t fixing: s u
+ rule: measure_induct [of size, rule_format])
case (1 t)
from 1(3)
show ?case
@@ -467,10 +439,10 @@
qed
theorem eta_postponement': assumes eta: "s -e>> t"
- shows "\<And>u. t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
+ shows "t => u \<Longrightarrow> \<exists>t'. s => t' \<and> t' -e>> u"
using eta [simplified rtrancl_subset
[OF eta_subset_par_eta par_eta_subset_eta, symmetric]]
-proof induct
+proof (induct fixing: u)
case 1
thus ?case by blast
next
--- a/src/HOL/Lambda/InductTermi.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/InductTermi.thy Wed Nov 23 22:26:13 2005 +0100
@@ -45,7 +45,7 @@
done
lemma IT_implies_termi: "t : IT ==> t : termi beta"
- apply (erule IT.induct)
+ apply (induct set: IT)
apply (drule rev_subsetD)
apply (rule lists_mono)
apply (rule Int_lower2)
@@ -63,16 +63,14 @@
subsection {* Every terminating term is in IT *}
-declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
+declare Var_apps_neq_Abs_apps [symmetric, simp]
lemma [simp, THEN not_sym, simp]: "Var n \<degree>\<degree> ss \<noteq> Abs r \<degree> s \<degree>\<degree> ts"
- apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
- done
+ by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
lemma [simp]:
"(Abs r \<degree> s \<degree>\<degree> ss = Abs r' \<degree> s' \<degree>\<degree> ss') = (r = r' \<and> s = s' \<and> ss = ss')"
- apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
- done
+ by (simp add: foldl_Cons [symmetric] del: foldl_Cons)
inductive_cases [elim!]:
"Var n \<degree>\<degree> ss : IT"
--- a/src/HOL/Lambda/Lambda.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Lambda.thy Wed Nov 23 22:26:13 2005 +0100
@@ -86,21 +86,15 @@
lemma rtrancl_beta_Abs [intro!]:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> Abs s \<rightarrow>\<^sub>\<beta>\<^sup>* Abs s'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppL:
"s \<rightarrow>\<^sub>\<beta>\<^sup>* s' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_AppR:
"t \<rightarrow>\<^sub>\<beta>\<^sup>* t' ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s \<degree> t'"
- apply (erule rtrancl_induct)
- apply (blast intro: rtrancl_into_rtrancl)+
- done
+ by (induct set: rtrancl) (blast intro: rtrancl_into_rtrancl)+
lemma rtrancl_beta_App [intro]:
"[| s \<rightarrow>\<^sub>\<beta>\<^sup>* s'; t \<rightarrow>\<^sub>\<beta>\<^sup>* t' |] ==> s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'"
@@ -112,72 +106,51 @@
subsection {* Substitution-lemmas *}
lemma subst_eq [simp]: "(Var k)[u/k] = u"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
- apply (simp add: subst_Var)
- done
+ by (simp add: subst_Var)
-lemma lift_lift [rule_format]:
- "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
- apply (induct_tac t)
- apply auto
- done
+lemma lift_lift:
+ "i < k + 1 \<Longrightarrow> lift (lift t i) (Suc k) = lift (lift t k) i"
+ by (induct t fixing: i k) auto
lemma lift_subst [simp]:
- "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
- apply (induct_tac t)
- apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
- done
+ "j < i + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
+ by (induct t fixing: i j s)
+ (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
lemma lift_subst_lt:
- "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
- apply (induct_tac t)
- apply (simp_all add: subst_Var lift_lift)
- done
+ "i < j + 1 \<Longrightarrow> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
+ by (induct t fixing: i j s) (simp_all add: subst_Var lift_lift)
lemma subst_lift [simp]:
- "\<forall>k s. (lift t k)[s/k] = t"
- apply (induct_tac t)
- apply simp_all
- done
+ "(lift t k)[s/k] = t"
+ by (induct t fixing: k s) simp_all
-lemma subst_subst [rule_format]:
- "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
- apply (induct_tac t)
- apply (simp_all
- add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
+lemma subst_subst:
+ "i < j + 1 \<Longrightarrow> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
+ by (induct t fixing: i j u v)
+ (simp_all add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
split: nat.split)
- done
subsection {* Equivalence proof for optimized substitution *}
-lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma liftn_0 [simp]: "liftn 0 t k = t"
+ by (induct t fixing: k) (simp_all add: subst_Var)
-lemma liftn_lift [simp]:
- "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma liftn_lift [simp]: "liftn (Suc n) t k = lift (liftn n t k) k"
+ by (induct t fixing: k) (simp_all add: subst_Var)
-lemma substn_subst_n [simp]:
- "\<forall>n. substn t s n = t[liftn n s 0 / n]"
- apply (induct_tac t)
- apply (simp_all add: subst_Var)
- done
+lemma substn_subst_n [simp]: "substn t s n = t[liftn n s 0 / n]"
+ by (induct t fixing: n) (simp_all add: subst_Var)
theorem substn_subst_0: "substn t s 0 = t[s/0]"
- apply simp
- done
+ by simp
subsection {* Preservation theorems *}
@@ -187,13 +160,11 @@
theorem subst_preserves_beta [simp]:
"r \<rightarrow>\<^sub>\<beta> s ==> (\<And>t i. r[t/i] \<rightarrow>\<^sub>\<beta> s[t/i])"
- apply (induct set: beta)
- apply (simp_all add: subst_subst [symmetric])
- done
+ by (induct set: beta) (simp_all add: subst_subst [symmetric])
theorem subst_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> r[t/i] \<rightarrow>\<^sub>\<beta>\<^sup>* s[t/i]"
- apply (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_into_rtrancl)
apply (erule subst_preserves_beta)
done
@@ -203,23 +174,22 @@
by (induct set: beta) auto
theorem lift_preserves_beta': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> lift r i \<rightarrow>\<^sub>\<beta>\<^sup>* lift s i"
- apply (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_into_rtrancl)
apply (erule lift_preserves_beta)
done
-theorem subst_preserves_beta2 [simp]:
- "\<And>r s i. r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
- apply (induct t)
+theorem subst_preserves_beta2 [simp]: "r \<rightarrow>\<^sub>\<beta> s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
+ apply (induct t fixing: r s i)
apply (simp add: subst_Var r_into_rtrancl)
apply (simp add: rtrancl_beta_App)
apply (simp add: rtrancl_beta_Abs)
done
theorem subst_preserves_beta2': "r \<rightarrow>\<^sub>\<beta>\<^sup>* s ==> t[r/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t[s/i]"
- apply (erule rtrancl.induct)
- apply (rule rtrancl_refl)
+ apply (induct set: rtrancl)
+ apply (rule rtrancl_refl)
apply (erule rtrancl_trans)
apply (erule subst_preserves_beta2)
done
--- a/src/HOL/Lambda/ListApplication.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListApplication.thy Wed Nov 23 22:26:13 2005 +0100
@@ -14,19 +14,14 @@
"t \<degree>\<degree> ts" == "foldl (op \<degree>) t ts"
lemma apps_eq_tail_conv [iff]: "(r \<degree>\<degree> ts = s \<degree>\<degree> ts) = (r = s)"
- apply (induct_tac ts rule: rev_induct)
- apply auto
- done
+ by (induct ts rule: rev_induct) auto
-lemma Var_eq_apps_conv [iff]:
- "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
- apply (induct ss)
- apply auto
- done
+lemma Var_eq_apps_conv [iff]: "(Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
+ by (induct ss fixing: s) auto
lemma Var_apps_eq_Var_apps_conv [iff]:
- "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
- apply (induct rs rule: rev_induct)
+ "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
+ apply (induct rs fixing: ss rule: rev_induct)
apply simp
apply blast
apply (induct_tac ss rule: rev_induct)
@@ -43,18 +38,14 @@
lemma Abs_eq_apps_conv [iff]:
"(Abs r = s \<degree>\<degree> ss) = (Abs r = s \<and> ss = [])"
- apply (induct_tac ss rule: rev_induct)
- apply auto
- done
+ by (induct ss rule: rev_induct) auto
lemma apps_eq_Abs_conv [iff]: "(s \<degree>\<degree> ss = Abs r) = (s = Abs r \<and> ss = [])"
- apply (induct_tac ss rule: rev_induct)
- apply auto
- done
+ by (induct ss rule: rev_induct) auto
lemma Abs_apps_eq_Abs_apps_conv [iff]:
- "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
- apply (induct rs rule: rev_induct)
+ "(Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
+ apply (induct rs fixing: ss rule: rev_induct)
apply simp
apply blast
apply (induct_tac ss rule: rev_induct)
@@ -62,14 +53,12 @@
done
lemma Abs_App_neq_Var_apps [iff]:
- "\<forall>s t. Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
- apply (induct_tac ss rule: rev_induct)
- apply auto
- done
+ "Abs s \<degree> t ~= Var n \<degree>\<degree> ss"
+ by (induct ss fixing: s t rule: rev_induct) auto
lemma Var_apps_neq_Abs_apps [iff]:
- "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
- apply (induct ss rule: rev_induct)
+ "Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
+ apply (induct ss fixing: ts rule: rev_induct)
apply simp
apply (induct_tac ts rule: rev_induct)
apply auto
@@ -77,7 +66,7 @@
lemma ex_head_tail:
"\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
- apply (induct_tac t)
+ apply (induct t)
apply (rule_tac x = "[]" in exI)
apply simp
apply clarify
@@ -89,21 +78,18 @@
lemma size_apps [simp]:
"size (r \<degree>\<degree> rs) = size r + foldl (op +) 0 (map size rs) + length rs"
- apply (induct_tac rs rule: rev_induct)
- apply auto
- done
+ by (induct rs rule: rev_induct) auto
lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
- apply simp
- done
+ by simp
lemma lift_map [simp]:
- "\<And>t. lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
- by (induct ts) simp_all
+ "lift (t \<degree>\<degree> ts) i = lift t i \<degree>\<degree> map (\<lambda>t. lift t i) ts"
+ by (induct ts fixing: t) simp_all
lemma subst_map [simp]:
- "\<And>t. subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
- by (induct ts) simp_all
+ "subst (t \<degree>\<degree> ts) u i = subst t u i \<degree>\<degree> map (\<lambda>t. subst t u i) ts"
+ by (induct ts fixing: t) simp_all
lemma app_last: "(t \<degree>\<degree> ts) \<degree> u = t \<degree>\<degree> (ts @ [u])"
by simp
@@ -111,60 +97,51 @@
text {* \medskip A customized induction schema for @{text "\<degree>\<degree>"}. *}
-lemma lem [rule_format (no_asm)]:
- "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
- |] ==> \<forall>t. size t = n --> P t"
-proof -
- case rule_context
- show ?thesis
- apply (induct_tac n rule: nat_less_induct)
- apply (rule allI)
- apply (cut_tac t = t in ex_head_tail)
+lemma lem:
+ assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
+ and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
+ shows "size t = n \<Longrightarrow> P t"
+ apply (induct n fixing: t rule: nat_less_induct)
+ apply (cut_tac t = t in ex_head_tail)
+ apply clarify
+ apply (erule disjE)
+ apply clarify
+ apply (rule prems)
apply clarify
- apply (erule disjE)
- apply clarify
- apply (rule prems)
- apply clarify
- apply (erule allE, erule impE)
- prefer 2
- apply (erule allE, erule mp, rule refl)
- apply simp
- apply (rule lem0)
- apply force
- apply (rule elem_le_sum)
- apply force
- apply clarify
- apply (rule prems)
- apply (erule allE, erule impE)
- prefer 2
- apply (erule allE, erule mp, rule refl)
- apply simp
- apply clarify
- apply (erule allE, erule impE)
- prefer 2
- apply (erule allE, erule mp, rule refl)
- apply simp
- apply (rule le_imp_less_Suc)
- apply (rule trans_le_add1)
- apply (rule trans_le_add2)
- apply (rule elem_le_sum)
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply (rule lem0)
apply force
- done
-qed
+ apply (rule elem_le_sum)
+ apply force
+ apply clarify
+ apply (rule prems)
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply clarify
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply (rule le_imp_less_Suc)
+ apply (rule trans_le_add1)
+ apply (rule trans_le_add2)
+ apply (rule elem_le_sum)
+ apply force
+ done
theorem Apps_dB_induct:
- "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)
- |] ==> P t"
-proof -
- case rule_context
- show ?thesis
- apply (rule_tac t = t in lem)
- prefer 3
- apply (rule refl)
- apply (assumption | rule prems)+
- done
-qed
+ assumes "!!n ts. \<forall>t \<in> set ts. P t ==> P (Var n \<degree>\<degree> ts)"
+ and "!!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u \<degree>\<degree> ts)"
+ shows "P t"
+ apply (rule_tac t = t in lem)
+ prefer 3
+ apply (rule refl)
+ apply (assumption | rule prems)+
+ done
end
--- a/src/HOL/Lambda/ListBeta.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListBeta.thy Wed Nov 23 22:26:13 2005 +0100
@@ -18,8 +18,8 @@
"rs => ss" == "(rs, ss) : step1 beta"
lemma head_Var_reduction_aux:
- "v -> v' ==> \<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss)"
- apply (erule beta.induct)
+ "v -> v' ==> (\<forall>rs. v = Var n \<degree>\<degree> rs --> (\<exists>ss. rs => ss \<and> v' = Var n \<degree>\<degree> ss))"
+ apply (induct set: beta)
apply simp
apply (rule allI)
apply (rule_tac xs = rs in rev_exhaust)
@@ -33,16 +33,14 @@
lemma head_Var_reduction:
"Var n \<degree>\<degree> rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n \<degree>\<degree> ss)"
- apply (drule head_Var_reduction_aux)
- apply blast
- done
+ by (drule head_Var_reduction_aux) blast
lemma apps_betasE_aux:
"u -> u' ==> \<forall>r rs. u = r \<degree>\<degree> rs -->
((\<exists>r'. r -> r' \<and> u' = r' \<degree>\<degree> rs) \<or>
(\<exists>rs'. rs => rs' \<and> u' = r \<degree>\<degree> rs') \<or>
(\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] \<degree>\<degree> ts))"
- apply (erule beta.induct)
+ apply (induct set: beta)
apply (clarify del: disjCI)
apply (case_tac r)
apply simp
@@ -70,38 +68,31 @@
done
lemma apps_betasE [elim!]:
- "[| r \<degree>\<degree> rs -> s; !!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R;
- !!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R;
- !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R |]
- ==> R"
-proof -
- assume major: "r \<degree>\<degree> rs -> s"
- case rule_context
- show ?thesis
- apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
- apply (assumption | rule refl | erule prems exE conjE impE disjE)+
- done
-qed
+ assumes major: "r \<degree>\<degree> rs -> s"
+ and "!!r'. [| r -> r'; s = r' \<degree>\<degree> rs |] ==> R"
+ and "!!rs'. [| rs => rs'; s = r \<degree>\<degree> rs' |] ==> R"
+ and "!!t u us. [| r = Abs t; rs = u # us; s = t[u/0] \<degree>\<degree> us |] ==> R"
+ shows R
+ apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
+ apply (assumption | rule refl | erule prems exE conjE impE disjE)+
+ done
lemma apps_preserves_beta [simp]:
"r -> s ==> r \<degree>\<degree> ss -> s \<degree>\<degree> ss"
- apply (induct_tac ss rule: rev_induct)
- apply auto
- done
+ by (induct ss rule: rev_induct) auto
lemma apps_preserves_beta2 [simp]:
"r ->> s ==> r \<degree>\<degree> ss ->> s \<degree>\<degree> ss"
- apply (erule rtrancl_induct)
+ apply (induct set: rtrancl)
apply blast
apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
done
-lemma apps_preserves_betas [rule_format, simp]:
- "\<forall>ss. rs => ss --> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
- apply (induct_tac rs rule: rev_induct)
+lemma apps_preserves_betas [simp]:
+ "rs => ss \<Longrightarrow> r \<degree>\<degree> rs -> r \<degree>\<degree> ss"
+ apply (induct rs fixing: ss rule: rev_induct)
apply simp
apply simp
- apply clarify
apply (rule_tac xs = ss in rev_exhaust)
apply simp
apply simp
--- a/src/HOL/Lambda/ListOrder.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ListOrder.thy Wed Nov 23 22:26:13 2005 +0100
@@ -87,18 +87,17 @@
apply blast
done
-lemma Cons_acc_step1I [rule_format, intro!]:
- "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
- apply (erule acc_induct)
+lemma Cons_acc_step1I [intro!]:
+ "x \<in> acc r ==> (!!xs. xs \<in> acc (step1 r) \<Longrightarrow> x # xs \<in> acc (step1 r))"
+ apply (induct set: acc)
apply (erule thin_rl)
- apply clarify
apply (erule acc_induct)
apply (rule accI)
apply blast
done
lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
- apply (erule lists.induct)
+ apply (induct set: lists)
apply (rule accI)
apply simp
apply (rule accI)
@@ -114,7 +113,7 @@
done
lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
- apply (erule acc_induct)
+ apply (induct set: acc)
apply clarify
apply (rule accI)
apply (drule ex_step1I, assumption)
--- a/src/HOL/Lambda/ParRed.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/ParRed.thy Wed Nov 23 22:26:13 2005 +0100
@@ -43,13 +43,10 @@
lemma par_beta_varL [simp]:
"(Var n => t) = (t = Var n)"
- apply blast
- done
+ by blast
lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *)
- apply (induct_tac t)
- apply simp_all
- done
+ by (induct t) simp_all
lemma beta_subset_par_beta: "beta <= par_beta"
apply (rule subsetI)
@@ -70,17 +67,14 @@
subsection {* Misc properties of par-beta *}
-lemma par_beta_lift [rule_format, simp]:
- "\<forall>t' n. t => t' --> lift t n => lift t' n"
- apply (induct_tac t)
- apply fastsimp+
- done
+lemma par_beta_lift [simp]:
+ "t => t' \<Longrightarrow> lift t n => lift t' n"
+ by (induct t fixing: t' n) fastsimp+
-lemma par_beta_subst [rule_format]:
- "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
- apply (induct_tac t)
+lemma par_beta_subst:
+ "s => s' \<Longrightarrow> t => t' \<Longrightarrow> t[s/n] => t'[s'/n]"
+ apply (induct t fixing: s s' t' n)
apply (simp add: subst_Var)
- apply (intro strip)
apply (erule par_beta_cases)
apply simp
apply (simp add: subst_subst [symmetric])
@@ -110,9 +104,8 @@
"cd (Abs u \<degree> t) = (cd u)[cd t/0]"
"cd (Abs s) = Abs (cd s)"
-lemma par_beta_cd [rule_format]:
- "\<forall>t. s => t --> t => cd s"
- apply (induct_tac s rule: cd.induct)
+lemma par_beta_cd: "s => t \<Longrightarrow> t => cd s"
+ apply (induct s fixing: t rule: cd.induct)
apply auto
apply (fast intro!: par_beta_subst)
done
--- a/src/HOL/Lambda/Type.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/Type.thy Wed Nov 23 22:26:13 2005 +0100
@@ -94,8 +94,8 @@
subsection {* Lists of types *}
lemma lists_typings:
- "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
- apply (induct ts)
+ "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
+ apply (induct ts fixing: Ts)
apply (case_tac Ts)
apply simp
apply (rule lists.Nil)
@@ -108,16 +108,16 @@
apply blast
done
-lemma types_snoc: "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
- apply (induct ts)
+lemma types_snoc: "e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t : T \<Longrightarrow> e \<tturnstile> ts @ [t] : Ts @ [T]"
+ apply (induct ts fixing: Ts)
apply simp
apply (case_tac Ts)
apply simp+
done
-lemma types_snoc_eq: "\<And>Ts. e \<tturnstile> ts @ [t] : Ts @ [T] =
+lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
(e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
- apply (induct ts)
+ apply (induct ts fixing: Ts)
apply (case_tac Ts)
apply simp+
apply (case_tac Ts)
@@ -156,8 +156,8 @@
subsection {* n-ary function types *}
lemma list_app_typeD:
- "\<And>t T. e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
- apply (induct ts)
+ "e \<turnstile> t \<degree>\<degree> ts : T \<Longrightarrow> \<exists>Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<and> e \<tturnstile> ts : Ts"
+ apply (induct ts fixing: t T)
apply simp
apply atomize
apply simp
@@ -176,8 +176,8 @@
by (insert list_app_typeD) fast
lemma list_app_typeI:
- "\<And>t T Ts. e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
- apply (induct ts)
+ "e \<turnstile> t : Ts \<Rrightarrow> T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow> e \<turnstile> t \<degree>\<degree> ts : T"
+ apply (induct ts fixing: t T Ts)
apply simp
apply atomize
apply (case_tac Ts)
@@ -201,8 +201,8 @@
*}
theorem var_app_type_eq:
- "\<And>T U. e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
- apply (induct ts rule: rev_induct)
+ "e \<turnstile> Var i \<degree>\<degree> ts : T \<Longrightarrow> e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> T = U"
+ apply (induct ts fixing: T U rule: rev_induct)
apply simp
apply (ind_cases "e \<turnstile> Var i : T")
apply (ind_cases "e \<turnstile> Var i : T")
@@ -220,9 +220,9 @@
apply simp
done
-lemma var_app_types: "\<And>ts Ts U. e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
+lemma var_app_types: "e \<turnstile> Var i \<degree>\<degree> ts \<degree>\<degree> us : T \<Longrightarrow> e \<tturnstile> ts : Ts \<Longrightarrow>
e \<turnstile> Var i \<degree>\<degree> ts : U \<Longrightarrow> \<exists>Us. U = Us \<Rrightarrow> T \<and> e \<tturnstile> us : Us"
- apply (induct us)
+ apply (induct us fixing: ts Ts U)
apply simp
apply (erule var_app_type_eq)
apply assumption
@@ -292,8 +292,8 @@
by (induct set: typing) auto
lemma lift_types:
- "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
- apply (induct ts)
+ "e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
+ apply (induct ts fixing: Ts)
apply simp
apply (case_tac Ts)
apply auto
@@ -311,9 +311,9 @@
done
lemma substs_lemma:
- "\<And>Ts. e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
+ "e \<turnstile> u : T \<Longrightarrow> e\<langle>i:T\<rangle> \<tturnstile> ts : Ts \<Longrightarrow>
e \<tturnstile> (map (\<lambda>t. t[u/i]) ts) : Ts"
- apply (induct ts)
+ apply (induct ts fixing: Ts)
apply (case_tac Ts)
apply simp
apply simp
@@ -352,18 +352,16 @@
subsection {* Alternative induction rule for types *}
lemma type_induct [induct type]:
+ assumes
"(\<And>T. (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T1) \<Longrightarrow>
- (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T) \<Longrightarrow> P T"
-proof -
- case rule_context
- show ?thesis
- proof (induct T)
- case Atom
- show ?case by (rule rule_context) simp_all
- next
- case Fun
- show ?case by (rule rule_context) (insert Fun, simp_all)
- qed
+ (\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> P T2) \<Longrightarrow> P T)"
+ shows "P T"
+proof (induct T)
+ case Atom
+ show ?case by (rule prems) simp_all
+next
+ case Fun
+ show ?case by (rule prems) (insert Fun, simp_all)
qed
end
--- a/src/HOL/Lambda/WeakNorm.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy Wed Nov 23 22:26:13 2005 +0100
@@ -52,14 +52,14 @@
done
lemma listall_conj1: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall P xs"
- by (induct xs) simp+
+ by (induct xs) simp_all
lemma listall_conj2: "listall (\<lambda>x. P x \<and> Q x) xs \<Longrightarrow> listall Q xs"
- by (induct xs) simp+
+ by (induct xs) simp_all
lemma listall_app: "listall P (xs @ ys) = (listall P xs \<and> listall P ys)"
apply (induct xs)
- apply (rule iffI, simp, simp)
+ apply (rule iffI, simp, simp)
apply (rule iffI, simp, simp)
done
--- a/src/HOL/Library/Accessible_Part.thy Wed Nov 23 22:23:52 2005 +0100
+++ b/src/HOL/Library/Accessible_Part.thy Wed Nov 23 22:26:13 2005 +0100
@@ -32,19 +32,15 @@
subsection {* Induction rules *}
theorem acc_induct:
- "a \<in> acc r ==>
- (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a"
-proof -
- assume major: "a \<in> acc r"
- assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
- show ?thesis
- apply (rule major [THEN acc.induct])
- apply (rule hyp)
- apply (rule accI)
- apply fast
- apply fast
- done
-qed
+ assumes major: "a \<in> acc r"
+ assumes hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x"
+ shows "P a"
+ apply (rule major [THEN acc.induct])
+ apply (rule hyp)
+ apply (rule accI)
+ apply fast
+ apply fast
+ done
theorems acc_induct_rule = acc_induct [rule_format, induct set: acc]