(* Title: HOL/Nominal/Examples/Standardization.thy Author: Stefan Berghofer and Tobias Nipkow Copyright 2005, 2008 TU Muenchen *) section ‹Standardization› theory Standardization imports "HOL-Nominal.Nominal" begin text ‹ The proof of the standardization theorem, as well as most of the theorems about lambda calculus in the following sections, are taken from ‹HOL/Lambda›. › subsection ‹Lambda terms› atom_decl name nominal_datatype lam = Var "name" | App "lam" "lam" (infixl "°" 200) | Lam "«name»lam" ("Lam [_]._" [0, 10] 10) instantiation lam :: size begin nominal_primrec size_lam where "size (Var n) = 0" | "size (t ° 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 instance .. end nominal_primrec subst :: "lam ⇒ name ⇒ lam ⇒ lam" ("_[_::=_]" [300, 0, 0] 300) where subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))" | subst_App: "(t⇩_{1}° t⇩_{2})[y::=s] = t⇩_{1}[y::=s] ° t⇩_{2}[y::=s]" | subst_Lam: "x ♯ (y, s) ⟹ (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 lemma subst_eqvt [eqvt]: "(pi::name prm) ∙ (t[x::=u]) = (pi ∙ t)[(pi ∙ x)::=(pi ∙ u)]" by (nominal_induct t avoiding: x u rule: lam.strong_induct) (perm_simp add: fresh_bij)+ lemma subst_rename: "y ♯ t ⟹ ([(y, x)] ∙ 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) lemma fresh_subst: "(x::name) ♯ t ⟹ x ♯ u ⟹ x ♯ t[y::=u]" by (nominal_induct t avoiding: x y u rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma fresh_subst': "(x::name) ♯ u ⟹ x ♯ t[x::=u]" by (nominal_induct t avoiding: x u rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma subst_forget: "(x::name) ♯ t ⟹ t[x::=u] = t" by (nominal_induct t avoiding: x u rule: lam.strong_induct) (auto simp add: abs_fresh fresh_atm) lemma subst_subst: "x ≠ y ⟹ x ♯ v ⟹ 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) declare subst_Var [simp del] lemma subst_eq [simp]: "(Var x)[x::=u] = u" by (simp add: subst_Var) lemma subst_neq [simp]: "x ≠ y ⟹ (Var x)[y::=u] = Var x" by (simp add: subst_Var) inductive beta :: "lam ⇒ lam ⇒ bool" (infixl "→⇩_{β}" 50) where beta: "x ♯ t ⟹ (Lam [x].s) ° t →⇩_{β}s[x::=t]" | appL [simp, intro!]: "s →⇩_{β}t ⟹ s ° u →⇩_{β}t ° u" | appR [simp, intro!]: "s →⇩_{β}t ⟹ u ° s →⇩_{β}u ° t" | abs [simp, intro!]: "s →⇩_{β}t ⟹ (Lam [x].s) →⇩_{β}(Lam [x].t)" equivariance beta nominal_inductive beta by (simp_all add: abs_fresh fresh_subst') lemma better_beta [simp, intro!]: "(Lam [x].s) ° t →⇩_{β}s[x::=t]" proof - obtain y::name where y: "y ♯ (x, s, t)" by (rule exists_fresh) (rule fin_supp) then have "y ♯ t" by simp then have "(Lam [y]. [(y, x)] ∙ s) ° t →⇩_{β}([(y, x)] ∙ s)[y::=t]" by (rule beta) moreover from y have "(Lam [x].s) = (Lam [y]. [(y, x)] ∙ s)" by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) ultimately show ?thesis using y by (simp add: subst_rename) qed abbreviation beta_reds :: "lam ⇒ lam ⇒ bool" (infixl "→⇩_{β}⇧^{*}" 50) where "s →⇩_{β}⇧^{*}t ≡ beta⇧^{*}⇧^{*}s t" subsection ‹Application of a term to a list of terms› abbreviation list_application :: "lam ⇒ lam list ⇒ lam" (infixl "°°" 150) where "t °° ts ≡ foldl (°) t ts" lemma apps_eq_tail_conv [iff]: "(r °° ts = s °° ts) = (r = s)" by (induct ts rule: rev_induct) (auto simp add: lam.inject) lemma Var_eq_apps_conv [iff]: "(Var m = s °° ss) = (Var m = s ∧ ss = [])" by (induct ss arbitrary: s) auto lemma Var_apps_eq_Var_apps_conv [iff]: "(Var m °° rs = Var n °° ss) = (m = n ∧ 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 lemma App_eq_foldl_conv: "(r ° s = t °° ts) = (if ts = [] then r ° s = t else (∃ss. ts = ss @ [s] ∧ r = t °° ss))" apply (rule_tac xs = ts in rev_exhaust) apply (auto simp add: lam.inject) done lemma Abs_eq_apps_conv [iff]: "((Lam [x].r) = s °° ss) = ((Lam [x].r) = s ∧ ss = [])" by (induct ss rule: rev_induct) auto lemma apps_eq_Abs_conv [iff]: "(s °° ss = (Lam [x].r)) = (s = (Lam [x].r) ∧ ss = [])" by (induct ss rule: rev_induct) auto lemma Abs_App_neq_Var_apps [iff]: "(Lam [x].s) ° t ≠ Var n °° ss" by (induct ss arbitrary: s t rule: rev_induct) (auto simp add: lam.inject) lemma Var_apps_neq_Abs_apps [iff]: "Var n °° ts ≠ (Lam [x].r) °° 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 lemma ex_head_tail: "∃ts h. t = h °° ts ∧ ((∃n. h = Var n) ∨ (∃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 lemma size_apps [simp]: "size (r °° rs) = size r + foldl (+) 0 (map size rs) + length rs" by (induct rs rule: rev_induct) auto lemma lem0: "(0::nat) < k ⟹ m ≤ n ⟹ m < n + k" by simp lemma subst_map [simp]: "(t °° ts)[x::=u] = t[x::=u] °° map (λt. t[x::=u]) ts" by (induct ts arbitrary: t) simp_all lemma app_last: "(t °° ts) ° u = t °° (ts @ [u])" by simp lemma perm_apps [eqvt]: "(pi::name prm) ∙ (t °° ts) = ((pi ∙ t) °° (pi ∙ ts))" by (induct ts rule: rev_induct) (auto simp add: append_eqvt) lemma fresh_apps [simp]: "(x::name) ♯ (t °° ts) = (x ♯ t ∧ x ♯ ts)" by (induct ts rule: rev_induct) (auto simp add: fresh_list_append fresh_list_nil fresh_list_cons) text ‹A customized induction schema for ‹°°›.› lemma lem: assumes "⋀n ts (z::'a::fs_name). (⋀z. ∀t ∈ set ts. P z t) ⟹ P z (Var n °° ts)" and "⋀x u ts z. x ♯ z ⟹ (⋀z. P z u) ⟹ (⋀z. ∀t ∈ set ts. P z t) ⟹ P z ((Lam [x].u) °° ts)" shows "size t = n ⟹ 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 "∃y::name. y ♯ (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)] ∙ 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 theorem Apps_lam_induct: assumes "⋀n ts (z::'a::fs_name). (⋀z. ∀t ∈ set ts. P z t) ⟹ P z (Var n °° ts)" and "⋀x u ts z. x ♯ z ⟹ (⋀z. P z u) ⟹ (⋀z. ∀t ∈ set ts. P z t) ⟹ P z ((Lam [x].u) °° 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 subsection ‹Congruence rules› lemma apps_preserves_beta [simp]: "r →⇩_{β}s ⟹ r °° ss →⇩_{β}s °° ss" by (induct ss rule: rev_induct) auto lemma rtrancl_beta_Abs [intro!]: "s →⇩_{β}⇧^{*}s' ⟹ (Lam [x].s) →⇩_{β}⇧^{*}(Lam [x].s')" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ lemma rtrancl_beta_AppL: "s →⇩_{β}⇧^{*}s' ⟹ s ° t →⇩_{β}⇧^{*}s' ° t" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ lemma rtrancl_beta_AppR: "t →⇩_{β}⇧^{*}t' ⟹ s ° t →⇩_{β}⇧^{*}s ° t'" by (induct set: rtranclp) (blast intro: rtranclp.rtrancl_into_rtrancl)+ lemma rtrancl_beta_App [intro]: "s →⇩_{β}⇧^{*}s' ⟹ t →⇩_{β}⇧^{*}t' ⟹ s ° t →⇩_{β}⇧^{*}s' ° t'" by (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR intro: rtranclp_trans) subsection ‹Lifting an order to lists of elements› definition step1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool" where "step1 r = (λys xs. ∃us z z' vs. xs = us @ z # vs ∧ r z' z ∧ ys = us @ z' # vs)" lemma not_Nil_step1 [iff]: "¬ step1 r [] xs" apply (unfold step1_def) apply blast done lemma not_step1_Nil [iff]: "¬ step1 r xs []" apply (unfold step1_def) apply blast done lemma Cons_step1_Cons [iff]: "(step1 r (y # ys) (x # xs)) = (r y x ∧ xs = ys ∨ x = y ∧ 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 ∧ vs = us ∨ ys = xs ∧ step1 r vs us ⟹ step1 r (ys @ vs) (xs @ us)" apply (unfold step1_def) apply auto apply blast apply (blast intro: append_eq_appendI) done lemma Cons_step1E [elim!]: assumes "step1 r ys (x # xs)" and "⋀y. ys = y # xs ⟹ r y x ⟹ R" and "⋀zs. ys = x # zs ⟹ step1 r zs xs ⟹ R" shows R using assms apply (cases ys) apply (simp add: step1_def) apply blast done lemma Snoc_step1_SnocD: "step1 r (ys @ [y]) (xs @ [x]) ⟹ (step1 r ys xs ∧ y = x ∨ ys = xs ∧ 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 subsection ‹Lifting beta-reduction to lists› abbreviation list_beta :: "lam list ⇒ lam list ⇒ bool" (infixl "[→⇩_{β}]⇩_{1}" 50) where "rs [→⇩_{β}]⇩_{1}ss ≡ step1 beta rs ss" lemma head_Var_reduction: "Var n °° rs →⇩_{β}v ⟹ ∃ss. rs [→⇩_{β}]⇩_{1}ss ∧ v = Var n °° ss" apply (induct u ≡ "Var n °° 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 lemma apps_betasE [case_names appL appR beta, consumes 1]: assumes major: "r °° rs →⇩_{β}s" and cases: "⋀r'. r →⇩_{β}r' ⟹ s = r' °° rs ⟹ R" "⋀rs'. rs [→⇩_{β}]⇩_{1}rs' ⟹ s = r °° rs' ⟹ R" "⋀t u us. (x ♯ r ⟹ r = (Lam [x].t) ∧ rs = u # us ∧ s = t[x::=u] °° us) ⟹ R" shows R proof - from major have "(∃r'. r →⇩_{β}r' ∧ s = r' °° rs) ∨ (∃rs'. rs [→⇩_{β}]⇩_{1}rs' ∧ s = r °° rs') ∨ (∃t u us. x ♯ r ⟶ r = (Lam [x].t) ∧ rs = u # us ∧ s = t[x::=u] °° us)" apply (nominal_induct u ≡ "r °° 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)] ∙ (Lam [x].s)") prefer 2 apply (simp add: perm_fresh_fresh) apply (drule conjunct1) apply (subgoal_tac "r = (Lam [xa]. [(xa, x)] ∙ 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 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 apply blast apply (clarify, auto 0 3 intro!: exI intro: append_step1I) done with cases show ?thesis by blast qed lemma apps_preserves_betas [simp]: "rs [→⇩_{β}]⇩_{1}ss ⟹ r °° rs →⇩_{β}r °° 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 subsection ‹Standard reduction relation› text ‹ Based on lecture notes by Ralph Matthes, original proof idea due to Ralph Loader. › declare listrel_mono [mono_set] lemma listrelp_eqvt [eqvt]: fixes f :: "'a::pt_name ⇒ 'b::pt_name ⇒ bool" assumes xy: "listrelp f (x::'a::pt_name list) y" shows "listrelp ((pi::name prm) ∙ f) (pi ∙ x) (pi ∙ y)" using xy by induct (simp_all add: listrelp.intros perm_app [symmetric]) inductive sred :: "lam ⇒ lam ⇒ bool" (infixl "→⇩_{s}" 50) and sredlist :: "lam list ⇒ lam list ⇒ bool" (infixl "[→⇩_{s}]" 50) where "s [→⇩_{s}] t ≡ listrelp (→⇩_{s}) s t" | Var: "rs [→⇩_{s}] rs' ⟹ Var x °° rs →⇩_{s}Var x °° rs'" | Abs: "x ♯ (ss, ss') ⟹ r →⇩_{s}r' ⟹ ss [→⇩_{s}] ss' ⟹ (Lam [x].r) °° ss →⇩_{s}(Lam [x].r') °° ss'" | Beta: "x ♯ (s, ss, t) ⟹ r[x::=s] °° ss →⇩_{s}t ⟹ (Lam [x].r) ° s °° ss →⇩_{s}t" equivariance sred nominal_inductive sred by (simp add: abs_fresh)+ lemma better_sred_Abs: assumes H1: "r →⇩_{s}r'" and H2: "ss [→⇩_{s}] ss'" shows "(Lam [x].r) °° ss →⇩_{s}(Lam [x].r') °° ss'" proof - obtain y::name where y: "y ♯ (x, r, r', ss, ss')" by (rule exists_fresh) (rule fin_supp) then have "y ♯ (ss, ss')" by simp moreover from H1 have "[(y, x)] ∙ (r →⇩_{s}r')" by (rule perm_boolI) then have "([(y, x)] ∙ r) →⇩_{s}([(y, x)] ∙ r')" by (simp add: eqvts) ultimately have "(Lam [y]. [(y, x)] ∙ r) °° ss →⇩_{s}(Lam [y]. [(y, x)] ∙ r') °° ss'" using H2 by (rule sred.Abs) moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] ∙ r)" by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) moreover from y have "(Lam [x].r') = (Lam [y]. [(y, x)] ∙ r')" by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) ultimately show ?thesis by simp qed lemma better_sred_Beta: assumes H: "r[x::=s] °° ss →⇩_{s}t" shows "(Lam [x].r) ° s °° ss →⇩_{s}t" proof - obtain y::name where y: "y ♯ (x, r, s, ss, t)" by (rule exists_fresh) (rule fin_supp) then have "y ♯ (s, ss, t)" by simp moreover from y H have "([(y, x)] ∙ r)[y::=s] °° ss →⇩_{s}t" by (simp add: subst_rename) ultimately have "(Lam [y].[(y, x)] ∙ r) ° s °° ss →⇩_{s}t" by (rule sred.Beta) moreover from y have "(Lam [x].r) = (Lam [y]. [(y, x)] ∙ r)" by (auto simp add: lam.inject alpha' fresh_prod fresh_atm) ultimately show ?thesis by simp qed lemmas better_sred_intros = sred.Var better_sred_Abs better_sred_Beta lemma refl_listrelp: "∀x∈set xs. R x x ⟹ listrelp R xs xs" by (induct xs) (auto intro: listrelp.intros) lemma refl_sred: "t →⇩_{s}t" by (nominal_induct t rule: Apps_lam_induct) (auto intro: refl_listrelp better_sred_intros) lemma listrelp_conj1: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp R x y" by (erule listrelp.induct) (auto intro: listrelp.intros) lemma listrelp_conj2: "listrelp (λx y. R x y ∧ S x y) x y ⟹ listrelp S x y" by (erule listrelp.induct) (auto intro: listrelp.intros) lemma listrelp_app: assumes xsys: "listrelp R xs ys" shows "listrelp R xs' ys' ⟹ listrelp R (xs @ xs') (ys @ ys')" using xsys by (induct arbitrary: xs' ys') (auto intro: listrelp.intros) lemma lemma1: assumes r: "r →⇩_{s}r'" and s: "s →⇩_{s}s'" shows "r ° s →⇩_{s}r' ° s'" using r proof induct case (Var rs rs' x) then have "rs [→⇩_{s}] rs'" by (rule listrelp_conj1) moreover have "[s] [→⇩_{s}] [s']" by (iprover intro: s listrelp.intros) ultimately have "rs @ [s] [→⇩_{s}] rs' @ [s']" by (rule listrelp_app) hence "Var x °° (rs @ [s]) →⇩_{s}Var x °° (rs' @ [s'])" by (rule sred.Var) thus ?case by (simp only: app_last) next case (Abs x ss ss' r r') from Abs(4) have "ss [→⇩_{s}] ss'" by (rule listrelp_conj1) moreover have "[s] [→⇩_{s}] [s']" by (iprover intro: s listrelp.intros) ultimately have "ss @ [s] [→⇩_{s}] ss' @ [s']" by (rule listrelp_app) with ‹r →⇩_{s}r'› have "(Lam [x].r) °° (ss @ [s]) →⇩_{s}(Lam [x].r') °° (ss' @ [s'])" by (rule better_sred_Abs) thus ?case by (simp only: app_last) next case (Beta x u ss t r) hence "r[x::=u] °° (ss @ [s]) →⇩_{s}t ° s'" by (simp only: app_last) hence "(Lam [x].r) ° u °° (ss @ [s]) →⇩_{s}t ° s'" by (rule better_sred_Beta) thus ?case by (simp only: app_last) qed lemma lemma1': assumes ts: "ts [→⇩_{s}] ts'" shows "r →⇩_{s}r' ⟹ r °° ts →⇩_{s}r' °° ts'" using ts by (induct arbitrary: r r') (auto intro: lemma1) lemma listrelp_betas: assumes ts: "listrelp (→⇩_{β}⇧^{*}) ts ts'" shows "⋀t t'. t →⇩_{β}⇧^{*}t' ⟹ t °° ts →⇩_{β}⇧^{*}t' °° ts'" using ts by induct auto lemma lemma2: assumes t: "t →⇩_{s}u" shows "t →⇩_{β}⇧^{*}u" using t by induct (auto dest: listrelp_conj2 intro: listrelp_betas apps_preserves_beta converse_rtranclp_into_rtranclp) lemma lemma3: assumes r: "r →⇩_{s}r'" shows "s →⇩_{s}s' ⟹ r[x::=s] →⇩_{s}r'[x::=s']" using r proof (nominal_induct avoiding: x s s' rule: sred.strong_induct) case (Var rs rs' y) hence "map (λt. t[x::=s]) rs [→⇩_{s}] map (λt. t[x::=s']) rs'" by induct (auto intro: listrelp.intros Var) moreover have "Var y[x::=s] →⇩_{s}Var y[x::=s']" by (cases "y = x") (auto simp add: Var intro: refl_sred) ultimately show ?case by simp (rule lemma1') next case (Abs y ss ss' r r') then have "r[x::=s] →⇩_{s}r'[x::=s']" by fast moreover from Abs(8) ‹s →⇩_{s}s'› have "map (λt. t[x::=s]) ss [→⇩_{s}] map (λt. t[x::=s']) ss'" by induct (auto intro: listrelp.intros Abs) ultimately show ?case using Abs(6) ‹y ♯ x› ‹y ♯ s› ‹y ♯ s'› by simp (rule better_sred_Abs) next case (Beta y u ss t r) thus ?case by (auto simp add: subst_subst fresh_atm intro: better_sred_Beta) qed lemma lemma4_aux: assumes rs: "listrelp (λt u. t →⇩_{s}u ∧ (∀r. u →⇩_{β}r ⟶ t →⇩_{s}r)) rs rs'" shows "rs' [→⇩_{β}]⇩_{1}ss ⟹ rs [→⇩_{s}] ss" using rs proof (induct arbitrary: ss) case Nil thus ?case by cases (auto intro: listrelp.Nil) next case (Cons x y xs ys) note Cons' = Cons show ?case proof (cases ss) case Nil with Cons show ?thesis by simp next case (Cons y' ys') hence ss: "ss = y' # ys'" by simp from Cons Cons' have "y →⇩_{β}y' ∧ ys' = ys ∨ y' = y ∧ ys [→⇩_{β}]⇩_{1}ys'" by simp hence "x # xs [→⇩_{s}] y' # ys'" proof assume H: "y →⇩_{β}y' ∧ ys' = ys" with Cons' have "x →⇩_{s}y'" by blast moreover from Cons' have "xs [→⇩_{s}] ys" by (iprover dest: listrelp_conj1) ultimately have "x # xs [→⇩_{s}] y' # ys" by (rule listrelp.Cons) with H show ?thesis by simp next assume H: "y' = y ∧ ys [→⇩_{β}]⇩_{1}ys'" with Cons' have "x →⇩_{s}y'" by blast moreover from H have "xs [→⇩_{s}] ys'" by (blast intro: Cons') ultimately show ?thesis by (rule listrelp.Cons) qed with ss show ?thesis by simp qed qed lemma lemma4: assumes r: "r →⇩_{s}r'" shows "r' →⇩_{β}r'' ⟹ r →⇩_{s}r''" using r proof (nominal_induct avoiding: r'' rule: sred.strong_induct) case (Var rs rs' x) then obtain ss where rs: "rs' [→⇩_{β}]⇩_{1}ss" and r'': "r'' = Var x °° ss" by (blast dest: head_Var_reduction) from Var(1) [simplified] rs have "rs [→⇩_{s}] ss" by (rule lemma4_aux) hence "Var x °° rs →⇩_{s}Var x °° ss" by (rule sred.Var) with r'' show ?case by simp next case (Abs x ss ss' r r') from ‹(Lam [x].r') °° ss' →⇩_{β}r''› show ?case proof (cases rule: apps_betasE [where x=x]) case (appL s) then obtain r''' where s: "s = (Lam [x].r''')" and r''': "r' →⇩_{β}r'''" using ‹x ♯ r''› by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha) from r''' have "r →⇩_{s}r'''" by (blast intro: Abs) moreover from Abs have "ss [→⇩_{s}] ss'" by (iprover dest: listrelp_conj1) ultimately have "(Lam [x].r) °° ss →⇩_{s}(Lam [x].r''') °° ss'" by (rule better_sred_Abs) with appL s show "(Lam [x].r) °° ss →⇩_{s}r''" by simp next case (appR rs') from Abs(6) [simplified] ‹ss' [→⇩_{β}]⇩_{1}rs'› have "ss [→⇩_{s}] rs'" by (rule lemma4_aux) with ‹r →⇩_{s}r'› have "(Lam [x].r) °° ss →⇩_{s}(Lam [x].r') °° rs'" by (rule better_sred_Abs) with appR show "(Lam [x].r) °° ss →⇩_{s}r''" by simp next case (beta t u' us') then have Lam_eq: "(Lam [x].r') = (Lam [x].t)" and ss': "ss' = u' # us'" and r'': "r'' = t[x::=u'] °° us'" by (simp_all add: abs_fresh) from Abs(6) ss' obtain u us where ss: "ss = u # us" and u: "u →⇩_{s}u'" and us: "us [→⇩_{s}] us'" by cases (auto dest!: listrelp_conj1) have "r[x::=u] →⇩_{s}r'[x::=u']" using ‹r →⇩_{s}r'› and u by (rule lemma3) with us have "r[x::=u] °° us →⇩_{s}r'[x::=u'] °° us'" by (rule lemma1') hence "(Lam [x].r) ° u °° us →⇩_{s}r'[x::=u'] °° us'" by (rule better_sred_Beta) with ss r'' Lam_eq show "(Lam [x].r) °° ss →⇩_{s}r''" by (simp add: lam.inject alpha) qed next case (Beta x s ss t r) show ?case by (rule better_sred_Beta) (rule Beta)+ qed lemma rtrancl_beta_sred: assumes r: "r →⇩_{β}⇧^{*}r'" shows "r →⇩_{s}r'" using r by induct (iprover intro: refl_sred lemma4)+ subsection ‹Terms in normal form› lemma listsp_eqvt [eqvt]: assumes xs: "listsp p (xs::'a::pt_name list)" shows "listsp ((pi::name prm) ∙ p) (pi ∙ 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 inductive NF :: "lam ⇒ bool" where App: "listsp NF ts ⟹ NF (Var x °° ts)" | Abs: "NF t ⟹ NF (Lam [x].t)" equivariance NF nominal_inductive NF by (simp add: abs_fresh) lemma Abs_NF: assumes NF: "NF ((Lam [x].t) °° 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 text ‹ @{term NF} characterizes exactly the terms that are in normal form. › lemma NF_eq: "NF t = (∀t'. ¬ t →⇩_{β}t')" proof assume H: "NF t" show "∀t'. ¬ t →⇩_{β}t'" proof fix t' from H show "¬ t →⇩_{β}t'" proof (nominal_induct avoiding: t' rule: NF.strong_induct) case (App ts t) show ?case proof assume "Var t °° ts →⇩_{β}t'" then obtain rs where "ts [→⇩_{β}]⇩_{1}rs" by (iprover dest: head_Var_reduction) with App show False by (induct rs arbitrary: ts) (auto del: in_listspD) qed next case (Abs t x) show ?case proof assume "(Lam [x].t) →⇩_{β}t'" then show False using Abs by (cases rule: beta.strong_cases) (auto simp add: abs_fresh lam.inject alpha) qed qed qed next assume H: "∀t'. ¬ t →⇩_{β}t'" then show "NF t" proof (nominal_induct t rule: Apps_lam_induct) case (1 n ts) then have "∀ts'. ¬ ts [→⇩_{β}]⇩_{1}ts'" by (iprover intro: apps_preserves_betas) with 1(1) have "listsp NF ts" by (induct ts) (auto simp add: in_listsp_conv_set) then show ?case by (rule NF.App) next case (2 x u ts) show ?case proof (cases ts) case Nil thus ?thesis by (metis 2 NF.Abs abs foldl_Nil) next case (Cons r rs) have "(Lam [x].u) ° r →⇩_{β}u[x::=r]" .. then have "(Lam [x].u) ° r °° rs →⇩_{β}u[x::=r] °° rs" by (rule apps_preserves_beta) with Cons have "(Lam [x].u) °° ts →⇩_{β}u[x::=r] °° rs" by simp with 2 show ?thesis by iprover qed qed qed subsection ‹Leftmost reduction and weakly normalizing terms› inductive lred :: "lam ⇒ lam ⇒ bool" (infixl "→⇩_{l}" 50) and lredlist :: "lam list ⇒ lam list ⇒ bool" (infixl "[→⇩_{l}]" 50) where "s [→⇩_{l}] t ≡ listrelp (→⇩_{l}) s t" | Var: "rs [→⇩_{l}] rs' ⟹ Var x °° rs →⇩_{l}Var x °° rs'" | Abs: "r →⇩_{l}r' ⟹ (Lam [x].r) →⇩_{l}(Lam [x].r')" | Beta: "r[x::=s] °° ss →⇩_{l}t ⟹ (Lam [x].r) ° s °° ss →⇩_{l}t" lemma lred_imp_sred: assumes lred: "s →⇩_{l}t" shows "s →⇩_{s}t" using lred proof induct case (Var rs rs' x) then have "rs [→⇩_{s}] rs'" by induct (iprover intro: listrelp.intros)+ then show ?case by (rule sred.Var) next case (Abs r r' x) from ‹r →⇩_{s}r'› have "(Lam [x].r) °° [] →⇩_{s}(Lam [x].r') °° []" using listrelp.Nil by (rule better_sred_Abs) then show ?case by simp next case (Beta r x s ss t) from ‹r[x::=s] °° ss →⇩_{s}t› show ?case by (rule better_sred_Beta) qed inductive WN :: "lam ⇒ bool" where Var: "listsp WN rs ⟹ WN (Var n °° rs)" | Lambda: "WN r ⟹ WN (Lam [x].r)" | Beta: "WN ((r[x::=s]) °° ss) ⟹ WN (((Lam [x].r) ° s) °° ss)" lemma listrelp_imp_listsp1: assumes H: "listrelp (λx y. P x) xs ys" shows "listsp P xs" using H by induct auto lemma listrelp_imp_listsp2: assumes H: "listrelp (λx y. P y) xs ys" shows "listsp P ys" using H by induct auto lemma lemma5: assumes lred: "r →⇩_{l}r'" shows "WN r" and "NF r'" using lred by induct (iprover dest: listrelp_conj1 listrelp_conj2 listrelp_imp_listsp1 listrelp_imp_listsp2 intro: WN.intros NF.intros)+ lemma lemma6: assumes wn: "WN r" shows "∃r'. r →⇩_{l}r'" using wn proof induct case (Var rs n) then have "∃rs'. rs [→⇩_{l}] rs'" by induct (iprover intro: listrelp.intros)+ then show ?case by (iprover intro: lred.Var) qed (iprover intro: lred.intros)+ lemma lemma7: assumes r: "r →⇩_{s}r'" shows "NF r' ⟹ r →⇩_{l}r'" using r proof induct case (Var rs rs' x) from ‹NF (Var x °° rs')› have "listsp NF rs'" by cases simp_all with Var(1) have "rs [→⇩_{l}] rs'" proof induct case Nil show ?case by (rule listrelp.Nil) next case (Cons x y xs ys) hence "x →⇩_{l}y" and "xs [→⇩_{l}] ys" by (auto del: in_listspD) thus ?case by (rule listrelp.Cons) qed thus ?case by (rule lred.Var) next case (Abs x ss ss' r r') from ‹NF ((Lam [x].r') °° ss')› have ss': "ss' = []" by (rule Abs_NF) from Abs(4) have ss: "ss = []" using ss' by cases simp_all from ss' Abs have "NF (Lam [x].r')" by simp hence "NF r'" by (cases rule: NF.strong_cases) (auto simp add: abs_fresh lam.inject alpha) with Abs have "r →⇩_{l}r'" by simp hence "(Lam [x].r) →⇩_{l}(Lam [x].r')" by (rule lred.Abs) with ss ss' show ?case by simp next case (Beta x s ss t r) hence "r[x::=s] °° ss →⇩_{l}t" by simp thus ?case by (rule lred.Beta) qed lemma WN_eq: "WN t = (∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t')" proof assume "WN t" then have "∃t'. t →⇩_{l}t'" by (rule lemma6) then obtain t' where t': "t →⇩_{l}t'" .. then have NF: "NF t'" by (rule lemma5) from t' have "t →⇩_{s}t'" by (rule lred_imp_sred) then have "t →⇩_{β}⇧^{*}t'" by (rule lemma2) with NF show "∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t'" by iprover next assume "∃t'. t →⇩_{β}⇧^{*}t' ∧ NF t'" then obtain t' where t': "t →⇩_{β}⇧^{*}t'" and NF: "NF t'" by iprover from t' have "t →⇩_{s}t'" by (rule rtrancl_beta_sred) then have "t →⇩_{l}t'" using NF by (rule lemma7) then show "WN t" by (rule lemma5) qed end