From a451ccc35fca39a0a73aaec2f1873c0acb6208d4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jan=20van=20Br=C3=BCgge?= <supermanitu@gmail.com>
Date: Sun, 14 Feb 2021 20:04:38 +0100
Subject: [PATCH] Adjust Lemmas

---
 Lemmas.thy | 185 +++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 152 insertions(+), 33 deletions(-)

diff --git a/Lemmas.thy b/Lemmas.thy
index b520a3a..0b8d7b0 100644
--- a/Lemmas.thy
+++ b/Lemmas.thy
@@ -2,31 +2,104 @@ theory Lemmas
   imports Syntax Defs
 begin
 
+lemma fresh_match_Pair:
+  fixes tys::"tyvar list" and vals::"var list"
+  assumes "set (map atom tys) \<sharp>* e" "set (map atom vals) \<sharp>* e" "set (map atom tys) \<sharp>* y"  "set (map atom vals) \<sharp>* y"
+  shows "set (map atom tys @ map atom vals) \<sharp>* (e, y)"
+  by (metis assms fresh_star_Pair fresh_star_Un set_append)
+
+lemma fresh_in_match_var:
+  fixes x::"var"
+  assumes "set (map atom tys) \<sharp>* x" "set (map atom vals) \<sharp>* x" "atom x \<sharp> MatchCtor D tys vals e"
+  shows "atom x \<sharp> e"
+  using assms fresh_at_base(2) fresh_star_Un fresh_star_def by fastforce
+
+lemma fresh_in_match_tyvar:
+  fixes a::"tyvar"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "atom a \<sharp> MatchCtor D tys vals e"
+  shows "atom a \<sharp> e"
+  using assms fresh_at_base(2) fresh_star_Un fresh_star_def by fastforce
+lemmas fresh_in_match = fresh_in_match_var fresh_in_match_tyvar
+
+lemma fresh_star_invert: "set (map atom xs) \<sharp>* a \<Longrightarrow> atom a \<sharp> xs"
+  unfolding fresh_star_def by (induction xs) (auto simp: fresh_Cons fresh_Nil fresh_at_base(2))
+
+lemma match_ctor_eqvt_var:
+  fixes a c::"var"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "set (map atom tys) \<sharp>* c" "set (map atom vals) \<sharp>* c"
+  shows "(a \<leftrightarrow> c) \<bullet> MatchCtor D tys vals e = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)"
+proof -
+  from assms(1,3) have 1: "(a \<leftrightarrow> c) \<bullet> tys = tys" using fresh_star_invert flip_fresh_fresh by blast
+  from assms(2,4) have 2: "(a \<leftrightarrow> c) \<bullet> vals = vals" using fresh_star_invert flip_fresh_fresh by blast
+  from 1 2 show ?thesis by auto
+qed
+
+lemma match_ctor_eqvt_tyvar:
+  fixes a c::"tyvar"
+  assumes "set (map atom tys) \<sharp>* a" "set (map atom vals) \<sharp>* a" "set (map atom tys) \<sharp>* c" "set (map atom vals) \<sharp>* c"
+  shows "(a \<leftrightarrow> c) \<bullet> MatchCtor D tys vals e = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)"
+proof -
+  from assms(1,3) have 1: "(a \<leftrightarrow> c) \<bullet> tys = tys" using fresh_star_invert flip_fresh_fresh by blast
+  from assms(2,4) have 2: "(a \<leftrightarrow> c) \<bullet> vals = vals" using fresh_star_invert flip_fresh_fresh by blast
+  from 1 2 show ?thesis by auto
+qed
+lemmas match_ctor_eqvt = match_ctor_eqvt_var match_ctor_eqvt_tyvar
+
 (* \<lbrakk> atom x \<sharp> t' ; x = y \<or> atom x \<sharp> t \<rbrakk> \<Longrightarrow> atom x \<sharp> t[t'/y] *)
-lemma fresh_subst_term: "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> e \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_term e e' y"
-  by (nominal_induct e avoiding: x y e' rule: term.strong_induct) auto
-lemma fresh_subst_term_tyvar: "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term e e' y"
-  by (nominal_induct e avoiding: y a e' rule: term.strong_induct) auto
+lemma fresh_subst_term:
+  shows "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> e \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_term e e' y"
+  and "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> alts \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_alt_list alts e' y"
+  and "\<lbrakk> atom x \<sharp> e' ; x = y \<or> atom x \<sharp> alt \<rbrakk> \<Longrightarrow> atom x \<sharp> subst_alt alt e' y"
+proof (nominal_induct e and alts and alt avoiding: x y e' rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom x \<sharp> e[e'/y]" using fresh_in_match(1) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed auto
+lemma fresh_subst_term_tyvar:
+  shows "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term e e' y"
+  and "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> alts \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_list alts e' y"
+  and "\<lbrakk> atom (a::tyvar) \<sharp> e' ; atom a \<sharp> alt \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt alt e' y"
+proof (nominal_induct e and alts and alt avoiding: a y e' rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom a \<sharp> e[e'/y]" using fresh_in_match(2) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed auto
 lemma fresh_subst_type: "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> \<sigma> \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_type \<sigma> \<tau> b"
   by (nominal_induct \<sigma> avoiding: a b \<tau> rule: \<tau>.strong_induct) auto
-lemma fresh_subst_term_type: "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term_type e \<tau> b"
-  by (nominal_induct e avoiding: a b \<tau> rule: term.strong_induct) (auto simp: fresh_subst_type)
+lemma fresh_subst_term_type:
+  shows "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> e \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_term_type e \<tau> b"
+  and "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> alts \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_list_type alts \<tau> b"
+  and "\<lbrakk> atom a \<sharp> \<tau> ; a = b \<or> atom a \<sharp> alt \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_alt_type alt \<tau> b"
+proof (nominal_induct e and alts and alt avoiding: a b \<tau> rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  then have "atom a \<sharp> e[\<tau>/b]" using fresh_in_match(2) by blast
+  then show ?case using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+qed (auto simp: fresh_subst_type)
 lemma fresh_subst_context_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> atom (x::var) \<sharp> subst_context \<Gamma> \<tau>' a"
   by (induction \<Gamma> \<tau>' a rule: subst_context.induct) (auto simp: fresh_Cons)
 lemma fresh_subst_context_tyvar: "\<lbrakk> atom a \<sharp> \<tau>' ; a = b \<or> atom a \<sharp> \<Gamma> \<rbrakk> \<Longrightarrow> atom a \<sharp> subst_context \<Gamma> \<tau>' b"
   by (induction \<Gamma> \<tau>' a rule: subst_context.induct) (auto simp: fresh_Cons fresh_Nil fresh_subst_type)
-lemmas fresh_subst = fresh_subst_term fresh_subst_term_tyvar fresh_subst_type fresh_subst_term_type fresh_subst_context_var fresh_subst_context_tyvar
+lemmas fresh_subst = fresh_subst_term(1) fresh_subst_term_tyvar(1) fresh_subst_type fresh_subst_term_type(1) fresh_subst_context_var fresh_subst_context_tyvar fresh_subst_term(2,3) fresh_subst_term_tyvar(2,3) fresh_subst_term_type(2,3)
 
 (* atom c \<sharp> t \<Longrightarrow> t[t'/x] = ((x \<leftrightarrow> c) \<bullet> t)[t'/c] *)
-lemma subst_term_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term e e' x = subst_term ((x \<leftrightarrow> c) \<bullet> e) e' c"
-proof (nominal_induct e avoiding: c x e' rule: term.strong_induct)
+lemma subst_term_var_name:
+  shows "atom c \<sharp> e \<Longrightarrow> subst_term e e' x = subst_term ((x \<leftrightarrow> c) \<bullet> e) e' c"
+  and "atom c \<sharp> alts \<Longrightarrow> subst_alt_list alts e' x = subst_alt_list ((x \<leftrightarrow> c) \<bullet> alts) e' c"
+  and "atom c \<sharp> alt \<Longrightarrow> subst_alt alt e' x = subst_alt ((x \<leftrightarrow> c) \<bullet> alt) e' c"
+proof (nominal_induct e and alts and alt avoiding: c x e' rule: term_alt_list_alt.strong_induct)
   case (Let y \<tau> e1 e2)
   then have "(Let y \<tau> e1 e2)[e'/x] = Let y \<tau> e1[e'/x] e2[e'/x]" by auto
   also have "... = Let y \<tau> ((x \<leftrightarrow> c) \<bullet> e1)[e'/c] ((x \<leftrightarrow> c) \<bullet> e2)[e'/c]"
-    by (metis Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(7))
+    by (metis Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(7))
   also have "... = (Let y \<tau> ((x \<leftrightarrow> c) \<bullet> e1) ((x \<leftrightarrow> c) \<bullet> e2))[e'/c]" by (simp add: Let.hyps(1) Let.hyps(3))
   finally show ?case
-    by (metis Let.hyps(1) Let.hyps(2) flip_fresh_fresh fresh_at_base(2) no_vars_in_ty term.perm_simps(7))
+    by (metis Let.hyps(1) Let.hyps(2) flip_fresh_fresh fresh_at_base(2) no_vars_in_ty term_alt_list_alt.perm_simps(7))
+next
+  case (MatchCtor D tys vals e)
+  from MatchCtor have "(MatchCtor D tys vals e)[e'/x] = MatchCtor D tys vals e[e'/x]" using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by auto
+  also have "... = MatchCtor D tys vals ((x \<leftrightarrow> c) \<bullet> e)[e'/c]" using fresh_in_match(1) MatchCtor by metis
+  also have "... = (MatchCtor D tys vals ((x \<leftrightarrow> c) \<bullet> e))[e'/c]" using fresh_match_Pair[OF MatchCtor(3,6,1,4)] by simp
+  finally show ?case using match_ctor_eqvt(1)[OF MatchCtor(2,5,1,4)] by presburger
 qed (auto simp: flip_fresh_fresh fresh_at_base)
 
 lemma subst_type_var_name: "atom c \<sharp> \<sigma> \<Longrightarrow> subst_type \<sigma> \<tau> a = subst_type ((a \<leftrightarrow> c) \<bullet> \<sigma>) \<tau> c"
@@ -38,12 +111,15 @@ proof (nominal_induct \<sigma> avoiding: c a \<tau> rule: \<tau>.strong_induct)
   finally show ?case by (metis TyForall.hyps(1) TyForall.hyps(2) \<tau>.perm_simps(5) flip_fresh_fresh fresh_at_base(2) no_tyvars_in_kinds)
 qed (auto simp: fresh_at_base)
 
-lemma subst_term_type_var_name: "atom c \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type ((a \<leftrightarrow> c) \<bullet> e) \<tau> c"
-proof (nominal_induct e avoiding: c a \<tau> rule: term.strong_induct)
+lemma subst_term_type_var_name:
+  shows "atom c \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type ((a \<leftrightarrow> c) \<bullet> e) \<tau> c"
+  and "atom c \<sharp> alts \<Longrightarrow> subst_alt_list_type alts \<tau> a = subst_alt_list_type ((a \<leftrightarrow> c) \<bullet> alts) \<tau> c"
+  and "atom c \<sharp> alt \<Longrightarrow> subst_alt_type alt \<tau> a = subst_alt_type ((a \<leftrightarrow> c) \<bullet> alt) \<tau> c"
+proof (nominal_induct e and alts and alt avoiding: c a \<tau> rule: term_alt_list_alt.strong_induct)
   case (Lam x \<tau>1 e)
   then have "(\<lambda> x:\<tau>1. e)[\<tau>/a] = (\<lambda> x:\<tau>1[\<tau>/a]. e[\<tau>/a])" by simp
   also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. e[\<tau>/a])" using subst_type_var_name Lam by force
-  also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c])" using Lam by (metis fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(5))
+  also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c]. ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c])" using Lam by (metis fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(5))
   also have "... = (\<lambda> x:((a \<leftrightarrow> c) \<bullet> \<tau>1). ((a \<leftrightarrow> c) \<bullet> e))[\<tau>/c]" by simp
   finally show ?case by (simp add: Lam.hyps(2) flip_fresh_fresh)
 next
@@ -51,11 +127,16 @@ next
   then have "(Let x \<tau>1 e1 e2)[\<tau>/a] = Let x \<tau>1[\<tau>/a] e1[\<tau>/a] e2[\<tau>/a]" by simp
   also have "... = Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c] e1[\<tau>/a] e2[\<tau>/a]" using subst_type_var_name Let by auto
   also have "... = Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1)[\<tau>/c] ((a \<leftrightarrow> c) \<bullet> e1)[\<tau>/c] ((a \<leftrightarrow> c) \<bullet> e2)[\<tau>/c]"
-    by (metis (mono_tags, lifting) Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term.fresh(7))
+    by (metis (mono_tags, lifting) Let.hyps(1) Let.hyps(4) Let.hyps(5) Let.prems fresh_at_base(2) list.set(1) list.set(2) singletonD term_alt_list_alt.fresh(7))
   also have "... = (Let x ((a \<leftrightarrow> c) \<bullet> \<tau>1) ((a \<leftrightarrow> c) \<bullet> e1) ((a \<leftrightarrow> c) \<bullet> e2))[\<tau>/c]" by simp
   finally show ?case by (simp add: flip_fresh_fresh)
+next
+  case (MatchCtor D tys vals e)
+  have "(MatchCtor D tys vals e)[\<tau>/a] = MatchCtor D tys vals e[\<tau>/a]" using fresh_match_Pair[OF MatchCtor(3,6,2,5)] by simp
+  also have "... = MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e)[\<tau>/c]" using fresh_in_match(2) MatchCtor by metis
+  also have "... = (MatchCtor D tys vals ((a \<leftrightarrow> c) \<bullet> e))[\<tau>/c]" using fresh_match_Pair[OF MatchCtor(3,6,1,4)] by simp
+  finally show ?case using match_ctor_eqvt(2)[OF MatchCtor(2,5,1,4)] by presburger
 qed (auto simp: flip_fresh_fresh fresh_at_base subst_type_var_name)
-lemmas subst_var_name = subst_term_var_name subst_type_var_name subst_term_type_var_name
 
 lemma subst_context_var_name: "atom c \<sharp> \<Gamma> \<Longrightarrow> subst_context \<Gamma> \<tau> a = subst_context ((a \<leftrightarrow> c) \<bullet> \<Gamma>) \<tau> c"
 proof (induction \<Gamma> \<tau> a rule: subst_context.induct)
@@ -74,14 +155,15 @@ proof (induction \<Gamma> \<tau> a rule: subst_context.induct)
     show ?thesis using a b c 1 by argo
   qed
 qed (auto simp: flip_fresh_fresh fresh_Cons subst_type_var_name)
+lemmas subst_var_name = subst_term_var_name(1) subst_type_var_name subst_term_type_var_name(1) subst_context_var_name subst_term_var_name(2,3) subst_term_type_var_name(2,3)
 
 (* [[atom a]]lst. t = [[atom a2]]lst. t2 \<Longrightarrow> subst t t' a = subst t2 t' a2 *)
 lemma subst_term_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term e t a = subst_term e' t a'"
-  by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name)
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_var_name(1))
 lemma subst_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_type e \<tau> a = subst_type e' \<tau> a'"
   by (metis Abs1_eq_iff(3) flip_commute subst_type_var_name)
 lemma subst_term_type_same: "[[atom a]]lst. e = [[atom a']]lst. e' \<Longrightarrow> subst_term_type e \<tau> a = subst_term_type e' \<tau> a'"
-  by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name)
+  by (metis Abs1_eq_iff(3) flip_commute subst_term_type_var_name(1))
 lemmas subst_same = subst_term_same subst_type_same subst_term_type_same
 
 (* atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin (B x _) \<Gamma> *)
@@ -93,13 +175,23 @@ lemma fresh_not_isin_var: "atom x \<sharp> \<Gamma> \<Longrightarrow> \<not>isin
   by (metis (mono_tags, lifting) binder.fresh(1) binder.strong_exhaust fresh_Cons fresh_at_base(2) isin.simps(2) isin.simps(3))
 
 (* atom x \<sharp> t \<Longrightarrow> subst t' x t = t *)
-lemma fresh_subst_term_same: "atom x \<sharp> e \<Longrightarrow> subst_term e e' x = e"
-proof (induction e e' x rule: subst_term.induct)
-  case (5 y e x \<tau> e2)
+lemma fresh_subst_term_same:
+  shows "atom x \<sharp> e \<Longrightarrow> subst_term e e' x = e"
+  and "atom x \<sharp> alts \<Longrightarrow> subst_alt_list alts e' x = alts"
+  and "atom x \<sharp> alt \<Longrightarrow> subst_alt alt e' x = alt"
+proof (induction e e' x and alts e' x and alt e' x rule: subst_term_subst_alt_list_subst_alt.induct)
+  case (6 y e x \<tau> e2)
   then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
 next
-  case (7 y e x \<tau> e1 e2)
+  case (8 y e x \<tau> e1 e2)
   then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
+next
+  case (11 y e x t)
+  then show ?case using fresh_PairD(2) fresh_at_base(2) by fastforce
+next
+  case (12 tys vals e x D t)
+  then have "atom x \<sharp> t" by (meson fresh_PairD(2) fresh_at_base(2) fresh_star_def term_alt_list_alt.fresh(11))
+  then show ?case using 12 by simp
 qed auto
 
 lemma fresh_subst_type_same: "atom a \<sharp> \<sigma> \<Longrightarrow> subst_type \<sigma> \<tau> a = \<sigma>"
@@ -109,33 +201,60 @@ proof (induction \<sigma> \<tau> a rule: subst_type.induct)
     using fresh_Pair fresh_at_base(2) fresh_def list.set(1) list.set(2) subst_type.simps(4) by fastforce
 qed auto
 
-lemma fresh_subst_term_type_same: "atom a \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = e"
-proof (induction e \<tau> a rule: subst_term_type.induct)
-  case (6 b \<tau> a k e2)
-  then show ?case by (simp add: "6.hyps" fresh_Pair fresh_at_base(2))
+lemma fresh_subst_term_type_same:
+  shows "atom a \<sharp> e \<Longrightarrow> subst_term_type e \<tau> a = e"
+  and "atom a \<sharp> alts \<Longrightarrow> subst_alt_list_type alts \<tau> a = alts"
+  and "atom a \<sharp> alt \<Longrightarrow> subst_alt_type alt \<tau> a = alt"
+proof (induction e \<tau> a and alts \<tau> a and alt \<tau> a rule: subst_term_type_subst_alt_list_type_subst_alt_type.induct)
+  case (7 b \<tau> a k e2)
+  then show ?case by (simp add: "7.hyps" fresh_Pair fresh_at_base(2))
+next
+  case (12 tys vals \<tau> a D e)
+  then have "atom a \<sharp> e" by (meson fresh_PairD(2) fresh_at_base(2) fresh_star_def term_alt_list_alt.fresh(11))
+  then show ?case using 12 by auto
 qed (auto simp: fresh_subst_type_same)
 
 lemma fresh_subst_context_same: "atom a \<sharp> \<Gamma> \<Longrightarrow> subst_context \<Gamma> \<tau> a = \<Gamma>"
   by (induction \<Gamma> \<tau> a rule: subst_context.induct) (auto simp: fresh_Cons fresh_subst_type_same)
 
-lemmas fresh_subst_same = fresh_subst_term_same fresh_subst_type_same fresh_subst_term_type_same fresh_subst_context_same
+lemmas fresh_subst_same = fresh_subst_term_same(1) fresh_subst_type_same fresh_subst_term_type_same(1) fresh_subst_context_same fresh_subst_term_same(2,3) fresh_subst_term_type_same(2,3)
 
 (* \<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst (subst e t2 x) t1 y = subst (subst e t1 y) (subst t2 t1 y) x *)
-lemma subst_subst_term: "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_term (subst_term e t2 x) t1 y = subst_term (subst_term e t1 y) (subst_term t2 t1 y) x"
-  by (nominal_induct e avoiding: x y t1 t2 rule: term.strong_induct) (auto simp: fresh_subst_same fresh_subst)
+lemma subst_subst_term:
+  shows "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_term (subst_term e t2 x) t1 y = subst_term (subst_term e t1 y) (subst_term t2 t1 y) x"
+  and "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_alt_list (subst_alt_list alts t2 x) t1 y = subst_alt_list (subst_alt_list alts t1 y) (subst_term t2 t1 y) x"
+  and "\<lbrakk> x \<noteq> y ; atom x \<sharp> t1 \<rbrakk> \<Longrightarrow> subst_alt (subst_alt alt t2 x) t1 y = subst_alt (subst_alt alt t1 y) (subst_term t2 t1 y) x"
+proof (nominal_induct e and alts and alt avoiding: x y t1 t2 rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  have 1: "set (map atom tys) \<sharp>* t2[t1/y]" unfolding fresh_star_def using fresh_subst(2) by (metis MatchCtor(3,4) ex_map_conv fresh_star_def)
+  have 2: "set (map atom vals) \<sharp>* t2[t1/y]" unfolding fresh_star_def using fresh_subst(1) by (metis MatchCtor(7,8) ex_map_conv fresh_star_def)
+  have "(MatchCtor D tys vals e)[t2/x][t1/y] = MatchCtor D tys vals e[t2/x][t1/y]" using fresh_match_Pair[OF MatchCtor(4,8,1,5)] fresh_match_Pair[OF MatchCtor(3,7,2,6)] by simp
+  also have "... = MatchCtor D tys vals e[t1/y][t2[t1/y]/x]" using MatchCtor by simp
+  finally show ?case using fresh_match_Pair[OF MatchCtor(3,7,2,6)] fresh_match_Pair[OF 1 2 MatchCtor(1,5)] by simp
+qed (auto simp: fresh_subst_same fresh_subst)
 lemma subst_subst_type: "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_type (subst_type \<sigma> \<tau>2 a) \<tau>1 b = subst_type (subst_type \<sigma> \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
   by (nominal_induct \<sigma> avoiding: a b \<tau>1 \<tau>2 rule: \<tau>.strong_induct) (auto simp: fresh_subst_same fresh_subst)
-lemma subst_subst_term_type: "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_term_type (subst_term_type e \<tau>2 a) \<tau>1 b = subst_term_type (subst_term_type e \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
-  by (nominal_induct e avoiding: a b \<tau>1 \<tau>2 rule: term.strong_induct) (auto simp: fresh_subst_same fresh_subst subst_subst_type)
+lemma subst_subst_term_type:
+  shows "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_term_type (subst_term_type e \<tau>2 a) \<tau>1 b = subst_term_type (subst_term_type e \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+  and "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_alt_list_type (subst_alt_list_type alts \<tau>2 a) \<tau>1 b = subst_alt_list_type (subst_alt_list_type alts \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+  and "\<lbrakk> a \<noteq> b ; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_alt_type (subst_alt_type alt \<tau>2 a) \<tau>1 b = subst_alt_type (subst_alt_type alt \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
+proof (nominal_induct e and alts and alt avoiding: a b \<tau>1 \<tau>2 rule: term_alt_list_alt.strong_induct)
+  case (MatchCtor D tys vals e)
+  have 1: "set (map atom tys) \<sharp>* \<tau>2[\<tau>1/b]" unfolding fresh_star_def using fresh_subst(3) by (metis MatchCtor(3,4) ex_map_conv fresh_star_def)
+  have 2: "set (map atom vals) \<sharp>* \<tau>2[\<tau>1/b]" unfolding fresh_star_def by simp
+  have "(MatchCtor D tys vals e)[\<tau>2/a][\<tau>1/b] = MatchCtor D tys vals e[\<tau>2/a][\<tau>1/b]" using fresh_match_Pair[OF MatchCtor(4,8,1,5)] fresh_match_Pair[OF MatchCtor(3,7,2,6)] by simp
+  also have "... = MatchCtor D tys vals e[\<tau>1/b][\<tau>2[\<tau>1/b]/a]" using MatchCtor by simp
+  finally show ?case using fresh_match_Pair[OF MatchCtor(3,7,2,6)] fresh_match_Pair[OF 1 2 MatchCtor(1,5)] by simp
+qed (auto simp: fresh_subst_same fresh_subst subst_subst_type)
 lemma subst_subst_context: "\<lbrakk> a \<noteq> b; atom a \<sharp> \<tau>1 \<rbrakk> \<Longrightarrow> subst_context (subst_context \<Gamma> \<tau>2 a) \<tau>1 b = subst_context (subst_context \<Gamma> \<tau>1 b) (subst_type \<tau>2 \<tau>1 b) a"
   by (induction \<Gamma> \<tau>2 a rule: subst_context.induct) (auto simp: subst_subst_type)
-lemmas subst_subst = subst_subst_term subst_subst_type subst_subst_term_type subst_subst_context
+lemmas subst_subst = subst_subst_term(1) subst_subst_type subst_subst_term_type(1) subst_subst_context subst_subst_term(2,3) subst_subst_term_type(2,3)
 
 (* misc *)
 lemma fv_supp_subset: "fv_\<tau> \<tau> \<subseteq> supp \<tau>"
   by (induction \<tau> rule: \<tau>.induct) (auto simp: \<tau>.supp \<tau>.fv_defs)
 
 lemma head_ctor_is_value: "head_ctor e \<Longrightarrow> is_value e"
-  by (induction e rule: term.induct) auto
+  by (induction e rule: term_alt_list_alt.inducts(1)) auto
 
 end