156 lemma Lam_rsp: "A \<approx> B \<Longrightarrow> Lam [x]. A \<approx> Lam [x]. B"

   157   unfolding equ_def

   158   apply auto

   159   apply (rule_tac x="Lam [x]. r" in exI)

   160   apply (auto simp add: Lam_beta)

   161   done

   162 

   231 lemma subst_rsp_pre:

   232   "x \<approx> y \<Longrightarrow> xb \<approx> ya \<Longrightarrow> x [xa ::= xb] \<approx> y [xa ::= ya]"

   233   unfolding equ_def

   234   apply auto

   235   apply (rule_tac x="r [xa ::= ra]" in exI)

   236   apply (simp add: beta_subst)

   237   done

   238 

   331 

   332 lemma [quot_respect]:

   333   shows "(equ ===> op=) Supp Supp"

   334   unfolding fun_rel_def by (auto simp add: Supp_rsp)

   346 

   347 lemma supp_subst:

   348   shows "supp (t[x ::= s]) \<subseteq> (supp t - {atom x}) \<union> supp s"

   349   by (induct t x s rule: subst.induct) (auto simp add: lam.supp supp_at_base)

   350 

   351 lemma supp_beta: "x \<longrightarrow>b r \<Longrightarrow> supp r \<subseteq> supp x"

   352   apply (induct rule: beta.induct)

   353   apply (simp_all add: lam.supp)

   354   apply blast+

   355   using supp_subst by blast

   356 

   357 lemma supp_beta_star: "x \<longrightarrow>b* r \<Longrightarrow> supp r \<subseteq> supp x"

   358   apply (erule beta_star.induct)

   359   apply auto

   360   using supp_beta by blast

   361 

   362 lemma supp_equ: "x \<approx> y \<Longrightarrow> \<exists>z. z \<approx> x \<and> supp z \<subseteq> supp x \<inter> supp y"

   363   unfolding equ_def

   364   apply (simp (no_asm) only: equ_def[symmetric])

   365   apply (elim exE)

   366   apply (rule_tac x=r in exI)

   367   apply rule

   368   apply (metis bs1 equ_def)

   369   using supp_beta_star by blast

   370 

   371 lemma supp_psubset: "Supp x \<subset> supp x \<Longrightarrow> \<exists>t. t \<approx> x \<and> supp t \<subset> supp x"

   372 proof -

   373   assume "Supp x \<subset> supp x"

   374   then obtain a where "a \<in> supp x" "a \<notin> Supp x" by blast

   375   then obtain y where nin: "y \<approx> x" "a \<notin> supp y" unfolding Supp_def by blast

   376   then obtain t where eq: "t \<approx> x" "supp t \<subseteq> supp x \<inter> supp y"

   377     using supp_equ equ_sym by blast

   378   then have "supp t \<subset> supp x" using nin

   379     by (metis `(a\<Colon>atom) \<in> supp (x\<Colon>lam)` le_infE psubset_eq set_rev_mp)

   380   then show "\<exists>t. t \<approx> x \<and> supp t \<subset> supp x" using eq by blast

   381 qed

   382 

   383 lemma Supp_exists: "\<exists>t. supp t = Supp t \<and> t \<approx> x"

   384 proof -

   385   have "\<And>fs x. supp x = fs \<Longrightarrow> \<exists>t. supp t = Supp t \<and> t \<approx> x"

   386   proof -

   387     fix fs

   388     show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   389     proof (cases "finite fs")

   390       case True

   391       assume fs: "finite fs"

   392       then show "\<And>x. supp x = fs \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   393       proof (induct fs rule: finite_psubset_induct, clarify)

   394         fix A :: "atom set" fix x :: lam

   395         assume IH: "\<And>B xa. \<lbrakk>B \<subset> supp x; supp xa = B\<rbrakk> \<Longrightarrow> \<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> xa"

   396         show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   397         proof (cases "supp x = Supp x")

   398           assume "supp x = Supp x"

   399           then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   400             by (rule_tac x="x" in exI) (simp add: equ_refl)

   401         next

   402           assume "supp x \<noteq> Supp x"

   403           then have "Supp x \<subset> supp x" using Supp_supp by blast

   404           then obtain y where a1: "supp y \<subset> supp x" "y \<approx> x"

   405             using supp_psubset by blast

   406           then obtain t where "supp t = Supp t \<and> t \<approx> y"

   407             using IH[of "supp y" y] by blast

   408           then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" using a1 equ_trans

   409             by blast

   410         qed

   411       qed

   412     next

   413       case False

   414       fix x :: lam

   415       assume "supp x = fs" "infinite fs"

   416       then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x"

   417         by (auto simp add: finite_supp)

   418     qed simp

   419   qed

   420   then show "\<exists>t\<Colon>lam. supp t = Supp t \<and> t \<approx> x" by blast

   421 qed

   422 

   423 lemma subst3: "x \<noteq> y \<and> atom x \<notin> Supp s \<Longrightarrow> Lam [x]. t [y ::= s] \<approx> Lam [x]. (t [y ::= s])"

   424 proof -

   425   assume as: "x \<noteq> y \<and> atom x \<notin> Supp s"

   426   obtain s' where s: "supp s' = Supp s'" "s' \<approx> s" using Supp_exists[of s] by blast

   427   then have lhs: "Lam [x]. t [y ::= s] \<approx> Lam [x]. t [y ::= s']" using subst_rsp_pre equ_refl equ_sym by blast

   428   have supp: "Supp s' = Supp s" using Supp_rsp s(2) by blast

   429   have lhs_rhs: "Lam [x]. t [y ::= s'] = Lam [x]. (t [y ::= s'])"

   430     by (simp add: fresh_def supp_Pair s supp as supp_at_base)

   431   have "t [y ::= s'] \<approx> t [y ::= s]"

   432     using subst_rsp_pre[OF equ_refl s(2)] .

   433   with Lam_rsp have rhs: "Lam [x]. (t [y ::= s']) \<approx> Lam [x]. (t [y ::= s])" .

   434   show ?thesis 

   435     using lhs[unfolded lhs_rhs] rhs equ_trans by blast

   436 qed

   437 

   438 thm subst3[quot_lifted]