[STATEMENT]
lemma left_right_simps[simp]:
  "left (app l r) = l"
  "right (app l r) = r"
  "is_app t \<Longrightarrow> app (left t) (right t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left (app l r) = l &&& right (app l r) = r &&& (is_app t \<Longrightarrow> app (left t) (right t) = t)
[PROOF STEP]
unfolding is_app_def left_def right_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case unapp (app l r) of Some (l, xa) \<Rightarrow> l) = l &&& (case unapp (app l r) of Some (xa, r) \<Rightarrow> r) = r &&& (unapp t \<noteq> None \<Longrightarrow> app (case unapp t of Some (l, xa) \<Rightarrow> l) (case unapp t of Some (xa, r) \<Rightarrow> r) = t)
[PROOF STEP]
by auto


[STATEMENT]
lemma closed_except_const[simp]: "closed_except (const name) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_except (const name) S
[PROOF STEP]
unfolding closed_except_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees (const name) |\<subseteq>| S
[PROOF STEP]
by auto


[STATEMENT]
lemma closed_except_self: "closed_except t (frees t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_except t (frees t)
[PROOF STEP]
unfolding closed_except_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees t |\<subseteq>| frees t
[PROOF STEP]
by simp


[STATEMENT]
lemma subst_id: "id_env env \<Longrightarrow> subst t env = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id_env env \<Longrightarrow> subst t env = t
[PROOF STEP]
proof (induction t arbitrary: env rule: raw_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name env. id_env env \<Longrightarrow> subst (const name) env = const name
 2. \<And>name env. id_env env \<Longrightarrow> subst (free name) env = free name
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. id_env env \<Longrightarrow> subst t\<^sub>1 env = t\<^sub>1; \<And>env. id_env env \<Longrightarrow> subst t\<^sub>2 env = t\<^sub>2; id_env env\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) env = app t\<^sub>1 t\<^sub>2
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. id_env x \<longrightarrow> subst a x = a) t
[PROOF STEP]
case (abs t)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>name env. id_env env \<Longrightarrow> subst (const name) env = const name
 2. \<And>name env. id_env env \<Longrightarrow> subst (free name) env = free name
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. id_env env \<Longrightarrow> subst t\<^sub>1 env = t\<^sub>1; \<And>env. id_env env \<Longrightarrow> subst t\<^sub>2 env = t\<^sub>2; id_env env\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) env = app t\<^sub>1 t\<^sub>2
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. id_env x \<longrightarrow> subst a x = a) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred (\<lambda>a. \<forall>x. id_env x \<longrightarrow> subst a x = a) t
[PROOF STEP]
by (rule raw_subst_id)
[PROOF STATE]
proof (state)
this:
abs_pred (\<lambda>a. \<forall>x. id_env x \<longrightarrow> subst a x = a) t

goal (3 subgoals):
 1. \<And>name env. id_env env \<Longrightarrow> subst (const name) env = const name
 2. \<And>name env. id_env env \<Longrightarrow> subst (free name) env = free name
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. id_env env \<Longrightarrow> subst t\<^sub>1 env = t\<^sub>1; \<And>env. id_env env \<Longrightarrow> subst t\<^sub>2 env = t\<^sub>2; id_env env\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) env = app t\<^sub>1 t\<^sub>2
[PROOF STEP]
qed (auto split: option.splits)


[STATEMENT]
lemma subst_drop: "x |\<notin>| frees t \<Longrightarrow> subst t (fmdrop x env) = subst t env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x |\<notin>| frees t \<Longrightarrow> subst t (fmdrop x env) = subst t env
[PROOF STEP]
proof (induction t arbitrary: env rule: raw_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name env. x |\<notin>| frees (const name) \<Longrightarrow> subst (const name) (fmdrop x env) = subst (const name) env
 2. \<And>name env. x |\<notin>| frees (free name) \<Longrightarrow> subst (free name) (fmdrop x env) = subst (free name) env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. x |\<notin>| frees t\<^sub>1 \<Longrightarrow> subst t\<^sub>1 (fmdrop x env) = subst t\<^sub>1 env; \<And>env. x |\<notin>| frees t\<^sub>2 \<Longrightarrow> subst t\<^sub>2 (fmdrop x env) = subst t\<^sub>2 env; x |\<notin>| frees (app t\<^sub>1 t\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (fmdrop x env) = subst (app t\<^sub>1 t\<^sub>2) env
 4. \<And>t. abs_pred (\<lambda>a. x |\<notin>| frees a \<longrightarrow> (\<forall>xa. subst a (fmdrop x xa) = subst a xa)) t
[PROOF STEP]
case (abs t)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>name env. x |\<notin>| frees (const name) \<Longrightarrow> subst (const name) (fmdrop x env) = subst (const name) env
 2. \<And>name env. x |\<notin>| frees (free name) \<Longrightarrow> subst (free name) (fmdrop x env) = subst (free name) env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. x |\<notin>| frees t\<^sub>1 \<Longrightarrow> subst t\<^sub>1 (fmdrop x env) = subst t\<^sub>1 env; \<And>env. x |\<notin>| frees t\<^sub>2 \<Longrightarrow> subst t\<^sub>2 (fmdrop x env) = subst t\<^sub>2 env; x |\<notin>| frees (app t\<^sub>1 t\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (fmdrop x env) = subst (app t\<^sub>1 t\<^sub>2) env
 4. \<And>t. abs_pred (\<lambda>a. x |\<notin>| frees a \<longrightarrow> (\<forall>xa. subst a (fmdrop x xa) = subst a xa)) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred (\<lambda>a. x |\<notin>| frees a \<longrightarrow> (\<forall>xa. subst a (fmdrop x xa) = subst a xa)) t
[PROOF STEP]
by (rule raw_subst_drop)
[PROOF STATE]
proof (state)
this:
abs_pred (\<lambda>a. x |\<notin>| frees a \<longrightarrow> (\<forall>xa. subst a (fmdrop x xa) = subst a xa)) t

goal (3 subgoals):
 1. \<And>name env. x |\<notin>| frees (const name) \<Longrightarrow> subst (const name) (fmdrop x env) = subst (const name) env
 2. \<And>name env. x |\<notin>| frees (free name) \<Longrightarrow> subst (free name) (fmdrop x env) = subst (free name) env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. x |\<notin>| frees t\<^sub>1 \<Longrightarrow> subst t\<^sub>1 (fmdrop x env) = subst t\<^sub>1 env; \<And>env. x |\<notin>| frees t\<^sub>2 \<Longrightarrow> subst t\<^sub>2 (fmdrop x env) = subst t\<^sub>2 env; x |\<notin>| frees (app t\<^sub>1 t\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (fmdrop x env) = subst (app t\<^sub>1 t\<^sub>2) env
[PROOF STEP]
qed (auto split: option.splits)


[STATEMENT]
lemma subst_frees: "fmpred (\<lambda>_. closed) env \<Longrightarrow> frees (subst t env) = frees t |-| fmdom env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_env env \<Longrightarrow> frees (subst t env) = frees t |-| fmdom env
[PROOF STEP]
proof (induction t arbitrary: env rule: raw_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name env. closed_env env \<Longrightarrow> frees (subst (const name) env) = frees (const name) |-| fmdom env
 2. \<And>name env. closed_env env \<Longrightarrow> frees (subst (free name) env) = frees (free name) |-| fmdom env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>1 env) = frees t\<^sub>1 |-| fmdom env; \<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>2 env) = frees t\<^sub>2 |-| fmdom env; closed_env env\<rbrakk> \<Longrightarrow> frees (subst (app t\<^sub>1 t\<^sub>2) env) = frees (app t\<^sub>1 t\<^sub>2) |-| fmdom env
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. closed_env x \<longrightarrow> frees (subst a x) = frees a |-| fmdom x) t
[PROOF STEP]
case (abs t)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>name env. closed_env env \<Longrightarrow> frees (subst (const name) env) = frees (const name) |-| fmdom env
 2. \<And>name env. closed_env env \<Longrightarrow> frees (subst (free name) env) = frees (free name) |-| fmdom env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>1 env) = frees t\<^sub>1 |-| fmdom env; \<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>2 env) = frees t\<^sub>2 |-| fmdom env; closed_env env\<rbrakk> \<Longrightarrow> frees (subst (app t\<^sub>1 t\<^sub>2) env) = frees (app t\<^sub>1 t\<^sub>2) |-| fmdom env
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. closed_env x \<longrightarrow> frees (subst a x) = frees a |-| fmdom x) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred (\<lambda>a. \<forall>x. closed_env x \<longrightarrow> frees (subst a x) = frees a |-| fmdom x) t
[PROOF STEP]
by (rule raw_subst_frees)
[PROOF STATE]
proof (state)
this:
abs_pred (\<lambda>a. \<forall>x. closed_env x \<longrightarrow> frees (subst a x) = frees a |-| fmdom x) t

goal (3 subgoals):
 1. \<And>name env. closed_env env \<Longrightarrow> frees (subst (const name) env) = frees (const name) |-| fmdom env
 2. \<And>name env. closed_env env \<Longrightarrow> frees (subst (free name) env) = frees (free name) |-| fmdom env
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>1 env) = frees t\<^sub>1 |-| fmdom env; \<And>env. closed_env env \<Longrightarrow> frees (subst t\<^sub>2 env) = frees t\<^sub>2 |-| fmdom env; closed_env env\<rbrakk> \<Longrightarrow> frees (subst (app t\<^sub>1 t\<^sub>2) env) = frees (app t\<^sub>1 t\<^sub>2) |-| fmdom env
[PROOF STEP]
qed (auto split: option.splits simp: closed_except_def)


[STATEMENT]
lemma subst_consts': "consts (subst t env) = consts t |\<union>| ffUnion (consts |`| fmimage env (frees t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts (subst t env) = consts t |\<union>| ffUnion (consts |`| fmimage env (frees t))
[PROOF STEP]
proof (induction t arbitrary: env rule: raw_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>name env. consts (subst (free name) env) = consts (free name) |\<union>| ffUnion (consts |`| fmimage env (frees (free name)))
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
case (free name)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>name env. consts (subst (free name) env) = consts (free name) |\<union>| ffUnion (consts |`| fmimage env (frees (free name)))
 3. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts (subst (free name) env) = consts (free name) |\<union>| ffUnion (consts |`| fmimage env (frees (free name)))
[PROOF STEP]
by (auto
          split: option.splits
          simp: ffUnion_alt_def fmlookup_ran_iff fmlookup_image_iff fmlookup_dom_iff
          intro!: fBexI)
[PROOF STATE]
proof (state)
this:
consts (subst (free name) env) = consts (free name) |\<union>| ffUnion (consts |`| fmimage env (frees (free name)))

goal (3 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
case (abs t)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t
[PROOF STEP]
by (rule raw_subst_consts')
[PROOF STATE]
proof (state)
this:
abs_pred (\<lambda>a. \<forall>x. consts (subst a x) = consts a |\<union>| ffUnion (consts |`| fmimage x (frees a))) t

goal (2 subgoals):
 1. \<And>name env. consts (subst (const name) env) = consts (const name) |\<union>| ffUnion (consts |`| fmimage env (frees (const name)))
 2. \<And>t\<^sub>1 t\<^sub>2 env. \<lbrakk>\<And>env. consts (subst t\<^sub>1 env) = consts t\<^sub>1 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>1)); \<And>env. consts (subst t\<^sub>2 env) = consts t\<^sub>2 |\<union>| ffUnion (consts |`| fmimage env (frees t\<^sub>2))\<rbrakk> \<Longrightarrow> consts (subst (app t\<^sub>1 t\<^sub>2) env) = consts (app t\<^sub>1 t\<^sub>2) |\<union>| ffUnion (consts |`| fmimage env (frees (app t\<^sub>1 t\<^sub>2)))
[PROOF STEP]
qed (auto simp: funion_image_bind_eq finter_funion_distrib fbind_funion)


[STATEMENT]
lemma match_simps[simp]:
  "match (t\<^sub>1 $ t\<^sub>2) (app u\<^sub>1 u\<^sub>2) = do {
    env\<^sub>1 \<leftarrow> match t\<^sub>1 u\<^sub>1;
    env\<^sub>2 \<leftarrow> match t\<^sub>2 u\<^sub>2;
    Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)
  }"
  "match (Const name) (const name') = (if name = name' then Some fmempty else None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match (t\<^sub>1 $ t\<^sub>2) (app u\<^sub>1 u\<^sub>2) = match t\<^sub>1 u\<^sub>1 \<bind> (\<lambda>env\<^sub>1. match t\<^sub>2 u\<^sub>2 \<bind> (\<lambda>env\<^sub>2. Some (env\<^sub>1 ++\<^sub>f env\<^sub>2))) &&& match (Const name) (const name') = (if name = name' then Some fmempty else None)
[PROOF STEP]
by auto


[STATEMENT]
lemma match_some_induct[consumes 1, case_names app const free]:
  assumes "match t u = Some env"
  assumes "\<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. P t\<^sub>1 u\<^sub>1 env\<^sub>1 \<Longrightarrow> match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1 \<Longrightarrow> P t\<^sub>2 u\<^sub>2 env\<^sub>2 \<Longrightarrow> match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2 \<Longrightarrow> P (t\<^sub>1 $ t\<^sub>2) (app u\<^sub>1 u\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2)"
  assumes "\<And>name. P (Const name) (const name) fmempty"
  assumes "\<And>name u. P (Free name) u (fmupd name u fmempty)"
  shows "P t u env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t u env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match t u = Some env
\<lbrakk>P ?t\<^sub>1 ?u\<^sub>1 ?env\<^sub>1; match ?t\<^sub>1 ?u\<^sub>1 = Some ?env\<^sub>1; P ?t\<^sub>2 ?u\<^sub>2 ?env\<^sub>2; match ?t\<^sub>2 ?u\<^sub>2 = Some ?env\<^sub>2\<rbrakk> \<Longrightarrow> P (?t\<^sub>1 $ ?t\<^sub>2) (app ?u\<^sub>1 ?u\<^sub>2) (?env\<^sub>1 ++\<^sub>f ?env\<^sub>2)
P (Const ?name) (const ?name) fmempty
P (Free ?name) ?u (fmupd ?name ?u fmempty)

goal (1 subgoal):
 1. P t u env
[PROOF STEP]
by (induction t u arbitrary: env rule: match.induct)
   (auto split: option.splits if_splits elim!: option_bindE)


[STATEMENT]
lemma match_dom: "match p t = Some env \<Longrightarrow> fmdom env = frees p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match p t = Some env \<Longrightarrow> fmdom env = frees p
[PROOF STEP]
by (induction p arbitrary: t env)
   (fastforce split: option.splits if_splits elim: option_bindE)+


[STATEMENT]
lemma match_vars: "match p t = Some env \<Longrightarrow> fmpred (\<lambda>_ u. frees u |\<subseteq>| frees t) env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match p t = Some env \<Longrightarrow> fmpred (\<lambda>_ u. frees u |\<subseteq>| frees t) env
[PROOF STEP]
proof (induction p t env rule: match_some_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>1) env\<^sub>1; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>2) env\<^sub>2; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) (env\<^sub>1 ++\<^sub>f env\<^sub>2)
 2. \<And>name. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (const name)) fmempty
 3. \<And>name u. fmpred (\<lambda>_ ua. frees ua |\<subseteq>| frees u) (fmupd name u fmempty)
[PROOF STEP]
case (app t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2)
[PROOF STATE]
proof (state)
this:
fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>1) env\<^sub>1
fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>2) env\<^sub>2
match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1
match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2

goal (3 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>2 u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>1) env\<^sub>1; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>2) env\<^sub>2; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2\<rbrakk> \<Longrightarrow> fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) (env\<^sub>1 ++\<^sub>f env\<^sub>2)
 2. \<And>name. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (const name)) fmempty
 3. \<And>name u. fmpred (\<lambda>_ ua. frees ua |\<subseteq>| frees u) (fmupd name u fmempty)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) (env\<^sub>1 ++\<^sub>f env\<^sub>2)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) env\<^sub>1
 2. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) env\<^sub>2
[PROOF STEP]
using app
[PROOF STATE]
proof (prove)
using this:
fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>1) env\<^sub>1
fmpred (\<lambda>_ u. frees u |\<subseteq>| frees u\<^sub>2) env\<^sub>2
match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1
match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2

goal (2 subgoals):
 1. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) env\<^sub>1
 2. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) env\<^sub>2
[PROOF STEP]
by (fastforce intro: fmpred_mono_strong)+
[PROOF STATE]
proof (state)
this:
fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (app u\<^sub>1 u\<^sub>2)) (env\<^sub>1 ++\<^sub>f env\<^sub>2)

goal (2 subgoals):
 1. \<And>name. fmpred (\<lambda>_ u. frees u |\<subseteq>| frees (const name)) fmempty
 2. \<And>name u. fmpred (\<lambda>_ ua. frees ua |\<subseteq>| frees u) (fmupd name u fmempty)
[PROOF STEP]
qed auto


[STATEMENT]
lemma match_appE_split:
  assumes "match (t\<^sub>1 $ t\<^sub>2) u = Some env"
  obtains u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2 where
    "u = app u\<^sub>1 u\<^sub>2" "match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1" "match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2" "env = env\<^sub>1 ++\<^sub>f env\<^sub>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>u = app u\<^sub>1 u\<^sub>2; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; env = env\<^sub>1 ++\<^sub>f env\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match (t\<^sub>1 $ t\<^sub>2) u = Some env

goal (1 subgoal):
 1. (\<And>u\<^sub>1 u\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>u = app u\<^sub>1 u\<^sub>2; match t\<^sub>1 u\<^sub>1 = Some env\<^sub>1; match t\<^sub>2 u\<^sub>2 = Some env\<^sub>2; env = env\<^sub>1 ++\<^sub>f env\<^sub>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto split: option.splits elim!: option_bindE)


[STATEMENT]
lemma subst_consts:
  assumes "consts t |\<subseteq>| S" "fmpred (\<lambda>_ u. consts u |\<subseteq>| S) env"
  shows "consts (subst t env) |\<subseteq>| S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts (subst t env) |\<subseteq>| S
[PROOF STEP]
apply (subst subst_consts')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts t |\<union>| ffUnion (consts |`| fmimage env (frees t)) |\<subseteq>| S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
consts t |\<subseteq>| S
fmpred (\<lambda>_ u. consts u |\<subseteq>| S) env

goal (1 subgoal):
 1. consts t |\<union>| ffUnion (consts |`| fmimage env (frees t)) |\<subseteq>| S
[PROOF STEP]
by (auto intro!: ffUnion_least)


[STATEMENT]
lemma subst_empty[simp]: "subst t fmempty = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t fmempty = t
[PROOF STEP]
by (auto simp: subst_id)


[STATEMENT]
lemma subst_drop_fset: "fdisjnt S (frees t) \<Longrightarrow> subst t (fmdrop_fset S env) = subst t env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt S (frees t) \<Longrightarrow> subst t (fmdrop_fset S env) = subst t env
[PROOF STEP]
by (induct S) (auto simp: subst_drop fdisjnt_alt_def)


[STATEMENT]
lemma subst_restrict:
  assumes "frees t |\<subseteq>| M"
  shows "subst t (fmrestrict_fset M env) = subst t env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmrestrict_fset M env) = subst t env
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst t (fmrestrict_fset M env) = subst t env
[PROOF STEP]
have *: "fmrestrict_fset M env = fmdrop_fset (fmdom env - M) env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmrestrict_fset M env = fmdrop_fset (fmdom env |-| M) env
[PROOF STEP]
by (rule fmap_ext) auto
[PROOF STATE]
proof (state)
this:
fmrestrict_fset M env = fmdrop_fset (fmdom env |-| M) env

goal (1 subgoal):
 1. subst t (fmrestrict_fset M env) = subst t env
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmrestrict_fset M env) = subst t env
[PROOF STEP]
apply (subst *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmdrop_fset (fmdom env |-| M) env) = subst t env
[PROOF STEP]
apply (subst subst_drop_fset)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fdisjnt (fmdom env |-| M) (frees t)
 2. subst t env = subst t env
[PROOF STEP]
unfolding fdisjnt_alt_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. fmdom env |-| M |\<inter>| frees t = {||}
 2. subst t env = subst t env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
frees t |\<subseteq>| M

goal (2 subgoals):
 1. fmdom env |-| M |\<inter>| frees t = {||}
 2. subst t env = subst t env
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset M env) = subst t env

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_closed_except_id:
  assumes "closed_except t S" "fdisjnt (fmdom env) S"
  shows "subst t env = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t env = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closed_except t S
fdisjnt (fmdom env) S

goal (1 subgoal):
 1. subst t env = t
[PROOF STEP]
by (metis fdisjnt_subset_right fmdom_drop_fset fminus_cancel fmrestrict_fset_dom
          fmrestrict_fset_null closed_except_def subst_drop_fset subst_empty)


[STATEMENT]
lemma subst_closed_except_preserved:
  assumes "closed_except t S" "fdisjnt (fmdom env) S"
  shows "closed_except (subst t env) S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_except (subst t env) S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closed_except t S
fdisjnt (fmdom env) S

goal (1 subgoal):
 1. closed_except (subst t env) S
[PROOF STEP]
by (metis subst_closed_except_id)


[STATEMENT]
lemma subst_indep0:
  assumes "closed_env env\<^sub>2" "fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)"
  shows "subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t env\<^sub>2) env\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t env\<^sub>2) env\<^sub>1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closed_env env\<^sub>2
fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)

goal (1 subgoal):
 1. subst t (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t env\<^sub>2) env\<^sub>1
[PROOF STEP]
proof (induction t arbitrary: env\<^sub>1 env\<^sub>2 rule: raw_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (free name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (free name) env\<^sub>2) env\<^sub>1
 3. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
case (free name)
[PROOF STATE]
proof (state)
this:
closed_env env\<^sub>2
fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)

goal (4 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (free name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (free name) env\<^sub>2) env\<^sub>1
 3. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
 4. \<And>t. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (free name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (free name) env\<^sub>2) env\<^sub>1
[PROOF STEP]
using \<open>closed_env env\<^sub>2\<close>
[PROOF STATE]
proof (prove)
using this:
closed_env env\<^sub>2

goal (1 subgoal):
 1. subst (free name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (free name) env\<^sub>2) env\<^sub>1
[PROOF STEP]
by (cases rule: fmpred_cases[where x = name]) (auto simp: subst_closed_id)
[PROOF STATE]
proof (state)
this:
subst (free name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (free name) env\<^sub>2) env\<^sub>1

goal (3 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
case (abs t)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
 3. \<And>t. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t
[PROOF STEP]
by (rule raw_subst_indep)
[PROOF STATE]
proof (state)
this:
abs_pred (\<lambda>a. \<forall>x xa. closed_env xa \<longrightarrow> fdisjnt (fmdom x) (fmdom xa) \<longrightarrow> subst a (x ++\<^sub>f xa) = subst (subst a xa) x) t

goal (2 subgoals):
 1. \<And>name env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (const name) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (const name) env\<^sub>2) env\<^sub>1
 2. \<And>t\<^sub>1 t\<^sub>2 env\<^sub>1 env\<^sub>2. \<lbrakk>\<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>1 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>1 env\<^sub>2) env\<^sub>1; \<And>env\<^sub>1 env\<^sub>2. \<lbrakk>closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst t\<^sub>2 (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst t\<^sub>2 env\<^sub>2) env\<^sub>1; closed_env env\<^sub>2; fdisjnt (fmdom env\<^sub>1) (fmdom env\<^sub>2)\<rbrakk> \<Longrightarrow> subst (app t\<^sub>1 t\<^sub>2) (env\<^sub>1 ++\<^sub>f env\<^sub>2) = subst (subst (app t\<^sub>1 t\<^sub>2) env\<^sub>2) env\<^sub>1
[PROOF STEP]
qed auto


[STATEMENT]
lemma subst_indep:
  assumes "closed_env \<Gamma>'"
  shows "subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>'))
[PROOF STEP]
by (metis subst_restrict')
[PROOF STATE]
proof (state)
this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>'))

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>'))

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "\<dots> = subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>')) = subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>')
[PROOF STEP]
by (smt fmlookup_add fmlookup_restrict_fset subst_cong)
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>')) = subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t) (\<Gamma> ++\<^sub>f \<Gamma>')) = subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "\<dots> = subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>')
[PROOF STEP]
by (rule subst_cong) (simp add: fmfilter_alt_defs(5))
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t) \<Gamma> ++\<^sub>f \<Gamma>') = subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "\<dots> = subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)
[PROOF STEP]
apply (rule subst_indep0[OF assms])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fdisjnt (fmdom (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)) (fmdom \<Gamma>')
[PROOF STEP]
using fmdom_restrict_fset
[PROOF STATE]
proof (prove)
using this:
fmdom (fmrestrict_fset ?A ?m) |\<subseteq>| ?A

goal (1 subgoal):
 1. fdisjnt (fmdom (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)) (fmdom \<Gamma>')
[PROOF STEP]
unfolding fdisjnt_alt_def
[PROOF STATE]
proof (prove)
using this:
fmdom (fmrestrict_fset ?A ?m) |\<subseteq>| ?A

goal (1 subgoal):
 1. fmdom (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>) |\<inter>| fmdom \<Gamma>' = {||}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst t (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>)

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "\<dots> = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>) = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closed_env \<Gamma>'

goal (1 subgoal):
 1. subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>) = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)
[PROOF STEP]
by (auto simp: subst_frees)
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>) = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') (fmrestrict_fset (frees t |-| fmdom \<Gamma>') \<Gamma>) = subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>)

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
have "\<dots> = subst (subst t \<Gamma>') \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') (fmrestrict_fset (frees (subst t \<Gamma>')) \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>

goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst (subst t \<Gamma>') \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_indep':
  assumes "closed_env \<Gamma>'" "fdisjnt (fmdom \<Gamma>') (fmdom \<Gamma>)"
  shows "subst t (\<Gamma>' ++\<^sub>f \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (\<Gamma>' ++\<^sub>f \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
closed_env \<Gamma>'
fdisjnt (fmdom \<Gamma>') (fmdom \<Gamma>)

goal (1 subgoal):
 1. subst t (\<Gamma>' ++\<^sub>f \<Gamma>) = subst (subst t \<Gamma>') \<Gamma>
[PROOF STEP]
by (metis subst_indep fmadd_disjnt)


[STATEMENT]
lemma subst_twice:
  assumes "\<Gamma>' \<subseteq>\<^sub>f \<Gamma>" "closed_env \<Gamma>'"
  shows "subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
have "subst (subst t \<Gamma>') \<Gamma> = subst t (\<Gamma> ++\<^sub>f \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t (\<Gamma> ++\<^sub>f \<Gamma>')
[PROOF STEP]
apply (rule subst_indep[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed_env \<Gamma>'
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') \<Gamma> = subst t (\<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') \<Gamma> = subst t (\<Gamma> ++\<^sub>f \<Gamma>')

goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
have "\<dots> = subst t \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t \<Gamma>
[PROOF STEP]
apply (rule subst_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x |\<in>| frees t \<Longrightarrow> fmlookup (\<Gamma> ++\<^sub>f \<Gamma>') x = fmlookup \<Gamma> x
[PROOF STEP]
using \<open>\<Gamma>' \<subseteq>\<^sub>f \<Gamma>\<close>
[PROOF STATE]
proof (prove)
using this:
\<Gamma>' \<subseteq>\<^sub>f \<Gamma>

goal (1 subgoal):
 1. \<And>x. x |\<in>| frees t \<Longrightarrow> fmlookup (\<Gamma> ++\<^sub>f \<Gamma>') x = fmlookup \<Gamma> x
[PROOF STEP]
unfolding fmsubset_alt_def
[PROOF STATE]
proof (prove)
using this:
fmpred (\<lambda>k v. fmlookup \<Gamma> k = Some v) \<Gamma>'

goal (1 subgoal):
 1. \<And>x. x |\<in>| frees t \<Longrightarrow> fmlookup (\<Gamma> ++\<^sub>f \<Gamma>') x = fmlookup \<Gamma> x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
subst t (\<Gamma> ++\<^sub>f \<Gamma>') = subst t \<Gamma>

goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>

goal (1 subgoal):
 1. subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
subst (subst t \<Gamma>') \<Gamma> = subst t \<Gamma>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchs_alt_def0:
  assumes "length ps = length vs"
  shows "map_option (\<lambda>env. m ++\<^sub>f env) (matchs ps vs) = map_option (foldl (++\<^sub>f) m) (those (map2 match ps vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs ps vs) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match ps vs))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length ps = length vs

goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs ps vs) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match ps vs))
[PROOF STEP]
proof (induction arbitrary: m rule: list_induct2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m. map_option ((++\<^sub>f) m) (matchs [] []) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match [] []))
 2. \<And>x xs y ys m. \<lbrakk>length xs = length ys; \<And>m. map_option ((++\<^sub>f) m) (matchs xs ys) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match xs ys))\<rbrakk> \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
case (Cons x xs y ys)
[PROOF STATE]
proof (state)
this:
length xs = length ys
map_option ((++\<^sub>f) ?m) (matchs xs ys) = map_option (foldl (++\<^sub>f) ?m) (those (Term_Utils.map2 match xs ys))

goal (2 subgoals):
 1. \<And>m. map_option ((++\<^sub>f) m) (matchs [] []) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match [] []))
 2. \<And>x xs y ys m. \<lbrakk>length xs = length ys; \<And>m. map_option ((++\<^sub>f) m) (matchs xs ys) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match xs ys))\<rbrakk> \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
proof (cases "match x y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. match x y = None \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
 2. \<And>a. match x y = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
case x_y: Some
[PROOF STATE]
proof (state)
this:
match x y = Some a_

goal (2 subgoals):
 1. match x y = None \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
 2. \<And>a. match x y = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
proof (cases "matchs xs ys")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. matchs xs ys = None \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
 2. \<And>a. matchs xs ys = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
matchs xs ys = None

goal (2 subgoals):
 1. matchs xs ys = None \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
 2. \<And>a. matchs xs ys = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
with x_y Cons
[PROOF STATE]
proof (chain)
picking this:
match x y = Some a_
length xs = length ys
map_option ((++\<^sub>f) ?m) (matchs xs ys) = map_option (foldl (++\<^sub>f) ?m) (those (Term_Utils.map2 match xs ys))
matchs xs ys = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
match x y = Some a_
length xs = length ys
map_option ((++\<^sub>f) ?m) (matchs xs ys) = map_option (foldl (++\<^sub>f) ?m) (those (Term_Utils.map2 match xs ys))
matchs xs ys = None

goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))

goal (1 subgoal):
 1. \<And>a. matchs xs ys = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. matchs xs ys = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
case Some
[PROOF STATE]
proof (state)
this:
matchs xs ys = Some a_

goal (1 subgoal):
 1. \<And>a. matchs xs ys = Some a \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
with x_y
[PROOF STATE]
proof (chain)
picking this:
match x y = Some a___
matchs xs ys = Some a_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
match x y = Some a___
matchs xs ys = Some a_

goal (1 subgoal):
 1. map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>match x y = Some a___; matchs xs ys = Some a_\<rbrakk> \<Longrightarrow> Some (m ++\<^sub>f a___ ++\<^sub>f a_) = map_option (foldl (++\<^sub>f) m) (map_option ((#) a___) (those (Term_Utils.map2 match xs ys)))
[PROOF STEP]
using Cons(2)
[PROOF STATE]
proof (prove)
using this:
map_option ((++\<^sub>f) ?m) (matchs xs ys) = map_option (foldl (++\<^sub>f) ?m) (those (Term_Utils.map2 match xs ys))

goal (1 subgoal):
 1. \<lbrakk>match x y = Some a___; matchs xs ys = Some a_\<rbrakk> \<Longrightarrow> Some (m ++\<^sub>f a___ ++\<^sub>f a_) = map_option (foldl (++\<^sub>f) m) (map_option ((#) a___) (those (Term_Utils.map2 match xs ys)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>match x y = Some a___; matchs xs ys = Some a_; \<And>m. Some (m ++\<^sub>f a_) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match xs ys))\<rbrakk> \<Longrightarrow> map_option (foldl (++\<^sub>f) (m ++\<^sub>f a___)) (those (Term_Utils.map2 match xs ys)) = map_option (foldl (++\<^sub>f) m) (map_option ((#) a___) (those (Term_Utils.map2 match xs ys)))
[PROOF STEP]
apply (subst option.map_comp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>match x y = Some a___; matchs xs ys = Some a_; \<And>m. Some (m ++\<^sub>f a_) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match xs ys))\<rbrakk> \<Longrightarrow> map_option (foldl (++\<^sub>f) (m ++\<^sub>f a___)) (those (Term_Utils.map2 match xs ys)) = map_option (foldl (++\<^sub>f) m \<circ> (#) a___) (those (Term_Utils.map2 match xs ys))
[PROOF STEP]
by (auto cong: map_option_cong)
[PROOF STATE]
proof (state)
this:
map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))

goal (1 subgoal):
 1. match x y = None \<Longrightarrow> map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
map_option ((++\<^sub>f) m) (matchs (x # xs) (y # ys)) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match (x # xs) (y # ys)))

goal (1 subgoal):
 1. \<And>m. map_option ((++\<^sub>f) m) (matchs [] []) = map_option (foldl (++\<^sub>f) m) (those (Term_Utils.map2 match [] []))
[PROOF STEP]
qed simp


[STATEMENT]
lemma matchs_alt_def:
  assumes "length ps = length vs"
  shows "matchs ps vs = map_option (foldl (++\<^sub>f) fmempty) (those (map2 match ps vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matchs ps vs = map_option (foldl (++\<^sub>f) fmempty) (those (Term_Utils.map2 match ps vs))
[PROOF STEP]
by (subst matchs_alt_def0[where m = fmempty, simplified, symmetric, OF assms])
   (simp add: option.map_ident)


[STATEMENT]
lemma matchs_neq_length_none[simp]: "length xs \<noteq> length ys \<Longrightarrow> matchs xs ys = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs \<noteq> length ys \<Longrightarrow> matchs xs ys = None
[PROOF STEP]
by (induct xs ys rule: matchs.induct) fastforce+


[STATEMENT]
lemma matchs_app[simp]:
  assumes "length xs\<^sub>2 = length ys\<^sub>2"
  shows "matchs (xs\<^sub>1 @ xs\<^sub>2) (ys\<^sub>1 @ ys\<^sub>2) =
          matchs xs\<^sub>1 ys\<^sub>1 \<bind> (\<lambda>env\<^sub>1. matchs xs\<^sub>2 ys\<^sub>2 \<bind> (\<lambda>env\<^sub>2. Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matchs (xs\<^sub>1 @ xs\<^sub>2) (ys\<^sub>1 @ ys\<^sub>2) = matchs xs\<^sub>1 ys\<^sub>1 \<bind> (\<lambda>env\<^sub>1. matchs xs\<^sub>2 ys\<^sub>2 \<bind> (\<lambda>env\<^sub>2. Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xs\<^sub>2 = length ys\<^sub>2

goal (1 subgoal):
 1. matchs (xs\<^sub>1 @ xs\<^sub>2) (ys\<^sub>1 @ ys\<^sub>2) = matchs xs\<^sub>1 ys\<^sub>1 \<bind> (\<lambda>env\<^sub>1. matchs xs\<^sub>2 ys\<^sub>2 \<bind> (\<lambda>env\<^sub>2. Some (env\<^sub>1 ++\<^sub>f env\<^sub>2)))
[PROOF STEP]
by (induct xs\<^sub>1 ys\<^sub>1 rule: matchs.induct) fastforce+


[STATEMENT]
lemma find_match_map:
  "find_match (map (\<lambda>(pat, t). (pat, f pat t)) cs) t =
    map_option (\<lambda>(env, pat, rhs). (env, pat, f pat rhs)) (find_match cs t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_match (map (\<lambda>(pat, t). (pat, f pat t)) cs) t = map_option (\<lambda>(env, pat, rhs). (env, pat, f pat rhs)) (find_match cs t)
[PROOF STEP]
by (induct cs) (auto split: option.splits)


[STATEMENT]
lemma find_match_elem:
  assumes "find_match cs t = Some (env, pat, rhs)"
  shows "(pat, rhs) \<in> set cs" "match pat t = Some env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pat, rhs) \<in> set cs &&& match pat t = Some env
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_match cs t = Some (env, pat, rhs)

goal (1 subgoal):
 1. (pat, rhs) \<in> set cs &&& match pat t = Some env
[PROOF STEP]
by (induct cs) (auto split: option.splits)


[STATEMENT]
lemma match_subst_closed:
  assumes "match pat t = Some env" "closed_except rhs (frees pat)" "closed t"
  shows "closed (subst rhs env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (subst rhs env)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match pat t = Some env
closed_except rhs (frees pat)
closed t

goal (1 subgoal):
 1. closed (subst rhs env)
[PROOF STEP]
by (smt fminusE fmpred_iff fset_mp fsubsetI closed_except_def match_vars match_dom subst_frees)


[STATEMENT]
lemma rewrite_step_closed:
  assumes "frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1" "(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'" "closed u"
  shows "closed u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed u'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'
closed u
[PROOF STEP]
obtain env where *: "match t\<^sub>1 u = Some env"
[PROOF STATE]
proof (prove)
using this:
frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'
closed u

goal (1 subgoal):
 1. (\<And>env. match t\<^sub>1 u = Some env \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
match t\<^sub>1 u = Some env

goal (1 subgoal):
 1. closed u'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
match t\<^sub>1 u = Some env
[PROOF STEP]
have "closed (subst t\<^sub>2 env)"
[PROOF STATE]
proof (prove)
using this:
match t\<^sub>1 u = Some env

goal (1 subgoal):
 1. closed (subst t\<^sub>2 env)
[PROOF STEP]
apply (rule match_subst_closed[where pat = t\<^sub>1 and t = u])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closed_except t\<^sub>2 (frees t\<^sub>1)
 2. closed u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'
closed u

goal (2 subgoals):
 1. closed_except t\<^sub>2 (frees t\<^sub>1)
 2. closed u
[PROOF STEP]
unfolding closed_except_def
[PROOF STATE]
proof (prove)
using this:
frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'
frees u |\<subseteq>| {||}

goal (2 subgoals):
 1. frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
 2. frees u |\<subseteq>| {||}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed (subst t\<^sub>2 env)

goal (1 subgoal):
 1. closed u'
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
match t\<^sub>1 u = Some env
closed (subst t\<^sub>2 env)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
match t\<^sub>1 u = Some env
closed (subst t\<^sub>2 env)

goal (1 subgoal):
 1. closed u'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
match t\<^sub>1 u = Some env
closed (subst t\<^sub>2 env)
frees t\<^sub>2 |\<subseteq>| frees t\<^sub>1
(t\<^sub>1, t\<^sub>2) \<turnstile> u \<rightarrow> u'
closed u

goal (1 subgoal):
 1. closed u'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closed u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchesI[intro]: "subst t env = u \<Longrightarrow> t \<lesssim> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t env = u \<Longrightarrow> t \<lesssim> u
[PROOF STEP]
unfolding matches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst t env = u \<Longrightarrow> \<exists>env. subst t env = u
[PROOF STEP]
by auto


[STATEMENT]
lemma matchesE[elim]:
  assumes "t \<lesssim> u"
  obtains env where "subst t env = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>env. subst t env = u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t \<lesssim> u

goal (1 subgoal):
 1. (\<And>env. subst t env = u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding matches_def
[PROOF STATE]
proof (prove)
using this:
\<exists>env. subst t env = u

goal (1 subgoal):
 1. (\<And>env. subst t env = u \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma overlapping_refl: "overlapping t t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. overlapping t t
[PROOF STEP]
unfolding overlapping_def matches_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u. (\<exists>env. subst t env = u) \<and> (\<exists>env. subst t env = u)
[PROOF STEP]
by blast


[STATEMENT]
lemma overlapping_sym: "overlapping t u \<Longrightarrow> overlapping u t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. overlapping t u \<Longrightarrow> overlapping u t
[PROOF STEP]
unfolding overlapping_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ua. t \<lesssim> ua \<and> u \<lesssim> ua \<Longrightarrow> \<exists>ua. u \<lesssim> ua \<and> t \<lesssim> ua
[PROOF STEP]
by auto


[STATEMENT]
lemma overlappingI[intro]: "s \<lesssim> u \<Longrightarrow> t \<lesssim> u \<Longrightarrow> overlapping s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<lesssim> u; t \<lesssim> u\<rbrakk> \<Longrightarrow> overlapping s t
[PROOF STEP]
unfolding overlapping_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<lesssim> u; t \<lesssim> u\<rbrakk> \<Longrightarrow> \<exists>u. s \<lesssim> u \<and> t \<lesssim> u
[PROOF STEP]
by auto


[STATEMENT]
lemma overlappingE[elim]:
  assumes "overlapping s t"
  obtains u where "s \<lesssim> u" "t \<lesssim> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s \<lesssim> u; t \<lesssim> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
overlapping s t

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s \<lesssim> u; t \<lesssim> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding overlapping_def
[PROOF STATE]
proof (prove)
using this:
\<exists>u. s \<lesssim> u \<and> t \<lesssim> u

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s \<lesssim> u; t \<lesssim> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma rewrite_firstE:
  assumes "rewrite_first cs t t'"
  obtains pat rhs env where "(pat, rhs) \<in> set cs" "match pat t = Some env" "t' = subst rhs env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pat rhs env. \<lbrakk>(pat, rhs) \<in> set cs; match pat t = Some env; t' = subst rhs env\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rewrite_first cs t t'

goal (1 subgoal):
 1. (\<And>pat rhs env. \<lbrakk>(pat, rhs) \<in> set cs; match pat t = Some env; t' = subst rhs env\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by induction auto


[STATEMENT]
lemma find_match_rewrite_first:
  assumes "find_match cs t = Some (env, pat, rhs)"
  shows "rewrite_first cs t (subst rhs env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rewrite_first cs t (subst rhs env)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
find_match cs t = Some (env, pat, rhs)

goal (1 subgoal):
 1. rewrite_first cs t (subst rhs env)
[PROOF STEP]
proof (induction cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. find_match [] t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first [] t (subst rhs env)
 2. \<And>a cs. \<lbrakk>find_match cs t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first cs t (subst rhs env); find_match (a # cs) t = Some (env, pat, rhs)\<rbrakk> \<Longrightarrow> rewrite_first (a # cs) t (subst rhs env)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
find_match cs t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first cs t (subst rhs env)
find_match (c # cs) t = Some (env, pat, rhs)

goal (2 subgoals):
 1. find_match [] t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first [] t (subst rhs env)
 2. \<And>a cs. \<lbrakk>find_match cs t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first cs t (subst rhs env); find_match (a # cs) t = Some (env, pat, rhs)\<rbrakk> \<Longrightarrow> rewrite_first (a # cs) t (subst rhs env)
[PROOF STEP]
obtain pat0 rhs0 where "c = (pat0, rhs0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>pat0 rhs0. c = (pat0, rhs0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
c = (pat0, rhs0)

goal (2 subgoals):
 1. find_match [] t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first [] t (subst rhs env)
 2. \<And>a cs. \<lbrakk>find_match cs t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first cs t (subst rhs env); find_match (a # cs) t = Some (env, pat, rhs)\<rbrakk> \<Longrightarrow> rewrite_first (a # cs) t (subst rhs env)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
c = (pat0, rhs0)

goal (1 subgoal):
 1. rewrite_first (c # cs) t (subst rhs env)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
c = (pat0, rhs0)
find_match cs t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first cs t (subst rhs env)
find_match (c # cs) t = Some (env, pat, rhs)

goal (1 subgoal):
 1. rewrite_first (c # cs) t (subst rhs env)
[PROOF STEP]
by (cases "match pat0 t") (auto intro: rewrite_first.intros)
[PROOF STATE]
proof (state)
this:
rewrite_first (c # cs) t (subst rhs env)

goal (1 subgoal):
 1. find_match [] t = Some (env, pat, rhs) \<Longrightarrow> rewrite_first [] t (subst rhs env)
[PROOF STEP]
qed simp


[STATEMENT]
lemma term_cases_cong[fundef_cong]:
  assumes "t = u" "otherwise1 = otherwise2"
  assumes "(\<And>name. t = const name \<Longrightarrow> if_const1 name = if_const2 name)"
  assumes "(\<And>name. t = free name \<Longrightarrow> if_free1 name = if_free2 name)"
  assumes "(\<And>u\<^sub>1 u\<^sub>2. t = app u\<^sub>1 u\<^sub>2 \<Longrightarrow> if_app1 u\<^sub>1 u\<^sub>2 = if_app2 u\<^sub>1 u\<^sub>2)"
  shows "term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t = u
otherwise1 = otherwise2
t = const ?name \<Longrightarrow> if_const1 ?name = if_const2 ?name
t = free ?name \<Longrightarrow> if_free1 ?name = if_free2 ?name
t = app ?u\<^sub>1 ?u\<^sub>2 \<Longrightarrow> if_app1 ?u\<^sub>1 ?u\<^sub>2 = if_app2 ?u\<^sub>1 ?u\<^sub>2

goal (1 subgoal):
 1. term_cases if_const1 if_free1 if_app1 otherwise1 t = term_cases if_const2 if_free2 if_app2 otherwise2 u
[PROOF STEP]
unfolding term_cases_def
[PROOF STATE]
proof (prove)
using this:
t = u
otherwise1 = otherwise2
t = const ?name \<Longrightarrow> if_const1 ?name = if_const2 ?name
t = free ?name \<Longrightarrow> if_free1 ?name = if_free2 ?name
t = app ?u\<^sub>1 ?u\<^sub>2 \<Longrightarrow> if_app1 ?u\<^sub>1 ?u\<^sub>2 = if_app2 ?u\<^sub>1 ?u\<^sub>2

goal (1 subgoal):
 1. (case unconst t of None \<Rightarrow> case unfree t of None \<Rightarrow> case unapp t of None \<Rightarrow> otherwise1 | Some (xa, xb) \<Rightarrow> if_app1 xa xb | Some x \<Rightarrow> if_free1 x | Some x \<Rightarrow> if_const1 x) = (case unconst u of None \<Rightarrow> case unfree u of None \<Rightarrow> case unapp u of None \<Rightarrow> otherwise2 | Some (xa, xb) \<Rightarrow> if_app2 xa xb | Some x \<Rightarrow> if_free2 x | Some x \<Rightarrow> if_const2 x)
[PROOF STEP]
by (auto split: option.splits)


[STATEMENT]
lemma term_cases[simp]:
  "term_cases if_const if_free if_app otherwise (const name) = if_const name"
  "term_cases if_const if_free if_app otherwise (free name) = if_free name"
  "term_cases if_const if_free if_app otherwise (app t u) = if_app t u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_cases if_const if_free if_app otherwise (const name) = if_const name &&& term_cases if_const if_free if_app otherwise (free name) = if_free name &&& term_cases if_const if_free if_app otherwise (app t u) = if_app t u
[PROOF STEP]
unfolding term_cases_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case unconst (const name) of None \<Rightarrow> case unfree (const name) of None \<Rightarrow> case unapp (const name) of None \<Rightarrow> otherwise | Some (xa, xb) \<Rightarrow> if_app xa xb | Some x \<Rightarrow> if_free x | Some x \<Rightarrow> if_const x) = if_const name &&& (case unconst (free name) of None \<Rightarrow> case unfree (free name) of None \<Rightarrow> case unapp (free name) of None \<Rightarrow> otherwise | Some (xa, xb) \<Rightarrow> if_app xa xb | Some x \<Rightarrow> if_free x | Some x \<Rightarrow> if_const x) = if_free name &&& (case unconst (app t u) of None \<Rightarrow> case unfree (app t u) of None \<Rightarrow> case unapp (app t u) of None \<Rightarrow> otherwise | Some (xa, xb) \<Rightarrow> if_app xa xb | Some x \<Rightarrow> if_free x | Some x \<Rightarrow> if_const x) = if_app t u
[PROOF STEP]
by (auto split: option.splits)


[STATEMENT]
lemma term_cases_template:
  assumes "\<And>x. f x = term_cases if_const if_free if_app otherwise x"
  shows "f (const name) = if_const name"
    and "f (free name) = if_free name"
    and "f (app t u) = if_app t u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (const name) = if_const name &&& f (free name) = if_free name &&& f (app t u) = if_app t u
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_cases if_const if_free if_app otherwise (const name) = if_const name &&& term_cases if_const if_free if_app otherwise (free name) = if_free name &&& term_cases if_const if_free if_app otherwise (app t u) = if_app t u
[PROOF STEP]
by (rule term_cases)+


[STATEMENT]
lemma strip_comb_simps[simp]:
  "strip_comb (app t u) = (let (f, args) = strip_comb t in (f, args @ [u]))"
  "unapp t = None \<Longrightarrow> strip_comb t = (t, [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_comb (app t u) = (let (f, args) = strip_comb t in (f, args @ [u])) &&& (unapp t = None \<Longrightarrow> strip_comb t = (t, []))
[PROOF STEP]
by (subst strip_comb.simps; auto)+


[STATEMENT]
lemma strip_comb_induct[case_names app no_app]:
  assumes "\<And>x y. P x \<Longrightarrow> P (app x y)"
  assumes "\<And>t. unapp t = None \<Longrightarrow> P t"
  shows "P t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t
[PROOF STEP]
proof (rule strip_comb.induct, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. (\<And>x2 x y. \<lbrakk>unapp t = Some x2; (x, y) = x2\<rbrakk> \<Longrightarrow> P x) \<Longrightarrow> P t
[PROOF STEP]
case (1 t)
[PROOF STATE]
proof (state)
this:
\<lbrakk>unapp t = Some ?x2.0; (?x, ?y) = ?x2.0\<rbrakk> \<Longrightarrow> P ?x

goal (1 subgoal):
 1. \<And>t. (\<And>x2 x y. \<lbrakk>unapp t = Some x2; (x, y) = x2\<rbrakk> \<Longrightarrow> P x) \<Longrightarrow> P t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t
[PROOF STEP]
proof (cases "unapp t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. unapp t = None \<Longrightarrow> P t
 2. \<And>a. unapp t = Some a \<Longrightarrow> P t
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
unapp t = None

goal (2 subgoals):
 1. unapp t = None \<Longrightarrow> P t
 2. \<And>a. unapp t = Some a \<Longrightarrow> P t
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
P ?x \<Longrightarrow> P (app ?x ?y)
unapp ?t = None \<Longrightarrow> P ?t
unapp t = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P ?x \<Longrightarrow> P (app ?x ?y)
unapp ?t = None \<Longrightarrow> P ?t
unapp t = None

goal (1 subgoal):
 1. P t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
P t

goal (1 subgoal):
 1. \<And>a. unapp t = Some a \<Longrightarrow> P t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. unapp t = Some a \<Longrightarrow> P t
[PROOF STEP]
case (Some a)
[PROOF STATE]
proof (state)
this:
unapp t = Some a

goal (1 subgoal):
 1. \<And>a. unapp t = Some a \<Longrightarrow> P t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
unapp t = Some a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unapp t = Some a

goal (1 subgoal):
 1. P t
[PROOF STEP]
apply (cases a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>unapp t = Some a; a = (aa, b)\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
using 1 assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>unapp t = Some ?x2.0; (?x, ?y) = ?x2.0\<rbrakk> \<Longrightarrow> P ?x
P ?x \<Longrightarrow> P (app ?x ?y)
unapp ?t = None \<Longrightarrow> P ?t

goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>unapp t = Some a; a = (aa, b)\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sstrip_comb_termination[termination_simp]:
  "(f, ts) = strip_comb t \<Longrightarrow> t' \<in> set ts \<Longrightarrow> size t' < size t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(f, ts) = strip_comb t; t' \<in> set ts\<rbrakk> \<Longrightarrow> size t' < size t
[PROOF STEP]
by (metis snd_conv strip_comb_size)


[STATEMENT]
lemma strip_comb_empty: "snd (strip_comb t) = [] \<Longrightarrow> fst (strip_comb t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (strip_comb t) = [] \<Longrightarrow> fst (strip_comb t) = t
[PROOF STEP]
by (induction t rule: strip_comb_induct) (auto split: prod.splits)


[STATEMENT]
lemma strip_comb_app: "fst (strip_comb (app t u)) = fst (strip_comb t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (strip_comb (app t u)) = fst (strip_comb t)
[PROOF STEP]
by (simp split: prod.splits)


[STATEMENT]
lemma list_comb_app[simp]: "list_comb f (xs @ ys) = list_comb (list_comb f xs) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_comb f (xs @ ys) = list_comb (list_comb f xs) ys
[PROOF STEP]
by (induct xs arbitrary: f) auto


[STATEMENT]
lemma list_comb_size[simp]: "size (list_comb f xs) = size f + size_list size xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size (list_comb f xs) = size f + size_list size xs
[PROOF STEP]
by (induct xs arbitrary: f) auto


[STATEMENT]
lemma subst_list_comb: "subst (list_comb f xs) env = list_comb (subst f env) (map (\<lambda>t. subst t env) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subst (list_comb f xs) env = list_comb (subst f env) (map (\<lambda>t. subst t env) xs)
[PROOF STEP]
by (induct xs arbitrary: f) auto


[STATEMENT]
lemma list_strip_comb[simp]: "list_comb (fst (strip_comb t)) (snd (strip_comb t)) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_comb (fst (strip_comb t)) (snd (strip_comb t)) = t
[PROOF STEP]
by (induction t rule: strip_comb_induct) (auto split: prod.splits)


[STATEMENT]
lemma strip_list_comb: "strip_comb (list_comb f ys) = (fst (strip_comb f), snd (strip_comb f) @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_comb (list_comb f ys) = (fst (strip_comb f), snd (strip_comb f) @ ys)
[PROOF STEP]
by (induct ys arbitrary: f) (auto simp: split_beta)


[STATEMENT]
lemma strip_list_comb_const: "strip_comb (name $$ xs) = (const name, xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip_comb (name $$ xs) = (const name, xs)
[PROOF STEP]
by (simp add: strip_list_comb)


[STATEMENT]
lemma frees_list_comb[simp]: "frees (list_comb t xs) = frees t |\<union>| freess xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees (list_comb t xs) = frees t |\<union>| freess xs
[PROOF STEP]
by (induct xs arbitrary: t) (auto simp: freess_def)


[STATEMENT]
lemma consts_list_comb: "consts (list_comb f xs) = consts f |\<union>| ffUnion (fset_of_list (map consts xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consts (list_comb f xs) = consts f |\<union>| ffUnion (fset_of_list (map consts xs))
[PROOF STEP]
by (induct xs arbitrary: f) auto


[STATEMENT]
lemma ids_list_comb: "ids (list_comb f xs) = ids f |\<union>| ffUnion (fset_of_list (map ids xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ids (list_comb f xs) = ids f |\<union>| ffUnion (fset_of_list (map ids xs))
[PROOF STEP]
unfolding ids_def frees_list_comb consts_list_comb freess_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees f |\<union>| (ffUnion \<circ> fset_of_list \<circ> map frees) xs |\<union>| (consts f |\<union>| ffUnion (fset_of_list (map consts xs))) = frees f |\<union>| consts f |\<union>| ffUnion (fset_of_list (map (\<lambda>t. frees t |\<union>| consts t) xs))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x |\<notin>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs); x |\<notin>| consts f; x |\<in>| ffUnion (frees |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
 2. \<And>x. \<lbrakk>x |\<notin>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs); x |\<notin>| consts f; x |\<in>| ffUnion (consts |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
 3. \<And>x. \<lbrakk>x |\<notin>| ffUnion (consts |`| fset_of_list xs); x |\<notin>| consts f; x |\<notin>| ffUnion (frees |`| fset_of_list xs); x |\<in>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
[PROOF STEP]
apply (smt fbind_iff finsert_absorb finsert_fsubset funion_image_bind_eq inf_sup_ord(3))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x |\<notin>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs); x |\<notin>| consts f; x |\<in>| ffUnion (consts |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
 2. \<And>x. \<lbrakk>x |\<notin>| ffUnion (consts |`| fset_of_list xs); x |\<notin>| consts f; x |\<notin>| ffUnion (frees |`| fset_of_list xs); x |\<in>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
[PROOF STEP]
apply (metis fbind_iff funionCI funion_image_bind_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x |\<notin>| ffUnion (consts |`| fset_of_list xs); x |\<notin>| consts f; x |\<notin>| ffUnion (frees |`| fset_of_list xs); x |\<in>| ffUnion ((\<lambda>t. frees t |\<union>| consts t) |`| fset_of_list xs)\<rbrakk> \<Longrightarrow> x |\<in>| frees f
[PROOF STEP]
by (smt fbind_iff funionE funion_image_bind_eq)


[STATEMENT]
lemma frees_strip_comb: "frees t = frees (fst (strip_comb t)) |\<union>| freess (snd (strip_comb t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frees t = frees (fst (strip_comb t)) |\<union>| freess (snd (strip_comb t))
[PROOF STEP]
by (metis list_strip_comb frees_list_comb)


[STATEMENT]
lemma list_comb_cases':
  obtains (app) "is_app (list_comb f xs)"
        | (empty) "list_comb f xs = f" "xs = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_app (list_comb f xs) \<Longrightarrow> thesis; \<lbrakk>list_comb f xs = f; xs = []\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (induction xs arbitrary: f) auto


[STATEMENT]
lemma list_comb_cases[consumes 1]:
  assumes "t = list_comb f xs"
  obtains (head) "t = f" "xs = []"
        | (app) u v where "t = app u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>t = f; xs = []\<rbrakk> \<Longrightarrow> thesis; \<And>u v. t = app u v \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t = list_comb f xs

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>t = f; xs = []\<rbrakk> \<Longrightarrow> thesis; \<And>u v. t = app u v \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis list_comb_cases' left_right_simps(3))


[STATEMENT]
lemma list_comb_nesting[simp]: "left_nesting (list_comb f xs) = left_nesting f + length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. left_nesting (list_comb f xs) = left_nesting f + length xs
[PROOF STEP]
by (induct xs arbitrary: f) auto