# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1721076503 -3600
# Node ID f1872ef41766e0f1440fdf2d7a7e1ba2ad1268c1
# Parent  38c63d4027c489a484608900dfd1af03b41679c2
Revised mixfix and streamlined proofs

diff -r 38c63d4027c4 -r f1872ef41766 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Jul 12 14:18:56 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy	Mon Jul 15 21:48:23 2024 +0100
@@ -50,17 +50,17 @@
 
 nominal_datatype trm = 
     Ax   "name" "coname"
-  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ (_)._" [100,100,100,100] 100)
-  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR (_)._ _" [100,100,100] 100)
-  | NotL "\<guillemotleft>coname\<guillemotright>trm" "name"                 ("NotL <_>._ _" [100,100,100] 100)
-  | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
-  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL1 (_)._ _" [100,100,100] 100)
-  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL2 (_)._ _" [100,100,100] 100)
-  | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR1 <_>._ _" [100,100,100] 100)
-  | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 100)
-  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
-  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 100)
-  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)
+  | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ (_)._" [0,100,1000,100] 101)
+  | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR (_)._ _" [100,100,100] 101)
+  | NotL "\<guillemotleft>coname\<guillemotright>trm" "name"                 ("NotL <_>._ _" [0,100,100] 101)
+  | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [0,100,0,100,100] 101)
+  | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL1 (_)._ _" [100,100,100] 101)
+  | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name"                  ("AndL2 (_)._ _" [100,100,100] 101)
+  | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR1 <_>._ _" [100,100,100] 101)
+  | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 101)
+  | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 101)
+  | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 101)
+  | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 101)
 
 text \<open>named terms\<close>
 
@@ -1319,217 +1319,151 @@
 lemma better_NotL_substn:
   assumes a: "y\<sharp>M"
   shows "(NotL <a>.M y){y:=<c>.P} = fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y")
-apply(auto simp: fresh_left calc_atm forget)
-apply(generate_fresh "name")
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
-done
+proof (generate_fresh "coname")
+  fix ca :: coname
+  assume d: "ca \<sharp> (M, P, a, c, y)"
+  then have "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y"
+    by (metis alpha(2) fresh_prod perm_fresh_fresh(2) trm.inject(4))
+  with a d show ?thesis
+    apply(simp add: fresh_left calc_atm forget)
+    apply (metis trm.inject(4))
+    done
+qed
 
 lemma better_AndL1_substn:
   assumes a: "y\<sharp>[x].M"
   shows "(AndL1 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z')"
-using a
-apply -
-apply(generate_fresh "name")
-apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]\<bullet>M) y")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(generate_fresh "name")
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "name")
+  fix d:: name
+  assume d: "d \<sharp> (M, P, c, x, y)"
+  then have \<section>: "AndL1 (x).M y = AndL1 (d).([(d,x)]\<bullet>M) y"
+    by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(6))
+  with d have "(\<lambda>z'. Cut <c>.P (z').AndL1 (d).([(d, x)] \<bullet> M){x:=<c>.P} (z')) 
+             = (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M (z'))"
+    by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(6))
+  with d have "(\<lambda>z'. Cut <c>.P (z').AndL1 d.([(d, x)] \<bullet> M){y:=<c>.P} z')
+             = (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M (z'))"
+    apply(simp add: trm.inject alpha fresh_prod fresh_atm)
+    by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap)
+  with d \<section> show ?thesis
+    by (simp add: fresh_left calc_atm)
+qed
 
 lemma better_AndL2_substn:
   assumes a: "y\<sharp>[x].M"
   shows "(AndL2 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z')"
-using a
-apply -
-apply(generate_fresh "name")
-apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\<bullet>M) y")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(generate_fresh "name")
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "name")
+  fix d:: name
+  assume d: "d \<sharp> (M, P, c, x, y)"
+  then have \<section>: "AndL2 (x).M y = AndL2 (d).([(d,x)]\<bullet>M) y"
+    by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(7))
+  with d have "(\<lambda>z'. Cut <c>.P (z').AndL2 (d).([(d, x)] \<bullet> M){x:=<c>.P} (z')) 
+             = (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M (z'))"
+    by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(7))
+  with d have "(\<lambda>z'. Cut <c>.P (z').AndL2 d.([(d, x)] \<bullet> M){y:=<c>.P} z')
+             = (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M (z'))"
+    apply(simp add: trm.inject alpha fresh_prod fresh_atm)
+    by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap)
+  with d \<section> show ?thesis
+    by (simp add: fresh_left calc_atm)
+qed
 
 lemma better_AndR_substc:
-  assumes a: "c\<sharp>([a].M,[b].N)"
+  assumes "c\<sharp>([a].M,[b].N)"
   shows "(AndR <a>.M <b>.N c){c:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.M <b>.N a') (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "coname")
-apply(subgoal_tac "AndR <a>.M <b>.N c = AndR <ca>.([(ca,a)]\<bullet>M) <caa>.([(caa,b)]\<bullet>N) c")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule trans)
-apply(rule substc.simps)
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp: fresh_prod fresh_atm)[1]
-apply(simp)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule conjI)
-apply(rule forget)
-apply(auto simp: fresh_left calc_atm abs_fresh)[1]
-apply(rule forget)
-apply(auto simp: fresh_left calc_atm abs_fresh)[1]
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "coname" , generate_fresh "coname")
+  fix d :: coname
+    and e :: coname
+  assume d: "d \<sharp> (M, N, P, a, b, c, z)"
+    and e: "e \<sharp> (M, N, P, a, b, c, z, d)"
+  then have "AndR <a>.M <b>.N c = AndR <d>.([(d,a)]\<bullet>M) <e>.([(e,b)]\<bullet>N) c"
+    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
+  with assms d e show ?thesis
+    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+    by (metis (no_types, opaque_lifting) abs_fresh(2) forget(2) trm.inject(5))
+qed
 
 lemma better_OrL_substn:
-  assumes a: "x\<sharp>([y].M,[z].N)"
+  assumes "x\<sharp>([y].M,[z].N)"
   shows "(OrL (y).M (z).N x){x:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (y).M (z).N z')"
-using a
-apply -
-apply(generate_fresh "name")
-apply(generate_fresh "name")
-apply(subgoal_tac "OrL (y).M (z).N x = OrL (ca).([(ca,y)]\<bullet>M) (caa).([(caa,z)]\<bullet>N) x")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule trans)
-apply(rule substn.simps)
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp: fresh_prod fresh_atm)[1]
-apply(simp)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule conjI)
-apply(rule forget)
-apply(auto simp: fresh_left calc_atm abs_fresh)[1]
-apply(rule forget)
-apply(auto simp: fresh_left calc_atm abs_fresh)[1]
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "name" , generate_fresh "name")
+  fix d :: name
+    and e :: name
+  assume d: "d \<sharp> (M, N, P, c, x, y, z)"
+    and e: "e \<sharp> (M, N, P, c, x, y, z, d)"
+  with assms have "OrL (y).M (z).N x = OrL (d).([(d,y)]\<bullet>M) (e).([(e,z)]\<bullet>N) x"
+    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
+  with assms d e show ?thesis
+    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+    by (metis (no_types, lifting) abs_fresh(1) forget(1) trm.inject(10))
+qed
 
 lemma better_OrR1_substc:
   assumes a: "d\<sharp>[a].M"
   shows "(OrR1 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "coname")
+  fix c :: coname
+  assume c: "c \<sharp> (M, P, a, d, z)"
+  then have "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d"
+    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
+  with assms c show ?thesis
+    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+    by (metis abs_fresh(2) forget(2) trm.inject(8))
+qed
 
 lemma better_OrR2_substc:
   assumes a: "d\<sharp>[a].M"
   shows "(OrR2 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
-apply(auto)
-done
+proof (generate_fresh "coname")
+  fix c :: coname
+  assume c: "c \<sharp> (M, P, a, d, z)"
+  then have "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d"
+    by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto
+  with assms c show ?thesis
+    apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm)
+    by (metis abs_fresh(2) forget(2) trm.inject(9))
+qed
 
 lemma better_ImpR_substc:
-  assumes a: "d\<sharp>[a].M"
+  assumes "d\<sharp>[a].M"
   shows "(ImpR (x).<a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "name")
-apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>M) d")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(rule sym)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
-done
+proof (generate_fresh "coname" , generate_fresh "name")
+  fix c :: coname
+    and c' :: name
+  assume c: "c \<sharp> (M, P, a, d, x, z)"
+    and c': "c' \<sharp> (M, P, a, d, x, z, c)"
+  have \<dagger>: "ImpR (x).<a>.M d = ImpR (c').<c>.([(c,a)]\<bullet>[(c',x)]\<bullet>M) d"
+    apply (rule sym)
+    using c c'
+    apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
+    done
+  with assms c c' have "fresh_fun
+        (\<lambda>a'. Cut <a'>.ImpR (c').<c>.(([(c, a)] \<bullet> [(c', x)] \<bullet> M)){d:=(z).P} a' (z).P)
+      = fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
+    apply(intro arg_cong [where f="fresh_fun"])
+    by(fastforce simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh forget)
+  with assms c c' \<dagger> show ?thesis
+    by (auto simp: fresh_left calc_atm forget abs_fresh)
+qed
 
 lemma better_ImpL_substn:
-  assumes a: "y\<sharp>(M,[x].N)"
+  assumes "y\<sharp>(M,[x].N)"
   shows "(ImpL <a>.M (x).N y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z')"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "name")
-apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y")
-apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
-apply(rule_tac f="fresh_fun" in arg_cong)
-apply(simp add:  fun_eq_iff)
-apply(rule allI)
-apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
-apply(rule forget)
-apply(simp add: fresh_left calc_atm)
-apply(auto)[1]
-apply(rule sym)
-apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
-done
+proof (generate_fresh "coname" , generate_fresh "name")
+  fix ca :: coname
+    and caa :: name
+  assume d: "ca \<sharp> (M, N, P, a, c, x, y)"
+    and e: "caa \<sharp> (M, N, P, a, c, x, y, ca)"
+  have "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y"
+    apply(rule sym)
+    using d e
+    by(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm)
+  with d e assms show ?thesis
+    apply(simp add: fresh_left calc_atm forget abs_fresh)
+    apply(intro arg_cong [where f="fresh_fun"] ext)
+    apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
+    by (metis forget(1) fresh_aux(1) fresh_bij(1) swap_simps(1))
+qed
 
 lemma freshn_after_substc:
   fixes x::"name"
@@ -1556,170 +1490,124 @@
   by (meson assms fresh_def subset_iff supp_subst6)
 
 lemma substn_crename_comm:
-  assumes a: "c\<noteq>a" "c\<noteq>b"
+  assumes "c\<noteq>a" "c\<noteq>b"
   shows "M{x:=<c>.P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{x:=<c>.(P[a\<turnstile>c>b])}"
-using a
-apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
-apply(auto simp: subst_fresh rename_fresh trm.inject)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,x,c)")
-apply(erule exE)
-apply(subgoal_tac "Cut <c>.P (x).Ax x a = Cut <c>.P (x').Ax x' a")
-apply(simp)
-apply(rule trans)
-apply(rule crename.simps)
-apply(simp add: fresh_prod fresh_atm)
-apply(simp)
-apply(simp add: trm.inject)
-apply(simp add: alpha trm.inject calc_atm fresh_atm)
-apply(simp add: trm.inject)
-apply(simp add: alpha trm.inject calc_atm fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm)
-apply(simp)
-apply(simp add: crename_id)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(auto simp: fresh_atm)[1]
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm)
-apply(auto simp: fresh_atm)[1]
-apply(drule crename_ax)
-apply(simp add: fresh_atm)
-apply(simp add: fresh_atm)
-apply(simp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
-                                  trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh subst_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,P[a\<turnstile>c>b],name1,
-                                  trm1[a\<turnstile>c>b]{name2:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{name2:=<c>.P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh subst_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-done
+using assms
+proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    by(auto simp: subst_fresh rename_fresh trm.inject better_crename_Cut fresh_atm)
+next
+  case (Cut coname trm1 name trm2)
+  then show ?case
+    apply(simp add: rename_fresh better_crename_Cut fresh_atm)
+    by (meson crename_ax)
+next
+  case (NotL coname trm name)
+  obtain x'::name where "x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})"
+    by (meson exists_fresh(1) fs_name1)
+  with NotL show ?case
+    apply (simp add: subst_fresh rename_fresh trm.inject)
+    by (force simp: fresh_prod fresh_fun_simp_NotL better_crename_Cut fresh_atm)
+next
+  case (AndL1 name1 trm name2)
+  obtain x'::name where "x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL1 show ?case
+    apply (simp add: subst_fresh rename_fresh trm.inject)
+    apply (force simp: fresh_prod fresh_fun_simp_AndL1 better_crename_Cut fresh_atm)
+    done
+next
+  case (AndL2 name1 trm name2)
+  obtain x'::name where x': "x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})"
+    by (meson exists_fresh(1) fs_name1)
+  with AndL2 show ?case
+    apply (simp add: subst_fresh rename_fresh trm.inject)
+    apply (auto simp: fresh_prod fresh_fun_simp_AndL2 better_crename_Cut fresh_atm)
+    done
+next
+  case (OrL name1 trm1 name2 trm2 name3)
+  obtain x'::name where x': "x'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
+                                  trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})"
+    by (meson exists_fresh(1) fs_name1)
+  with OrL show ?case
+    apply (simp add: subst_fresh rename_fresh trm.inject)
+    apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_OrL better_crename_Cut)
+    done
+  next
+  case (ImpL coname trm1 name1 trm2 name2)
+  obtain x'::name where x': "x'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
+                                  trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})"
+    by (meson exists_fresh(1) fs_name1)
+  with ImpL show ?case
+    apply (simp add: subst_fresh rename_fresh trm.inject)
+    apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_ImpL better_crename_Cut)
+    done
+qed (auto simp: subst_fresh rename_fresh)
+
 
 lemma substc_crename_comm:
-  assumes a: "c\<noteq>a" "c\<noteq>b"
+  assumes "c\<noteq>a" "c\<noteq>b"
   shows "M{c:=(x).P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{c:=(x).(P[a\<turnstile>c>b])}"
-using a
-apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
-apply(auto simp: subst_fresh rename_fresh trm.inject)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(drule crename_ax)
-apply(simp add: fresh_atm)
-apply(simp add: fresh_atm)
-apply(simp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(a,b,trm{coname:=(x).P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{coname:=(x).P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
-                   P,P[a\<turnstile>c>b],x,trm1[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh subst_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
-                         trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
-                         trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
-                         trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})")
-apply(erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR)
-apply(rule trans)
-apply(rule better_crename_Cut)
-apply(simp add: fresh_atm fresh_prod)
-apply(simp add: rename_fresh fresh_atm)
-apply(rule exists_fresh')
-apply(rule fin_supp)
-done
+using assms
+proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
+  case (Ax name coname)
+  then show ?case
+    by(auto simp: subst_fresh rename_fresh trm.inject better_crename_Cut fresh_atm)
+next
+  case (Cut coname trm1 name trm2)
+  then show ?case
+    apply(simp add: rename_fresh  better_crename_Cut)
+    by (meson crename_ax)
+next
+  case (NotR name trm coname)
+  obtain c'::coname where "c'\<sharp>(a,b,trm{coname:=(x).P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{coname:=(x).P[a\<turnstile>c>b]})"
+    by (meson exists_fresh' fs_coname1)
+  with NotR show ?case
+    apply(simp add: subst_fresh rename_fresh trm.inject)
+    apply(clarsimp simp: fresh_prod)
+    apply(simp add: fresh_fun_simp_NotR)
+    by (simp add: better_crename_Cut fresh_atm(2))
+next
+  case (AndR coname1 trm1 coname2 trm2 coname3)
+  obtain c'::coname where "c'\<sharp>(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
+                   P,P[a\<turnstile>c>b],x,trm1[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]})"
+    by (meson exists_fresh' fs_coname1)
+  with AndR show ?case
+    apply(simp add: subst_fresh rename_fresh trm.inject)
+    apply(clarsimp simp: fresh_prod)
+    apply(simp add: fresh_fun_simp_AndR)
+    by (simp add: better_crename_Cut subst_fresh fresh_atm(2))
+next
+  case (OrR1 coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})"
+    by (meson exists_fresh' fs_coname1)
+  with OrR1 show ?case
+    apply(simp add: subst_fresh rename_fresh trm.inject)
+    apply(clarsimp simp: fresh_prod)
+    apply(simp add: fresh_fun_simp_OrR1)
+    by (simp add: better_crename_Cut fresh_atm(2))
+next
+  case (OrR2 coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})"
+    by (meson exists_fresh' fs_coname1)
+  with OrR2 show ?case
+    apply(simp add: subst_fresh rename_fresh trm.inject)
+    apply(clarsimp simp: fresh_prod)
+    apply(simp add: fresh_fun_simp_OrR2)
+    by (simp add: better_crename_Cut fresh_atm(2))
+next
+  case (ImpR name coname1 trm coname2)
+  obtain c'::coname where "c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>c>b]})"
+    by (meson exists_fresh' fs_coname1)
+  with ImpR show ?case
+    apply(simp add: subst_fresh rename_fresh trm.inject)
+    apply(clarsimp simp: fresh_prod)
+    apply(simp add: fresh_fun_simp_ImpR)
+    by (simp add: better_crename_Cut fresh_atm(2))
+qed (auto simp: subst_fresh rename_fresh trm.inject)
+
+
 
 lemma substn_nrename_comm:
   assumes a: "x\<noteq>y" "x\<noteq>z"
@@ -2421,58 +2309,35 @@
 equivariance fic
 
 lemma fic_Ax_elim:
-  assumes a: "fic (Ax x a) b"
+  assumes "fic (Ax x a) b"
   shows "a=b"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-done
+  using assms by (auto simp: trm.inject elim!: fic.cases)
 
 lemma fic_NotR_elim:
-  assumes a: "fic (NotR (x).M a) b"
+  assumes "fic (NotR (x).M a) b"
   shows "a=b \<and> b\<sharp>M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-apply(subgoal_tac "b\<sharp>[xa].Ma")
-apply(drule sym)
-apply(simp_all add: abs_fresh)
-done
+  using assms
+  by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))
 
 lemma fic_OrR1_elim:
-  assumes a: "fic (OrR1 <a>.M b) c"
+  assumes "fic (OrR1 <a>.M b) c"
   shows "b=c \<and> c\<sharp>[a].M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-done
+  using assms by (auto simp: trm.inject elim!: fic.cases)
 
 lemma fic_OrR2_elim:
-  assumes a: "fic (OrR2 <a>.M b) c"
+  assumes "fic (OrR2 <a>.M b) c"
   shows "b=c \<and> c\<sharp>[a].M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-done
+  using assms by (auto simp: trm.inject elim!: fic.cases)
 
 lemma fic_AndR_elim:
-  assumes a: "fic (AndR <a>.M <b>.N c) d"
+  assumes "fic (AndR <a>.M <b>.N c) d"
   shows "c=d \<and> d\<sharp>[a].M \<and> d\<sharp>[b].N"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-done
+  using assms by (auto simp: trm.inject elim!: fic.cases)
 
 lemma fic_ImpR_elim:
   assumes a: "fic (ImpR (x).<a>.M b) c"
   shows "b=c \<and> b\<sharp>[a].M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-apply(subgoal_tac "c\<sharp>[xa].[aa].Ma")
-apply(drule sym)
-apply(simp_all add: abs_fresh)
-done
+  using assms by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6))
 
 lemma fic_rest_elims:
   shows "fic (Cut <a>.M (x).N) d \<Longrightarrow> False"