--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/LetRecFunNo.thy	Tue Apr 03 16:38:56 2012 +0200
@@ -0,0 +1,299 @@
+theory Let
+imports "../Nominal2"
+begin
+
+atom_decl name
+
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Let as::"assn" t::"trm"   binds "bn as" in as t
+and assn =
+  ANil
+| ACons "name" "trm" "assn"
+binder
+  bn
+where
+  "bn ANil = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
+
+nominal_primrec substrec where
+  "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))"
+| "substrec fa fl fd y z (App l r) = fa l r"
+| "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
+   substrec fa fl fd y z (Let as t) = fl as t"
+| "(set (bn as) \<sharp>* (Let as t, y, z) \<and> \<not>(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow>
+   substrec fa fl fd y z (Let as t) = fd"
+  unfolding eqvt_def substrec_graph_def
+  apply (rule, perm_simp, rule, rule)
+  apply (case_tac x)
+  apply (rule_tac y="f" and c="(f, d, e)" in trm_assn.strong_exhaust(1))
+  apply metis
+  apply metis
+  apply (thin_tac "\<And>fa fl fd y z xa. x = (fa, fl, fd, y, z, Var xa) \<Longrightarrow> P")
+  apply (thin_tac "\<And>fa fl fd y z l r. x = (fa, fl, fd, y, z, App l r) \<Longrightarrow> P")
+  apply (drule_tac x="assn" in meta_spec)+
+  apply (drule_tac x="trm" in meta_spec)+
+  apply (drule_tac x="d" in meta_spec)+
+  apply (drule_tac x="e" in meta_spec)+
+  apply (drule_tac x="b" in meta_spec)+
+  apply (drule_tac x="a" in meta_spec)+
+  apply (drule_tac x="c" in meta_spec)+
+  apply (case_tac "(\<forall>bs s.
+             set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow>
+             Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s)")
+  apply simp
+  apply (thin_tac "set (bn assn) \<sharp>* (Let assn trm, d, e) \<and>
+         (\<forall>bs s.
+             set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow>
+             Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s) \<Longrightarrow>
+         x = (a, b, c, d, e, Let.Let assn trm) \<Longrightarrow> P")
+  apply simp
+  apply simp_all
+  apply clarify
+  apply metis
+  done
+termination (eqvt) by lexicographic_order
+
+nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where
+  "substarec fac ANil = ANil"
+| "substarec fac (ACons x t as) = fac x t as"
+  unfolding eqvt_def substarec_graph_def
+  apply (rule, perm_simp, rule, rule)
+  apply (case_tac x)
+  apply (rule_tac y="b" in trm_assn.exhaust(2))
+  apply auto
+  done
+termination (eqvt) by lexicographic_order
+
+lemma [fundef_cong]:
+ "(\<And>t1 t2. t = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow>
+  (\<And>as s. t = Let as s \<Longrightarrow> fl as s = fl' as s) \<Longrightarrow>
+  substrec fa fl fd y z t = substrec fa' fl' fd y z t"
+  apply (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1))
+  apply auto
+  apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let assn trm = Let bs s \<longrightarrow> fl assn trm = fl bs s)")
+  apply (subst substrec.simps(3)) apply simp
+  apply (subst substrec.simps(3)) apply simp
+  apply metis
+  apply (subst substrec.simps(4)) apply simp
+  apply (subst substrec.simps(4)) apply simp_all
+  done
+
+lemma [fundef_cong]:
+ "(\<And>x s as. t = ACons x s as \<Longrightarrow> fac x s as = fac' x s as) \<Longrightarrow>
+  substarec fac t = substarec fac' t"
+  by (rule_tac y="t" in trm_assn.exhaust(2)) simp_all
+
+function
+    subst  :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm"
+and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn"
+where
+  [simp del]: "subst y z t = substrec
+     (\<lambda>l r. App (subst y z l) (subst y z r))
+     (\<lambda>as t. Let (substa y z as) (subst y z t))
+     (Let (ACons y (Var y) ANil) (Var y)) y z t"
+| [simp del]: "substa y z t = substarec
+     (\<lambda>x t as. ACons x (subst y z t) (substa y z as)) t"
+  by pat_completeness auto
+
+termination by lexicographic_order
+
+lemma testl:
+  assumes a: "\<exists>y. f x = Inl y"
+  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
+using a
+apply clarify
+apply(frule_tac p="p" in permute_boolI)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst (asm) permute_fun_app_eq)
+back
+apply(simp)
+done
+
+lemma testr:
+  assumes a: "\<exists>y. f x = Inr y"
+  shows "(p \<bullet> (Sum_Type.Projr (f x))) = Sum_Type.Projr ((p \<bullet> f) (p \<bullet> x))"
+using a
+apply clarify
+apply(frule_tac p="p" in permute_boolI)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst (asm) permute_fun_app_eq)
+back
+apply(simp)
+done
+
+lemma permute_move: "p \<bullet> x = y \<longleftrightarrow> x = -p \<bullet> y"
+  by (metis eqvt_bound unpermute_def)
+
+lemma "subst_substa_graph x t \<Longrightarrow> subst_substa_graph (p \<bullet> x) (p \<bullet> t)"
+proof (induct arbitrary: p rule: subst_substa_graph.induct)
+fix f y z t p
+assume a: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t1)) (p \<bullet> f (Inl (y, z, t1)))"
+   and b: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t2)) (p \<bullet> f (Inl (y, z, t2)))"
+   and c: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inr (y, z, as)) (p \<bullet> f (Inr (y, z, as)))"
+   and d: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, s)) (p \<bullet> f (Inl (y, z, s)))"
+   then show "subst_substa_graph (p \<bullet> Inl (y, z, t))
+           (p \<bullet> Inl (substrec
+                      (\<lambda>l r. App (Sum_Type.Projl (f (Inl (y, z, l))))
+                              (Sum_Type.Projl (f (Inl (y, z, r)))))
+                      (\<lambda>as t. Let.Let (Sum_Type.Projr (f (Inr (y, z, as))))
+                               (Sum_Type.Projl (f (Inl (y, z, t)))))
+                      (Let.Let (ACons y (Var y) ANil) (Var y)) y z t))"
+     proof (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1))
+       fix name
+       assume "t = Var name"
+       then show ?thesis
+         apply (simp add: eqvts split del: if_splits)
+         apply (simp only:  trm_assn.perm_simps)
+         apply (rule subst_substa_graph.intros(1)[of "Var (p \<bullet> name)" "p \<bullet> y" "p \<bullet> z", simplified])
+         by simp_all
+     next
+       fix trm1 trm2
+       assume e: "t = App trm1 trm2"
+       then show ?thesis
+         apply (simp add: eqvts)
+         apply (subst testl) back
+         apply (rule subst_substa_graph.cases[OF a[OF e, of 0, simplified]])
+         apply metis apply simp
+         apply (subst testl) back
+         apply (rule subst_substa_graph.cases[OF b[OF e, of 0, simplified]])
+         apply metis apply (simp add: eqvts)
+         apply (simp only: Inl_eqvt) apply simp
+         apply (rule subst_substa_graph.intros(1)[of "App (p \<bullet> trm1) (p \<bullet> trm2)" "p \<bullet> y" "p \<bullet> z", simplified])
+         apply simp_all apply clarify
+         using a[OF e, simplified Inl_eqvt, simplified]
+         apply (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps)
+         apply clarify
+         using b[OF e, simplified Inl_eqvt, simplified]
+         by (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps)
+     next
+       fix assn trm
+       assume e: "t = Let.Let assn trm" and f: "set (bn assn) \<sharp>* (t, y, z)"
+       then show ?thesis
+         apply (simp add: eqvts)
+         apply (simp only: permute_fun_def)
+         apply (simp only: eqvts permute_minus_cancel)
+         apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let.Let bs s, p \<bullet> y, p \<bullet> z) \<longrightarrow>
+                 Let.Let (p \<bullet> assn) (p \<bullet> trm) = Let.Let bs s \<longrightarrow>
+                 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> p \<bullet> assn))))
+                  (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> p \<bullet> trm)))) =
+                 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> bs))))
+                  (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> s)))))")
+         prefer 2
+         apply (subst substrec.simps(4))
+         apply rule
+         apply (simp add: fresh_star_Pair)
+         apply (intro conjI)
+         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         apply assumption
+         prefer 2
+         apply (subst substrec.simps(3))
+         apply rule
+         apply (simp add: fresh_star_Pair)
+         apply (intro conjI)
+         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         apply assumption
+(*       The following subgoal is motivated by:
+   thm subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified]*)
+         apply (subgoal_tac "subst_substa_graph (Inl (p \<bullet> y, p \<bullet> z, Let.Let (p \<bullet> assn) (p \<bullet> trm)))
+           (Inl (substrec
+           (\<lambda>l r. App (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, l))))
+                   (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, r)))))
+           (\<lambda>as t. Let.Let (Sum_Type.Projr ((p \<bullet> f) (Inr (p \<bullet> y, p \<bullet> z, as))))
+                    (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, t)))))
+           (Let.Let (ACons (p \<bullet> y) (Var (p \<bullet> y)) ANil) (Var (p \<bullet> y))) (p \<bullet> y) (p \<bullet> z)
+           (Let.Let (p \<bullet> assn) (p \<bullet> trm))))")
+         apply (subst (asm) substrec.simps(3))
+         apply rule
+         apply (simp add: fresh_star_Pair)
+         apply (intro conjI)
+         apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4))
+         (* We don't have equivariance of Projl/Projr at the arbitrary 'bs' point *)
+         defer
+         apply (subst testr) back
+         apply (rule subst_substa_graph.cases[OF c[OF e, of 0, simplified]])
+         apply simp apply simp
+         apply (subst testl) back
+         apply (rule subst_substa_graph.cases[OF d[OF e, of 0, simplified]])
+         apply simp apply simp apply simp
+         apply (rule subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified])
+         apply simp apply simp (* These two should follow by d for arbitrary 'as' point *)
+         defer defer
+         sorry
+     qed
+   next
+     fix f y z t p
+     show "subst_substa_graph (p \<bullet> Inr (y, z, t)) (p \<bullet> Inr (substarec (\<lambda>x t as. ACons
+       x (Sum_Type.Projl (f (Inl (y, z, t)))) (Sum_Type.Projr (f (Inr (y, z, as))))) t))"
+       sorry
+   qed
+
+(* Will follow from above and accp *)
+lemma [eqvt]:
+  "p \<bullet> (subst y z t) = subst (p \<bullet> y) (p \<bullet> z) (p \<bullet> t)"
+  "p \<bullet> (substa y z t2) = substa (p \<bullet> y) (p \<bullet> z) (p \<bullet> t2)"
+  sorry
+
+lemma substa_simps[simp]:
+  "substa y z ANil = ANil"
+  "substa y z (ACons x t as) = ACons x (subst y z t) (substa y z as)"
+  apply (subst substa.simps) apply (subst substarec.simps) apply rule
+  apply (subst substa.simps) apply (subst substarec.simps) apply rule
+  done
+
+lemma bn_substa: "bn (substa y z t) = bn t"
+  by (induct t rule: trm_assn.inducts(2)) (simp_all add: trm_assn.bn_defs)
+
+lemma fresh_fun_eqvt_app3:
+  assumes e: "eqvt f"
+  shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z"
+  using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types))
+
+lemma
+  "subst y z (Var x) = (if (y = x) then z else (Var x))"
+  "subst y z (App l r) = App (subst y z l) (subst y z r)"
+  "set (bn as) \<sharp>* (Let as t, y, z) \<Longrightarrow> subst y z (Let as t) = Let (substa y z as) (subst y z t)"
+  apply (subst subst.simps) apply (subst substrec.simps) apply rule
+  apply (subst subst.simps) apply (subst substrec.simps) apply rule
+  apply (subst subst.simps) apply (subst substrec.simps) apply auto
+  apply (subst (asm) Abs_eq_iff2)
+  apply clarify
+  apply (simp add: alphas bn_substa)
+  apply (rule_tac s="p \<bullet> ([bn as]lst. (substa y z as, subst y z t))" in trans)
+  apply (rule sym)
+  defer
+  apply (simp add: eqvts)
+  apply (subgoal_tac "supp p \<sharp>* y")
+  apply (subgoal_tac "supp p \<sharp>* z")
+  apply (simp add: perm_supp_eq)
+  apply (simp add: fresh_Pair fresh_star_def)
+  apply blast
+  apply (simp add: fresh_Pair fresh_star_def)
+  apply blast
+  apply (rule perm_supp_eq)
+  apply (simp add: fresh_star_Pair)
+  apply (simp add: fresh_star_def Abs_fresh_iff)
+  apply (auto)
+  apply (simp add: bn_substa fresh_Pair)
+  apply (rule)
+  apply (rule fresh_fun_eqvt_app3[of substa])
+  apply (simp add: eqvt_def eqvts_raw)
+  apply (metis (lifting) Diff_partition Un_iff)
+  apply (metis (lifting) Diff_partition Un_iff)
+  apply (simp add: fresh_def trm_assn.supp)
+  apply (metis (lifting) DiffI UnI1 supp_Pair)
+  apply (rule fresh_fun_eqvt_app3[of subst])
+  apply (simp add: eqvt_def eqvts_raw)
+  apply (metis (lifting) Diff_partition Un_iff)
+  apply (metis (lifting) Diff_partition Un_iff)
+  apply (simp add: fresh_def trm_assn.supp)
+  by (metis Diff_iff Un_iff supp_Pair)
+
+end