[STATEMENT]
theorem eta_expansion_safe':
  assumes "n \<le> arg_prefix S"
  shows "(\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
n \<le> arg_prefix S
[PROOF STEP]
have "set (take n S) \<subseteq> range Arg" and "length (take n S) = n"
[PROOF STATE]
proof (prove)
using this:
n \<le> arg_prefix S

goal (1 subgoal):
 1. set (take n S) \<subseteq> range Arg &&& length (take n S) = n
[PROOF STEP]
apply (induction S arbitrary: n rule: arg_prefix.induct)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>n. n \<le> arg_prefix [] \<Longrightarrow> set (take n []) \<subseteq> range Arg
 2. \<And>n. n \<le> arg_prefix [] \<Longrightarrow> length (take n []) = n
 3. \<And>x S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> length (take n S) = n; n \<le> arg_prefix (Arg x # S)\<rbrakk> \<Longrightarrow> set (take n (Arg x # S)) \<subseteq> range Arg
 4. \<And>x S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> length (take n S) = n; n \<le> arg_prefix (Arg x # S)\<rbrakk> \<Longrightarrow> length (take n (Arg x # S)) = n
 5. \<And>e1 e2 S n. n \<le> arg_prefix (Alts e1 e2 # S) \<Longrightarrow> set (take n (Alts e1 e2 # S)) \<subseteq> range Arg
 6. \<And>e1 e2 S n. n \<le> arg_prefix (Alts e1 e2 # S) \<Longrightarrow> length (take n (Alts e1 e2 # S)) = n
 7. \<And>x S n. n \<le> arg_prefix (Upd x # S) \<Longrightarrow> set (take n (Upd x # S)) \<subseteq> range Arg
 8. \<And>x S n. n \<le> arg_prefix (Upd x # S) \<Longrightarrow> length (take n (Upd x # S)) = n
 9. \<And>x S n. n \<le> arg_prefix (Dummy x # S) \<Longrightarrow> set (take n (Dummy x # S)) \<subseteq> range Arg
 10. \<And>x S n. n \<le> arg_prefix (Dummy x # S) \<Longrightarrow> length (take n (Dummy x # S)) = n
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x S n xa. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> min (length S) n = n; n \<le> Suc (arg_prefix S); xa \<in> set (take n (Arg x # S))\<rbrakk> \<Longrightarrow> xa \<in> range Arg
 2. \<And>S n. \<lbrakk>\<And>n. n \<le> arg_prefix S \<Longrightarrow> set (take n S) \<subseteq> range Arg; \<And>n. n \<le> arg_prefix S \<Longrightarrow> min (length S) n = n; n \<le> Suc (arg_prefix S)\<rbrakk> \<Longrightarrow> min (Suc (length S)) n = n
[PROOF STEP]
apply (case_tac n, auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
set (take n S) \<subseteq> range Arg
length (take n S) = n

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
hence "S = take n S @ drop n S"
[PROOF STATE]
proof (prove)
using this:
set (take n S) \<subseteq> range Arg
length (take n S) = n

goal (1 subgoal):
 1. S = take n S @ drop n S
[PROOF STEP]
by (metis append_take_drop_id)
[PROOF STATE]
proof (state)
this:
S = take n S @ drop n S

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
with eta_expansion_safe[OF \<open>_ \<subseteq> _\<close>] \<open>length _ = _\<close>
[PROOF STATE]
proof (chain)
picking this:
(?\<Gamma>, eta_expand (length (take n S)) ?e, take n S @ ?S) \<Rightarrow>\<^sup>* (?\<Gamma>, ?e, take n S @ ?S)
length (take n S) = n
S = take n S @ drop n S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(?\<Gamma>, eta_expand (length (take n S)) ?e, take n S @ ?S) \<Rightarrow>\<^sup>* (?\<Gamma>, ?e, take n S @ ?S)
length (take n S) = n
S = take n S @ drop n S

goal (1 subgoal):
 1. (\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Gamma>, eta_expand n e, S) \<Rightarrow>\<^sup>* (\<Gamma>, e, S)

goal:
No subgoals!
[PROOF STEP]
qed