# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1713779037 -3600
# Node ID 022a9c26b14fc78552ab1cc08cdca5e7894430ac
# Parent  6d56e85f674e77ccd8527d32b89376e9bd435db4
Tidied up another messy theory

diff -r 6d56e85f674e -r 022a9c26b14f src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Sun Apr 21 16:31:30 2024 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Mon Apr 22 10:43:57 2024 +0100
@@ -31,11 +31,7 @@
   "size (Var n) = 0"
 | "size (t \<degree> u) = size t + size u + 1"
 | "size (Lam [x].t) = size t + 1"
-  apply finite_guess+
-  apply (rule TrueI)+
-  apply (simp add: fresh_nat)
-  apply fresh_guess+
-  done
+  by (finite_guess | simp add: fresh_nat | fresh_guess)+
 
 instance ..
 
@@ -47,40 +43,36 @@
   subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))"
 | subst_App: "(t\<^sub>1 \<degree> t\<^sub>2)[y::=s] = t\<^sub>1[y::=s] \<degree> t\<^sub>2[y::=s]"
 | subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
-  apply(finite_guess)+
-  apply(rule TrueI)+
-  apply(simp add: abs_fresh)
-  apply(fresh_guess)+
-  done
+  by (finite_guess | simp add: abs_fresh | fresh_guess)+
 
 lemma subst_eqvt [eqvt]:
   "(pi::name prm) \<bullet> (t[x::=u]) = (pi \<bullet> t)[(pi \<bullet> x)::=(pi \<bullet> u)]"
   by (nominal_induct t avoiding: x u rule: lam.strong_induct)
-    (perm_simp add: fresh_bij)+
+     (perm_simp add: fresh_bij)+
 
 lemma subst_rename:
   "y \<sharp> t \<Longrightarrow> ([(y, x)] \<bullet> t)[y::=u] = t[x::=u]"
   by (nominal_induct t avoiding: x y u rule: lam.strong_induct)
-    (simp_all add: fresh_atm calc_atm abs_fresh)
+     (simp_all add: fresh_atm calc_atm abs_fresh)
 
 lemma fresh_subst: 
   "(x::name) \<sharp> t \<Longrightarrow> x \<sharp> u \<Longrightarrow> x \<sharp> t[y::=u]"
   by (nominal_induct t avoiding: x y u rule: lam.strong_induct)
-    (auto simp add: abs_fresh fresh_atm)
+     (auto simp add: abs_fresh fresh_atm)
 
 lemma fresh_subst': 
   "(x::name) \<sharp> u \<Longrightarrow> x \<sharp> t[x::=u]"
   by (nominal_induct t avoiding: x u rule: lam.strong_induct)
-    (auto simp add: abs_fresh fresh_atm)
+     (auto simp add: abs_fresh fresh_atm)
 
 lemma subst_forget: "(x::name) \<sharp> t \<Longrightarrow> t[x::=u] = t"
   by (nominal_induct t avoiding: x u rule: lam.strong_induct)
-    (auto simp add: abs_fresh fresh_atm)
+     (auto simp add: abs_fresh fresh_atm)
 
 lemma subst_subst:
   "x \<noteq> y \<Longrightarrow> x \<sharp> v \<Longrightarrow> t[y::=v][x::=u[y::=v]] = t[x::=u][y::=v]"
   by (nominal_induct t avoiding: x y u v rule: lam.strong_induct)
-    (auto simp add: fresh_subst subst_forget)
+     (auto simp add: fresh_subst subst_forget)
 
 declare subst_Var [simp del]
 
@@ -132,20 +124,18 @@
 
 lemma Var_apps_eq_Var_apps_conv [iff]:
     "(Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
-  apply (induct rs arbitrary: ss rule: rev_induct)
-   apply (simp add: lam.inject)
-   apply blast
-  apply (induct_tac ss rule: rev_induct)
-   apply (auto simp add: lam.inject)
-  done
+proof (induct rs arbitrary: ss rule: rev_induct)
+  case Nil then show ?case by (auto simp add: lam.inject)
+next
+  case (snoc x xs) then show ?case 
+  by (induct ss rule: rev_induct) (auto simp add: lam.inject)
+qed
 
 lemma App_eq_foldl_conv:
   "(r \<degree> s = t \<degree>\<degree> ts) =
     (if ts = [] then r \<degree> s = t
     else (\<exists>ss. ts = ss @ [s] \<and> r = t \<degree>\<degree> ss))"
-  apply (rule_tac xs = ts in rev_exhaust)
-   apply (auto simp add: lam.inject)
-  done
+  by (rule rev_exhaust [of ts]) (auto simp: lam.inject)
 
 lemma Abs_eq_apps_conv [iff]:
     "((Lam [x].r) = s \<degree>\<degree> ss) = ((Lam [x].r) = s \<and> ss = [])"
@@ -160,19 +150,20 @@
 
 lemma Var_apps_neq_Abs_apps [iff]:
     "Var n \<degree>\<degree> ts \<noteq> (Lam [x].r) \<degree>\<degree> ss"
-  apply (induct ss arbitrary: ts rule: rev_induct)
-   apply simp
-  apply (induct_tac ts rule: rev_induct)
-   apply (auto simp add: lam.inject)
-  done
+proof (induct ss arbitrary: ts rule: rev_induct)
+  case Nil then show ?case by simp
+next
+  case (snoc x xs) then show ?case
+  by (induct ts rule: rev_induct) (auto simp add: lam.inject)
+qed
 
 lemma ex_head_tail:
   "\<exists>ts h. t = h \<degree>\<degree> ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>x u. h = (Lam [x].u)))"
-  apply (induct t rule: lam.induct)
-    apply (metis foldl_Nil)
-   apply (metis foldl_Cons foldl_Nil foldl_append)
-  apply (metis foldl_Nil)
-  done
+proof (induct t rule: lam.induct)
+  case (App lam1 lam2)
+  then show ?case
+    by (metis foldl_Cons foldl_Nil foldl_append)
+qed auto
 
 lemma size_apps [simp]:
   "size (r \<degree>\<degree> rs) = size r + foldl (+) 0 (map size rs) + length rs"
@@ -198,56 +189,67 @@
 
 text \<open>A customized induction schema for \<open>\<degree>\<degree>\<close>.\<close>
 
-lemma lem:
+lemma Apps_lam_induct_aux:
   assumes "\<And>n ts (z::'a::fs_name). (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z (Var n \<degree>\<degree> ts)"
     and "\<And>x u ts z. x \<sharp> z \<Longrightarrow> (\<And>z. P z u) \<Longrightarrow> (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z ((Lam [x].u) \<degree>\<degree> ts)"
   shows "size t = n \<Longrightarrow> P z t"
-  apply (induct n arbitrary: t z rule: nat_less_induct)
-  apply (cut_tac t = t in ex_head_tail)
-  apply clarify
-  apply (erule disjE)
-   apply clarify
-   apply (rule assms)
-   apply clarify
-   apply (erule allE, erule impE)
-    prefer 2
-    apply (erule allE, erule impE, rule refl, erule spec)
-    apply simp
-    apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
-    apply (fastforce simp add: sum_list_map_remove1)
-  apply clarify
-  apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
-   prefer 2
-   apply (blast intro: exists_fresh' fin_supp) 
-  apply (erule exE)
-  apply (subgoal_tac "(Lam [x].u) = (Lam [y].([(y, x)] \<bullet> u))")
-  prefer 2
-  apply (auto simp add: lam.inject alpha' fresh_prod fresh_atm)[]
-  apply (simp (no_asm_simp))
-  apply (rule assms)
-  apply (simp add: fresh_prod)
-   apply (erule allE, erule impE)
-    prefer 2
-    apply (erule allE, erule impE, rule refl, erule spec)
-   apply simp
-  apply clarify
-  apply (erule allE, erule impE)
-   prefer 2
-   apply blast
-  apply simp
-  apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
-  apply (fastforce simp add: sum_list_map_remove1)
-  done
+proof (induct n arbitrary: t z rule: less_induct)
+  case (less n)
+  obtain ts h where t: "t = h \<degree>\<degree> ts" and D: "(\<exists>a. h = Var a) \<or> (\<exists>x u. h = (Lam [x].u))"
+    using ex_head_tail [of t] by metis
+  show ?case 
+    using D
+  proof (elim exE disjE)
+    fix a :: name
+    assume h: "h = Var a"
+    have "P z t" if "t \<in> set ts" for z t
+    proof -
+      have "size t < length ts + fold (+) (map size ts) 0"
+        using that
+        by (fastforce simp add: sum_list_map_remove1 fold_plus_sum_list_rev)
+      then have "size t < size (Var a \<degree>\<degree> ts)"
+        by simp (simp add: add.commute foldl_conv_fold)
+      then show ?thesis
+        using h less.hyps less.prems t by blast
+    qed
+    then show "P z t"
+      unfolding t h by (blast intro: assms)
+  next
+    fix x u
+    assume h: "h = (Lam [x].u)"
+    obtain y::name where y: "y \<sharp> (x, u, z)"
+      by (metis exists_fresh' fin_supp) 
+    then have eq: "(Lam [x].u) = (Lam [y].([(y, x)] \<bullet> u))"
+      by (metis alpha' fresh_prod lam.inject(3) perm_fresh_fresh)
+    show "P z t"
+      unfolding t h eq
+    proof (intro assms strip)
+      show "y \<sharp> z"
+        by (simp add: y)
+      have "size ([(y, x)] \<bullet> u) < size ((Lam [x].u) \<degree>\<degree> ts)"
+        by (simp add: eq)
+      then show "P z ([(y, x)] \<bullet> u)" for z
+        using h less.hyps less.prems t by blast
+      show "P z t" if "t\<in>set ts" for z t
+      proof -
+        have 2: "size t < size ((Lam [x].u) \<degree>\<degree> ts)"
+          using that
+          apply (simp add: eq)
+          apply (simp only: foldl_conv_fold add.commute fold_plus_sum_list_rev)
+          apply (fastforce simp add: sum_list_map_remove1)
+          done
+        then show ?thesis
+          using h less.hyps less.prems t by blast
+      qed
+    qed
+  qed
+qed
 
 theorem Apps_lam_induct:
   assumes "\<And>n ts (z::'a::fs_name). (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z (Var n \<degree>\<degree> ts)"
     and "\<And>x u ts z. x \<sharp> z \<Longrightarrow> (\<And>z. P z u) \<Longrightarrow> (\<And>z. \<forall>t \<in> set ts. P z t) \<Longrightarrow> P z ((Lam [x].u) \<degree>\<degree> ts)"
   shows "P z t"
-  apply (rule_tac t = t and z = z in lem)
-    prefer 3
-    apply (rule refl)
-    using assms apply blast+
-  done
+  using Apps_lam_induct_aux [of P] assms by blast
 
 
 subsection \<open>Congruence rules\<close>
@@ -277,66 +279,40 @@
 
 definition
   step1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
-  "step1 r =
+  "step1 r \<equiv>
     (\<lambda>ys xs. \<exists>us z z' vs. xs = us @ z # vs \<and> r z' z \<and> ys =
       us @ z' # vs)"
 
 lemma not_Nil_step1 [iff]: "\<not> step1 r [] xs"
-  apply (unfold step1_def)
-  apply blast
-  done
+  by (simp add: step1_def)
 
 lemma not_step1_Nil [iff]: "\<not> step1 r xs []"
-  apply (unfold step1_def)
-  apply blast
-  done
+  by (simp add: step1_def)
 
 lemma Cons_step1_Cons [iff]:
-    "(step1 r (y # ys) (x # xs)) =
-      (r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs)"
-  apply (unfold step1_def)
-  apply (rule iffI)
-   apply (erule exE)
-   apply (rename_tac ts)
-   apply (case_tac ts)
-    apply fastforce
-   apply force
-  apply (erule disjE)
-   apply blast
-  apply (blast intro: Cons_eq_appendI)
-  done
-
-lemma append_step1I:
-  "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
-    \<Longrightarrow> step1 r (ys @ vs) (xs @ us)"
-  apply (unfold step1_def)
-  apply auto
-   apply blast
-  apply (blast intro: append_eq_appendI)
-  done
+    "step1 r (y # ys) (x # xs) \<longleftrightarrow> r y x \<and> xs = ys \<or> x = y \<and> step1 r ys xs"
+  apply (rule )
+   apply (smt (verit, ccfv_SIG) append_eq_Cons_conv list.inject step1_def)
+  by (metis append_Cons append_Nil step1_def)
 
 lemma Cons_step1E [elim!]:
   assumes "step1 r ys (x # xs)"
     and "\<And>y. ys = y # xs \<Longrightarrow> r y x \<Longrightarrow> R"
     and "\<And>zs. ys = x # zs \<Longrightarrow> step1 r zs xs \<Longrightarrow> R"
   shows R
-  using assms
-  apply (cases ys)
-   apply (simp add: step1_def)
-  apply blast
-  done
+  by (metis Cons_step1_Cons assms list.exhaust not_Nil_step1)
+
+lemma append_step1I:
+  "step1 r ys xs \<and> vs = us \<or> ys = xs \<and> step1 r vs us
+    \<Longrightarrow> step1 r (ys @ vs) (xs @ us)"
+  by (smt (verit) append_Cons append_assoc step1_def)
 
 lemma Snoc_step1_SnocD:
-  "step1 r (ys @ [y]) (xs @ [x])
-    \<Longrightarrow> (step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
-  apply (unfold step1_def)
-  apply (clarify del: disjCI)
-  apply (rename_tac vs)
-  apply (rule_tac xs = vs in rev_exhaust)
-   apply force
-  apply simp
-  apply blast
-  done
+  assumes "step1 r (ys @ [y]) (xs @ [x])"
+  shows "(step1 r ys xs \<and> y = x \<or> ys = xs \<and> r y x)"
+  using assms
+    apply (clarsimp simp: step1_def)
+  by (metis butlast.simps(2) butlast_append butlast_snoc last.simps last_appendR list.simps(3))
 
 
 subsection \<open>Lifting beta-reduction to lists\<close>
@@ -347,15 +323,15 @@
 
 lemma head_Var_reduction:
   "Var n \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> v \<Longrightarrow> \<exists>ss. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<and> v = Var n \<degree>\<degree> ss"
-  apply (induct u \<equiv> "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
-     apply simp
-    apply (rule_tac xs = rs in rev_exhaust)
-     apply simp
-    apply (atomize, force intro: append_step1I iff: lam.inject)
-   apply (rule_tac xs = rs in rev_exhaust)
-    apply simp
-    apply (auto 0 3 intro: disjI2 [THEN append_step1I] simp add: lam.inject)
-  done
+proof (induct u \<equiv> "Var n \<degree>\<degree> rs" v arbitrary: rs set: beta)
+  case (appL s t u)
+  then show ?case
+    by (smt (verit, best) App_eq_foldl_conv app_last append_step1I lam.distinct(1))
+next
+  case (appR s t u)
+  then show ?case
+    by (smt (verit, ccfv_SIG) App_eq_foldl_conv Cons_step1_Cons app_last append_step1I lam.distinct(1))
+qed auto
 
 lemma apps_betasE [case_names appL appR beta, consumes 1]:
   assumes major: "r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> s"
@@ -364,58 +340,48 @@
       "\<And>t u us. (x \<sharp> r \<Longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us) \<Longrightarrow> R"
   shows R
 proof -
+  note [[simproc del: defined_all]]
   from major have
    "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
     (\<exists>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<and> s = r \<degree>\<degree> rs') \<or>
     (\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
-    supply [[simproc del: defined_all]]
-    apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
-    apply (simp add: App_eq_foldl_conv)
-    apply (split if_split_asm)
-    apply simp
-    apply blast
-    apply simp
-    apply (rule impI)+
-    apply (rule disjI2)
-    apply (rule disjI2)
-    apply (subgoal_tac "r = [(xa, x)] \<bullet> (Lam [x].s)")
-    prefer 2
-    apply (simp add: perm_fresh_fresh)
-    apply (drule conjunct1)
-    apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] \<bullet> s)")
-    prefer 2
-    apply (simp add: calc_atm)
-    apply (thin_tac "r = _")
-    apply simp
-    apply (rule exI)
-    apply (rule conjI)
-    apply (rule refl)
-    apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename)
-      apply (drule App_eq_foldl_conv [THEN iffD1])
-      apply (split if_split_asm)
-       apply simp
+  proof (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
+    case (beta y t s)
+    then show ?case
+      apply (simp add: App_eq_foldl_conv split: if_split_asm)
        apply blast
-      apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append)
-     apply (drule App_eq_foldl_conv [THEN iffD1])
-     apply (split if_split_asm)
-      apply simp
+      by (metis (no_types, lifting) abs_fresh(1) alpha' lam.fresh(3) lam.inject(3) subst_rename)
+  next
+    case (appL s t u)
+    then show ?case
+      apply (simp add: App_eq_foldl_conv split: if_split_asm)
       apply blast
-     apply (clarify, auto 0 3 intro!: exI intro: append_step1I)
-    done
+      by (smt (verit) append_Cons append_step1I snoc_eq_iff_butlast)
+  next
+    case (appR s t u)
+    then show ?case
+      apply (simp add: App_eq_foldl_conv step1_def split: if_split_asm)
+      apply force
+      by (metis snoc_eq_iff_butlast)
+  next
+    case (abs s t x)
+    then show ?case
+      by blast
+  qed
   with cases show ?thesis by blast
 qed
 
 lemma apps_preserves_betas [simp]:
     "rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 ss \<Longrightarrow> r \<degree>\<degree> rs \<rightarrow>\<^sub>\<beta> r \<degree>\<degree> ss"
-  apply (induct rs arbitrary: ss rule: rev_induct)
-   apply simp
-  apply simp
-  apply (rule_tac xs = ss in rev_exhaust)
-   apply simp
-  apply simp
-  apply (drule Snoc_step1_SnocD)
-  apply blast
-  done
+proof (induct rs arbitrary: ss rule: rev_induct)
+  case Nil
+  then show ?case by simp
+next
+  case (snoc x ts)
+  then show ?case 
+    apply (simp add: step1_def)
+    by (smt (verit) appR app_last apps_preserves_beta foldl_Cons foldl_append)
+qed
 
 
 subsection \<open>Standard reduction relation\<close>
@@ -653,14 +619,7 @@
 lemma listsp_eqvt [eqvt]:
   assumes xs: "listsp p (xs::'a::pt_name list)"
   shows "listsp ((pi::name prm) \<bullet> p) (pi \<bullet> xs)" using xs
-  apply induct
-  apply simp
-  apply simp
-  apply (rule listsp.intros)
-  apply (drule_tac pi=pi in perm_boolI)
-  apply perm_simp
-  apply assumption
-  done
+by induction (use perm_app in force)+
 
 inductive NF :: "lam \<Rightarrow> bool"
 where
@@ -674,13 +633,7 @@
 lemma Abs_NF:
   assumes NF: "NF ((Lam [x].t) \<degree>\<degree> ts)"
   shows "ts = []" using NF
-proof cases
-  case (App us i)
-  thus ?thesis by (simp add: Var_apps_neq_Abs_apps [THEN not_sym])
-next
-  case (Abs u)
-  thus ?thesis by simp
-qed
+  by (metis Abs_eq_apps_conv NF.cases Var_apps_neq_Abs_apps)
 
 text \<open>
 \<^term>\<open>NF\<close> characterizes exactly the terms that are in normal form.