--- 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.