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