src/HOL/Lambda/Type.thy

 
 subsection {* Lists of types *}
 
 lemma lists_typings:
     "e \<tturnstile> ts : Ts \<Longrightarrow> ts \<in> lists {t. \<exists>T. e \<turnstile> t : T}"
-  apply (induct ts fixing: Ts)
+  apply (induct ts arbitrary: Ts)
    apply (case_tac Ts)
      apply simp
      apply (rule lists.Nil)
     apply simp
   apply (case_tac Ts)

    apply blast
   apply blast
   done
 
 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 (induct ts arbitrary: Ts)
   apply simp
   apply (case_tac Ts)
   apply simp+
   done
 
 lemma types_snoc_eq: "e \<tturnstile> ts @ [t] : Ts @ [T] =
   (e \<tturnstile> ts : Ts \<and> e \<turnstile> t : T)"
-  apply (induct ts fixing: Ts)
+  apply (induct ts arbitrary: Ts)
   apply (case_tac Ts)
   apply simp+
   apply (case_tac Ts)
   apply (case_tac "ts @ [t]")
   apply simp+

 
 subsection {* n-ary function types *}
 
 lemma list_app_typeD:
     "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 (induct ts arbitrary: t T)
    apply simp
   apply atomize
   apply simp
   apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)

   "e \<turnstile> t \<degree>\<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:
     "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 (induct ts arbitrary: t T Ts)
    apply simp
   apply atomize
   apply (case_tac Ts)
    apply simp
   apply simp

 for program extraction.
 *}
 
 theorem var_app_type_eq:
   "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 (induct ts arbitrary: T U rule: rev_induct)
   apply simp
   apply (ind_cases "e \<turnstile> Var i : T")
   apply (ind_cases "e \<turnstile> Var i : T")
   apply simp
   apply simp

   apply simp
   done
 
 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 fixing: ts Ts U)
+  apply (induct us arbitrary: ts Ts U)
   apply simp
   apply (erule var_app_type_eq)
   apply assumption
   apply simp
   apply atomize

 
 
 subsection {* Lifting preserves well-typedness *}
 
 lemma lift_type [intro!]: "e \<turnstile> t : T \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> lift t i : T"
-  by (induct fixing: i U set: typing) auto
+  by (induct arbitrary: i U set: typing) auto
 
 lemma lift_types:
   "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 (induct ts arbitrary: Ts)
    apply simp
   apply (case_tac Ts)
    apply auto
   done
 
 
 subsection {* Substitution lemmas *}
 
 lemma subst_lemma:
     "e \<turnstile> t : T \<Longrightarrow> e' \<turnstile> u : U \<Longrightarrow> e = e'\<langle>i:U\<rangle> \<Longrightarrow> e' \<turnstile> t[u/i] : T"
-  apply (induct fixing: e' i U u set: typing)
+  apply (induct arbitrary: e' i U u set: typing)
     apply (rule_tac x = x and y = i in linorder_cases)
       apply auto
   apply blast
   done
 
 lemma substs_lemma:
   "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 fixing: Ts)
+  apply (induct ts arbitrary: Ts)
    apply (case_tac Ts)
     apply simp
    apply simp
   apply atomize
   apply (case_tac Ts)

 
 
 subsection {* Subject reduction *}
 
 lemma subject_reduction: "e \<turnstile> t : T \<Longrightarrow> t -> t' \<Longrightarrow> e \<turnstile> t' : T"
-  apply (induct fixing: t' set: typing)
+  apply (induct arbitrary: t' set: typing)
     apply blast
    apply blast
   apply atomize
   apply (ind_cases "s \<degree> t -> t'")
     apply hypsubst