theory Term1
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"
begin

atom_decl name

section {*** lets with binding patterns ***}

datatype rtrm1 =
  rVr1 "name"
| rAp1 "rtrm1" "rtrm1"
| rLm1 "name" "rtrm1"        --"name is bound in trm1"
| rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
and bp =
  BUnit
| BVr "name"
| BPr "bp" "bp"

print_theorems

(* to be given by the user *)

primrec 
  bv1
where
  "bv1 (BUnit) = {}"
| "bv1 (BVr x) = {atom x}"
| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"

setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
thm permute_rtrm1_permute_bp.simps

local_setup {*
  snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
  [[[], [], [(NONE, 0, 1)], [(SOME @{term bv1}, 0, 2)]],
  [[], [], []]] *}

notation
  alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
  alpha_bp ("_ \<approx>1b _" [100, 100] 100)
thm alpha_rtrm1_alpha_bp.intros
thm fv_rtrm1_fv_bp.simps[no_vars]

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases} ctxt)) ctxt)) *}
thm alpha1_inj

local_setup {*
snd o (build_eqvts @{binding bv1_eqvt} [@{term bv1}] [@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms bv1.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.inducts(2)})
*}

local_setup {*
snd o build_eqvts @{binding fv_rtrm1_fv_bp_eqvt} [@{term fv_rtrm1}, @{term fv_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] (@{thms fv_rtrm1_fv_bp.simps permute_rtrm1_permute_bp.simps}) @{thm rtrm1_bp.induct}
*}

ML {*
fun build_alpha_eqvts funs perms simps induct ctxt =
let
  val pi = Free ("p", @{typ perm});
  val types = map (domain_type o fastype_of) funs;
  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
  val args = map Free (indnames ~~ types);
  val args2 = map Free (indnames2 ~~ types);
  fun eqvtc ((alpha, perm), (arg, arg2)) =
    HOLogic.mk_imp (alpha $ arg $ arg2,
      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
  fun tac _ = (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps 
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
    THEN_ALL_NEW (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW
      (etac @{thm alpha_gen_compose_eqvt})) THEN_ALL_NEW
    (asm_full_simp_tac (HOL_ss addsimps 
      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))
) 1
  
in
  gl
end
*}ye

lemma alpha_gen_compose_eqvt:
  assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)"
  and     c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)"
  and     a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
  shows  "\<exists>pia. (g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f pia (g (pi \<bullet> e), pi \<bullet> s) \<and> P g pi d e t s R f pia"
  using b
  apply -
sorry

lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (p \<bullet> pi)) \<Longrightarrow> \<exists>pi. Q pi"
apply (erule exE)
apply (rule_tac x="pia \<bullet> pi" in exI)
by auto

prove {*
  build_alpha_eqvts [@{term alpha_rtrm1}, @{term alpha_bp}] [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"},@{term "permute :: perm \<Rightarrow> bp \<Rightarrow> bp"}] @{thms permute_rtrm1_permute_bp.simps alpha1_inj} @{thm alpha_rtrm1_alpha_bp.induct} @{context}
*}
apply(rule alpha_rtrm1_alpha_bp.induct)
apply(simp_all add: atom_eqvt alpha1_inj)
apply(erule exi)
apply(simp add: alpha_gen.simps)
apply(erule conjE)+
apply(rule conjI)
apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
apply(subst empty_eqvt[symmetric])
apply(subst insert_eqvt[symmetric])
apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric] set_eqvt[symmetric] empty_eqvt[symmetric] eqvts[symmetric])
apply(subst eqvts)
apply(subst eqvts)
apply(subst eqvts)
apply(subst eqvts)
apply(subst eqvts)
apply simp
apply(rule conjI)
apply(simp add: atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
thm eqvts
apply(simp add:eqvts)

thm insert_eqvt
apply(simp add: atom_eqvt[symmetric] Diff_eqvt[symmetric] insert_eqvt[symmetric])

apply(rule conjI)
thm atom_eqvt
apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
apply simp
apply(rule conjI)
apply(subst permute_eqvt[symmetric])
apply simp
apply(rule conjI)
apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1])
apply simp
apply(subst permute_eqvt[symmetric])
apply simp
apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1])
apply(simp)
thm permute_eq_iff[THEN iffD1]
apply(clarify)
apply(rule conjI)

apply(erule alpha_gen_compose_eqvt)

prefer 2
apply(erule conj_forward)
apply (simp add: eqvts)
apply(erule alpha_gen_compose_eqvt)
lemma alpha1_eqvt_proper[eqvt]:
  "pi \<bullet> (t \<approx>1 s) = ((pi \<bullet> t) \<approx>1 (pi \<bullet> s))"
  "pi \<bullet> (alpha_bp a b) = (alpha_bp (pi \<bullet> a) (pi \<bullet> b))"
  apply (simp_all only: eqvts)
  apply rule
  apply (simp_all add: alpha1_eqvt)
  apply (subst permute_minus_cancel(2)[symmetric,of "t" "pi"])
  apply (subst permute_minus_cancel(2)[symmetric,of "s" "pi"])
  apply (simp_all only: alpha1_eqvt)
  apply rule
  apply (simp_all add: alpha1_eqvt)
  apply (subst permute_minus_cancel(2)[symmetric,of "a" "pi"])
  apply (subst permute_minus_cancel(2)[symmetric,of "b" "pi"])
  apply (simp_all only: alpha1_eqvt)
done
thm eqvts_raw(1)

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_equivp}, []),
  (build_equivps [@{term alpha_rtrm1}, @{term alpha_bp}] @{thm rtrm1_bp.induct} @{thm alpha_rtrm1_alpha_bp.induct} @{thms rtrm1.inject bp.inject} @{thms alpha1_inj} @{thms rtrm1.distinct bp.distinct} @{thms alpha_rtrm1.cases alpha_bp.cases} @{thms alpha1_eqvt} ctxt)) ctxt)) *}
thm alpha1_equivp

local_setup  {* define_quotient_type [(([], @{binding trm1}, NoSyn), (@{typ rtrm1}, @{term alpha_rtrm1}))]
  (rtac @{thm alpha1_equivp(1)} 1) *}

local_setup {*
(fn ctxt => ctxt
 |> snd o (Quotient_Def.quotient_lift_const ("Vr1", @{term rVr1}))
 |> snd o (Quotient_Def.quotient_lift_const ("Ap1", @{term rAp1}))
 |> snd o (Quotient_Def.quotient_lift_const ("Lm1", @{term rLm1}))
 |> snd o (Quotient_Def.quotient_lift_const ("Lt1", @{term rLt1}))
 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm1", @{term fv_rtrm1})))
*}
print_theorems

local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}
local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}

lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]

setup {* define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}

lemmas
    permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]
and fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]
and fv_trm1_eqvt = fv_rtrm1_fv_bp_eqvt(1)[quot_lifted]
and alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemma supports:
  "(supp (atom x)) supports (Vr1 x)"
  "(supp t \<union> supp s) supports (Ap1 t s)"
  "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
  "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
  "{} supports BUnit"
  "(supp (atom x)) supports (BVr x)"
  "(supp a \<union> supp b) supports (BPr a b)"
apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
apply(rule_tac [!] allI)+
apply(rule_tac [!] impI)
apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
apply(simp_all add: fresh_atom)
done

lemma rtrm1_bp_fs:
  "finite (supp (x :: trm1))"
  "finite (supp (b :: bp))"
  apply (induct x and b rule: trm1_bp_inducts)
  apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
  apply(simp_all add: supp_atom)
  done

instance trm1 :: fs
apply default
apply (rule rtrm1_bp_fs(1))
done

lemma fv_eq_bv: "fv_bp bp = bv1 bp"
apply(induct bp rule: trm1_bp_inducts(2))
apply(simp_all)
done

lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
apply auto
apply (rule_tac x="(x \<rightleftharpoons> a)" in exI)
apply auto
done

lemma alpha_bp_eq_eq: "alpha_bp a b = (a = b)"
apply rule
apply (induct a b rule: alpha_rtrm1_alpha_bp.inducts(2))
apply (simp_all add: equivp_reflp[OF alpha1_equivp(2)])
done

lemma alpha_bp_eq: "alpha_bp = (op =)"
apply (rule ext)+
apply (rule alpha_bp_eq_eq)
done

lemma supp_fv:
  "supp t = fv_trm1 t"
  "supp b = fv_bp b"
apply(induct t and b rule: trm1_bp_inducts)
apply(simp_all)
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
apply(simp only: supp_at_base[simplified supp_def])
apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
apply(simp add: Collect_imp_eq Collect_neg_eq)
apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
apply(simp add: supp_Abs fv_trm1)
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
apply(simp add: alpha1_INJ)
apply(simp add: Abs_eq_iff)
apply(simp add: alpha_gen.simps)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
apply(simp (no_asm) add: supp_def permute_trm1)
apply(simp add: alpha1_INJ alpha_bp_eq)
apply(simp add: Abs_eq_iff)
apply(simp add: alpha_gen)
apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
apply(simp (no_asm) add: supp_def eqvts)
apply(fold supp_def)
apply(simp add: supp_at_base)
apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
done

lemma trm1_supp:
  "supp (Vr1 x) = {atom x}"
  "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"
  "supp (Lm1 x t) = (supp t) - {atom x}"
  "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"
by (simp_all add: supp_fv fv_trm1 fv_eq_bv)

lemma trm1_induct_strong:
  assumes "\<And>name b. P b (Vr1 name)"
  and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
  and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
  shows   "P a rtrma"
sorry

end