header {* Definition of Lambda terms and convertibility *}theory Lambda imports Nominal2 beginlemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x" unfolding fresh_def by blastatom_decl varnominal_datatype lam = V "var"| Ap "lam" "lam" (infixl "\<cdot>" 98)| Lm x::"var" l::"lam" bind x in l ("\<integral> _. _" [97, 97] 99)nominal_primrec subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90)where "(V x)[y ::= s] = (if x = y then s else (V x))"| "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])"| "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])"proof auto fix a b :: lam and aa :: var and P assume "\<And>x y s. a = V x \<and> aa = y \<and> b = s \<Longrightarrow> P" "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P" "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P" then show "P" by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) (blast, blast, simp add: fresh_star_def)next fix x :: var and t and xa :: var and ya sa ta assume *: "eqvt_at subst_sumC (t, ya, sa)" "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)" "[[atom x]]lst. t = [[atom xa]]lst. ta" then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)" apply - apply (erule Abs_lst1_fcb) apply(simp (no_asm) add: Abs_fresh_iff) apply(drule_tac a="atom xa" in fresh_eqvt_at) apply(simp add: finite_supp) apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff) apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") apply(simp add: atom_eqvt eqvt_at_def) apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+ donenext show "eqvt subst_graph" unfolding eqvt_def subst_graph_def by (rule, perm_simp, rule)qedtermination by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size)lemma subst_eqvt[eqvt]: shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" by (induct t x s rule: subst.induct) (simp_all)lemma forget[simp]: shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" by (nominal_induct t avoiding: x s rule: lam.strong_induct) (auto simp add: lam.fresh fresh_at_base)lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t" by (simp add: fresh_def)lemma subst_id[simp]: "M [x ::= V x] = M" by (rule_tac lam="M" and c="x" in lam.strong_induct) (simp_all add: fresh_star_def lam.fresh fresh_Pair)inductive beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80)where bI: "(\<integral>x. M) \<cdot> N \<approx> M[x ::= N]"| b1: "M \<approx> M"| b2: "M \<approx> N \<Longrightarrow> N \<approx> M"| b3: "M \<approx> N \<Longrightarrow> N \<approx> L \<Longrightarrow> M \<approx> L"| b4: "M \<approx> N \<Longrightarrow> Z \<cdot> M \<approx> Z \<cdot> N"| b5: "M \<approx> N \<Longrightarrow> M \<cdot> Z \<approx> N \<cdot> Z"| b6: "M \<approx> N \<Longrightarrow> \<integral>x. M \<approx> \<integral>x. N"lemmas [trans] = b3equivariance betaend