tuned inductions;
authorwenzelm
Tue Nov 13 22:18:03 2001 +0100 (2001-11-13)
changeset 12171dc87f33db447
parent 12170 1433a9cdb55c
child 12172 5e81c9d539f8
tuned inductions;
src/HOL/Induct/ABexp.thy
src/HOL/Induct/Mutil.thy
src/HOL/Induct/Term.thy
src/HOL/Induct/Tree.thy
src/HOL/Lambda/Type.thy
     1.1 --- a/src/HOL/Induct/ABexp.thy	Tue Nov 13 17:51:03 2001 +0100
     1.2 +++ b/src/HOL/Induct/ABexp.thy	Tue Nov 13 22:18:03 2001 +0100
     1.3 @@ -55,20 +55,17 @@
     1.4    "substb f (And b1 b2) = And (substb f b1) (substb f b2)"
     1.5    "substb f (Neg b) = Neg (substb f b)"
     1.6  
     1.7 -lemma subst1_aexp_bexp:
     1.8 -  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a \<and>
     1.9 -  evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
    1.10 +lemma subst1_aexp:
    1.11 +  "evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
    1.12 +and subst1_bexp:
    1.13 +  "evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
    1.14      --  {* one variable *}
    1.15 -  apply (induct a and b)
    1.16 -         apply simp_all
    1.17 -  done
    1.18 +  by (induct a and b) simp_all
    1.19  
    1.20 -lemma subst_all_aexp_bexp:
    1.21 -  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a \<and>
    1.22 -  evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
    1.23 -    -- {* all variables *}
    1.24 -  apply (induct a and b)
    1.25 -         apply auto
    1.26 -  done
    1.27 +lemma subst_all_aexp:
    1.28 +  "evala env (substa s a) = evala (\<lambda>x. evala env (s x)) a"
    1.29 +and subst_all_bexp:
    1.30 +  "evalb env (substb s b) = evalb (\<lambda>x. evala env (s x)) b"
    1.31 +  by (induct a and b) auto
    1.32  
    1.33  end
     2.1 --- a/src/HOL/Induct/Mutil.thy	Tue Nov 13 17:51:03 2001 +0100
     2.2 +++ b/src/HOL/Induct/Mutil.thy	Tue Nov 13 22:18:03 2001 +0100
     2.3 @@ -101,7 +101,7 @@
     2.4  text {* \medskip Tilings of dominoes *}
     2.5  
     2.6  lemma tiling_domino_finite [simp]: "t \<in> tiling domino ==> finite t"
     2.7 -  apply (erule tiling.induct)
     2.8 +  apply (induct set: tiling)
     2.9     apply auto
    2.10    done
    2.11  
    2.12 @@ -111,7 +111,7 @@
    2.13  
    2.14  lemma tiling_domino_0_1:
    2.15    "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured (Suc 0) \<inter> t)"
    2.16 -  apply (erule tiling.induct)
    2.17 +  apply (induct set: tiling)
    2.18     apply (drule_tac [2] domino_singletons)
    2.19     apply auto
    2.20    apply (subgoal_tac "\<forall>p C. C \<inter> a = {p} --> p \<notin> t")
     3.1 --- a/src/HOL/Induct/Term.thy	Tue Nov 13 17:51:03 2001 +0100
     3.2 +++ b/src/HOL/Induct/Term.thy	Tue Nov 13 22:18:03 2001 +0100
     3.3 @@ -32,31 +32,25 @@
     3.4  text {* \medskip A simple theorem about composition of substitutions *}
     3.5  
     3.6  lemma subst_comp:
     3.7 -  "(subst_term ((subst_term f1) \<circ> f2) t) =
     3.8 -    (subst_term f1 (subst_term f2 t)) \<and>
     3.9 -  (subst_term_list ((subst_term f1) \<circ> f2) ts) =
    3.10 -    (subst_term_list f1 (subst_term_list f2 ts))"
    3.11 -  apply (induct t and ts)
    3.12 -     apply simp_all
    3.13 -  done
    3.14 +  "subst_term (subst_term f1 \<circ> f2) t =
    3.15 +    subst_term f1 (subst_term f2 t)"
    3.16 +and "subst_term_list (subst_term f1 \<circ> f2) ts =
    3.17 +    subst_term_list f1 (subst_term_list f2 ts)"
    3.18 +  by (induct t and ts) simp_all
    3.19  
    3.20  
    3.21  text {* \medskip Alternative induction rule *}
    3.22  
    3.23 -lemma term_induct2:
    3.24 -  "(!!v. P (Var v)) ==>
    3.25 -    (!!f ts. list_all P ts ==> P (App f ts))
    3.26 -  ==> P t"
    3.27 -proof -
    3.28 -  case rule_context
    3.29 -  have "P t \<and> list_all P ts"
    3.30 -    apply (induct t and ts)
    3.31 -       apply (rule rule_context)
    3.32 -      apply (rule rule_context)
    3.33 -      apply assumption
    3.34 -     apply simp_all
    3.35 -    done
    3.36 -  thus ?thesis ..
    3.37 -qed
    3.38 +lemma
    3.39 +  (assumes var: "!!v. P (Var v)"
    3.40 +    and app: "!!f ts. list_all P ts ==> P (App f ts)")
    3.41 +  term_induct2: "P t"
    3.42 +and "list_all P ts"
    3.43 +  apply (induct t and ts)
    3.44 +     apply (rule var)
    3.45 +    apply (rule app)
    3.46 +    apply assumption
    3.47 +   apply simp_all
    3.48 +  done
    3.49  
    3.50  end
     4.1 --- a/src/HOL/Induct/Tree.thy	Tue Nov 13 17:51:03 2001 +0100
     4.2 +++ b/src/HOL/Induct/Tree.thy	Tue Nov 13 22:18:03 2001 +0100
     4.3 @@ -19,9 +19,7 @@
     4.4    "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
     4.5  
     4.6  lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
     4.7 -  apply (induct t)
     4.8 -   apply simp_all
     4.9 -  done
    4.10 +  by (induct t) simp_all
    4.11  
    4.12  consts
    4.13    exists_tree :: "('a => bool) => 'a tree => bool"
    4.14 @@ -32,9 +30,6 @@
    4.15  lemma exists_map:
    4.16    "(!!x. P x ==> Q (f x)) ==>
    4.17      exists_tree P ts ==> exists_tree Q (map_tree f ts)"
    4.18 -  apply (induct ts)
    4.19 -   apply simp_all
    4.20 -  apply blast
    4.21 -  done
    4.22 +  by (induct ts) auto
    4.23  
    4.24  end
     5.1 --- a/src/HOL/Lambda/Type.thy	Tue Nov 13 17:51:03 2001 +0100
     5.2 +++ b/src/HOL/Lambda/Type.thy	Tue Nov 13 22:18:03 2001 +0100
     5.3 @@ -182,12 +182,9 @@
     5.4  lemma lifts_IT: "ts \<in> lists IT \<Longrightarrow> map (\<lambda>t. lift t 0) ts \<in> lists IT"
     5.5    by (induct ts) auto
     5.6  
     5.7 -lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
     5.8 -proof -
     5.9 -  assume "e \<turnstile> t : T"
    5.10 -  thus "\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
    5.11 -    by induct auto
    5.12 -qed
    5.13 +lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> (\<And>i U. e\<langle>i:U\<rangle> \<turnstile> lift t i : T)"
    5.14 +  by (induct set: typing) auto
    5.15 +
    5.16  
    5.17  lemma lift_typings:
    5.18    "\<And>Ts. e \<tturnstile> ts : Ts \<Longrightarrow> e\<langle>i:U\<rangle> \<tturnstile> (map (\<lambda>t. lift t i) ts) : Ts"
    5.19 @@ -473,6 +470,7 @@
    5.20    qed
    5.21  qed
    5.22  
    5.23 +
    5.24  subsection {* Well-typed terms are strongly normalizing *}
    5.25  
    5.26  lemma type_implies_IT: "e \<turnstile> t : T \<Longrightarrow> t \<in> IT"