theory SingleLet
imports "../NewParser"
begin

atom_decl name

declare [[STEPS = 10]]

nominal_datatype trm =
  Var "name"
| App "trm" "trm"
| Lam x::"name" t::"trm"  bind_set x in t
| Let a::"assg" t::"trm"  bind_set "bn a" in t
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
and assg =
  As "name" "name" "trm" "name"
binder
  bn::"assg \<Rightarrow> atom set"
where
  "bn (As x y t z) = {atom x}"

thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
thm alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases


lemma [eqvt]:
 "p \<bullet> alpha_trm_raw x1 y1  = alpha_trm_raw (p \<bullet> x1) (p \<bullet> y1)"
 "p \<bullet> alpha_assg_raw x2 y2 = alpha_assg_raw (p \<bullet> x2) (p \<bullet> y2)"
 "p \<bullet> alpha_bn_raw x3 y3   = alpha_bn_raw (p \<bullet> x3) (p \<bullet> y3)"
sorry

lemmas ii = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros
lemmas cc = alpha_trm_raw.cases alpha_assg_raw.cases alpha_bn_raw.cases

ML {*
length @{thms cc}
*}

ML {*
  val pp = ["SingleLet.alpha_trm_raw", "SingleLet.alpha_assg_raw", "SingleLet.alpha_bn_raw"]
*}

lemma exi_sum: "\<exists>(q :: perm). P q \<Longrightarrow> \<exists>q. Q q \<Longrightarrow> (\<And>p q. P p \<Longrightarrow> Q q \<Longrightarrow> R (p + q)) \<Longrightarrow> \<exists>r. R r"
apply(erule exE)+
apply(rule_tac x="q + qa" in exI)
apply(simp)
done

lemma alpha_gen_compose_trans:
  assumes b: "(as, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (bs, s)"
  shows "(\<forall>x. R s x \<longrightarrow> R (pi \<bullet> t) x)"
  using b
  by (simp add: alphas)

lemma test:
  assumes b: "(as, t) \<approx>gen R f pi (bs, s)"
  shows "R (pi \<bullet> t) s"
  using b
  by (simp add: alphas)

lemma alpha_gen_trans_eqvt:
  assumes a: "(bs, x) \<approx>gen R f p (cs, y)" and a1: "(cs, y) \<approx>gen R f q (ds, z)"
  and b: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
  shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
  sorry


lemma
 "alpha_trm_raw x1 y1  \<Longrightarrow> (\<And>z1. alpha_trm_raw y1 z1 \<Longrightarrow> alpha_trm_raw x1 z1)"
 "alpha_assg_raw x2 y2 \<Longrightarrow> (\<And>z2. alpha_assg_raw y2 z2 \<Longrightarrow> alpha_assg_raw x2 z2)"
 "alpha_bn_raw x3 y3   \<Longrightarrow> (\<And>z3. alpha_bn_raw y3 z3 \<Longrightarrow> alpha_bn_raw x3 z3)"
apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
(* 8 *)
prefer 8
thm alpha_bn_raw.cases
apply(rotate_tac -1)
apply(erule alpha_bn_raw.cases)
apply(simp_all)[6]


apply(rotate_tac -1)
apply(erule cc)
apply(simp_all)[6]
apply(rule ii) 
apply(simp)
(* 1 *)
apply(rotate_tac -1)
apply(erule cc)
apply(simp_all)[6]
apply(rule ii) 
apply(simp)
apply(simp)
(* 2 *)
apply(rotate_tac -1)
apply(erule cc)
apply(simp_all)[6]
apply(rule ii)
apply(erule exE)+
apply(rule_tac x="pa + p" in exI)
apply(rule alpha_gen_trans_eqvt)
prefer 2
apply(assumption)
apply(simp add: alphas)
apply(metis)
apply(drule test)
apply(simp)
(* 3 *)
apply(rotate_tac -1)
apply(erule cc)
apply(simp_all)[6]
apply(rule ii)
apply(erule exE)+
apply(rule_tac x="pa + p" in exI)
apply(rule alpha_gen_trans_eqvt)
prefer 2
apply(assumption)
apply(simp add: alphas)
apply(metis)
apply(drule alpha_gen_compose_trans)
apply(simp)
apply(simp)
(* 4 *)
apply(rotate_tac -1)
apply(erule cc)
apply(simp_all)[6]
apply(rule ii)
apply(erule exE)+
apply(rule_tac x="pa + p" in exI)
apply(rule alpha_gen_trans_eqvt)
prefer 2
apply(assumption)
prefer 2
apply(drule test)
apply(simp add: prod_alpha_def)
apply(simp add: alphas)

apply(drule alpha_gen_compose_trans)
apply(drule_tac x="(- pa \<bullet> trm_rawaa)" in spec)
apply(simp)
apply(simp)
(* 4 *)
apply(assumption) 
apply(simp)
apply(simp)

(* 3 *)

(* 4 *)

(* 5 *)

(* 6 *)

(* 7 *)

(* 8 *)

(* 9 *)
done

ML {* Inductive.the_inductive *}
thm trm_assg.fv
thm trm_assg.supp
thm trm_assg.eq_iff
thm trm_assg.bn
thm trm_assg.perm
thm trm_assg.induct
thm trm_assg.inducts
thm trm_assg.distinct
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}

(* TEMPORARY
thm trm_assg.fv[simplified trm_assg.supp(1-2)]
*)

end