--- a/src/HOL/Induct/ABexp.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/ABexp.thy Tue Nov 13 22:18:03 2001 +0100
@@ -55,20 +55,17 @@
"substb f (And b1 b2) = And (substb f b1) (substb f b2)"
"substb f (Neg b) = Neg (substb f b)"
-lemma subst1_aexp_bexp:
- "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
- evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
+lemma subst1_aexp:
+ "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
+and subst1_bexp:
+ "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
-- {* one variable *}
- apply (induct a and b)
- apply simp_all
- done
+ by (induct a and b) simp_all
-lemma subst_all_aexp_bexp:
- "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
- evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
- -- {* all variables *}
- apply (induct a and b)
- apply auto
- done
+lemma subst_all_aexp:
+ "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
+and subst_all_bexp:
+ "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
+ by (induct a and b) auto
end
--- a/src/HOL/Induct/Mutil.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Mutil.thy Tue Nov 13 22:18:03 2001 +0100
@@ -101,7 +101,7 @@
text {* \medskip Tilings of dominoes *}
lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
- apply (erule tiling.induct)
+ apply (induct set: tiling)
apply auto
done
@@ -111,7 +111,7 @@
lemma tiling_domino_0_1:
"t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured (Suc 0) \<inter> t)"
- apply (erule tiling.induct)
+ apply (induct set: tiling)
apply (drule_tac [2] domino_singletons)
apply auto
apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
--- a/src/HOL/Induct/Term.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Term.thy Tue Nov 13 22:18:03 2001 +0100
@@ -32,31 +32,25 @@
text {* \medskip A simple theorem about composition of substitutions *}
lemma subst_comp:
- "(subst_term ((subst_term f1) \<circ> f2) t) =
- (subst_term f1 (subst_term f2 t)) \<and>
- (subst_term_list ((subst_term f1) \<circ> f2) ts) =
- (subst_term_list f1 (subst_term_list f2 ts))"
- apply (induct t and ts)
- apply simp_all
- done
+ "subst_term (subst_term f1 \<circ> f2) t =
+ subst_term f1 (subst_term f2 t)"
+and "subst_term_list (subst_term f1 \<circ> f2) ts =
+ subst_term_list f1 (subst_term_list f2 ts)"
+ by (induct t and ts) simp_all
text {* \medskip Alternative induction rule *}
-lemma term_induct2:
- "(!!v. P (Var v)) ==>
- (!!f ts. list_all P ts ==> P (App f ts))
- ==> P t"
-proof -
- case rule_context
- have "P t \<and> list_all P ts"
- apply (induct t and ts)
- apply (rule rule_context)
- apply (rule rule_context)
- apply assumption
- apply simp_all
- done
- thus ?thesis ..
-qed
+lemma
+ (assumes var: "!!v. P (Var v)"
+ and app: "!!f ts. list_all P ts ==> P (App f ts)")
+ term_induct2: "P t"
+and "list_all P ts"
+ apply (induct t and ts)
+ apply (rule var)
+ apply (rule app)
+ apply assumption
+ apply simp_all
+ done
end
--- a/src/HOL/Induct/Tree.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Induct/Tree.thy Tue Nov 13 22:18:03 2001 +0100
@@ -19,9 +19,7 @@
"map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
- apply (induct t)
- apply simp_all
- done
+ by (induct t) simp_all
consts
exists_tree :: "('a => bool) => 'a tree => bool"
@@ -32,9 +30,6 @@
lemma exists_map:
"(!!x. P x ==> Q (f x)) ==>
exists_tree P ts ==> exists_tree Q (map_tree f ts)"
- apply (induct ts)
- apply simp_all
- apply blast
- done
+ by (induct ts) auto
end
--- a/src/HOL/Lambda/Type.thy Tue Nov 13 17:51:03 2001 +0100
+++ b/src/HOL/Lambda/Type.thy Tue Nov 13 22:18:03 2001 +0100
@@ -182,12 +182,9 @@
lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
by (induct ts) auto
-lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
-proof -
- assume "e \<turnstile> t : T"
- thus "\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
- by induct auto
-qed
+lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)"
+ by (induct set: typing) auto
+
lemma lift_typings:
"\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
@@ -473,6 +470,7 @@
qed
qed
+
subsection {* Well-typed terms are strongly normalizing *}
lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"