98 | "subst s t (App l r) = App (subst s t l) (subst s t r)"

    98 | "subst s t (App l r) = App (subst s t l) (subst s t r)"

    99 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"

    99 | "atom v \<sharp> (s, t) \<Longrightarrow> subst s t (Lam v b) = Lam v (subst s t b)"

   100 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"

   100 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"

   101 | "substa s t ANil = ANil"

   101 | "substa s t ANil = ANil"

   102 | "substa s t (ACons v t' as) = ACons v (subst v t t') as"

   102 | "substa s t (ACons v t' as) = ACons v (subst v t t') as"

   103 

   104 

   104 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r")

   105 (*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r")

   105 defer

   106 defer

   106 apply rule

   107 apply rule

   107 apply (simp only: Ex1_def)

   108 apply (simp only: Ex1_def)

   111 apply simp_all[3]

   112 apply simp_all[3]

   112 apply rule

   113 apply rule

   113 apply rule

   114 apply rule

   114 apply (rule subst_substa_graph.intros)*)

   115 apply (rule subst_substa_graph.intros)*)

   115 

   116 

   116 defer

   118 defer

   117 apply (case_tac x)

   119 apply (case_tac x)

   118 apply (case_tac a)

   120 apply (case_tac a)

   119 thm trm_assn.strong_exhaust(1)

   121 thm trm_assn.strong_exhaust(1)

   120 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))

   122 apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))

   161 

   163 

   162 alpha_bn (Acons s (subst a t t') a1)

   164 alpha_bn (Acons s (subst a t t') a1)

   163          (Acons s (subst a t t') a2)

   165          (Acons s (subst a t t') a2)

   164 

   166 

   165 ACons v (subst v t t') as"

   167 ACons v (subst v t t') as"

   167 end

   169 end

   168 

   170 

   169 

   171 

   170 

   172