theory Terms

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

begin

atom_decl name

text {* primrec seems to be genarally faster than fun *}

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 ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}

thm permute_rtrm1_permute_bp.simps

local_setup {*

  snd o define_fv_alpha "Terms.rtrm1"

  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],

  [[], [[]], [[], []]]] *}

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

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

lemma alpha_bp_refl: "alpha_bp a a"

apply induct

apply (simp_all  add: alpha1_inj)

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: alpha_bp_refl)

done

lemma alpha_bp_eq: "alpha_bp = (op =)"

apply (rule ext)+

apply (rule alpha_bp_eq_eq)

done

ML {*

fun build_eqvts funs perms simps induct ctxt =

let

  val types = map (domain_type o fastype_of) funs;

  val fv_indnames = Datatype_Prop.make_tnames (map body_type types);

  val args = map Free (fv_indnames ~~ types);

  val perm_at = Const (@{const_name permute}, @{typ "perm \<Rightarrow> atom set \<Rightarrow> atom set"})

  fun eqvtc (fv, (arg, perm)) =

    HOLogic.mk_eq ((perm_at $ pi $ (fv $ arg)), (fv $ (perm $ pi $ arg)))

  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ (args ~~ perms))))

  fun tac _ = (indtac induct fv_indnames THEN_ALL_NEW

    (asm_full_simp_tac (HOL_ss addsimps 

      (@{thm atom_eqvt} :: (Nominal_ThmDecls.get_eqvts_thms ctxt) @ simps)))) 1

in

end

*}

*}

*}

lemma alpha1_eqvt:

  "t \<approx>1 s \<Longrightarrow> (pi \<bullet> t) \<approx>1 (pi \<bullet> s)"

  "alpha_bp a b \<Longrightarrow> alpha_bp (pi \<bullet> a) (pi \<bullet> b)"

  apply (induct t s and a b rule: alpha_rtrm1_alpha_bp.inducts)

  apply (simp_all add:eqvts alpha1_inj)

  apply (tactic {* 

    ALLGOALS (

      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

      (etac @{thm alpha_gen_compose_eqvt})

    ) *})

  apply (simp_all only: eqvts atom_eqvt)

  done

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

thm alpha_rtrm1_alpha_bp.induct

local_setup {* 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 {* 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 {* 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 {* 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 {* 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 {* 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 ["Terms.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_eqvt[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 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

section {*** lets with single assignments ***}

datatype rtrm2 =

  rVr2 "name"

| rAp2 "rtrm2" "rtrm2"

| rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"

| rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"

and rassign =

  rAs "name" "rtrm2"

(* to be given by the user *)

primrec 

  rbv2

where

  "rbv2 (rAs x t) = {atom x}"

setup {* snd o define_raw_perms ["rtrm2", "rassign"] ["Terms.rtrm2", "Terms.rassign"] *}

local_setup {* snd o define_fv_alpha "Terms.rtrm2"

  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term rbv2}, 0)]]],

   [[[], []]]] *}

notation

  alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and

  alpha_rassign ("_ \<approx>2b _" [100, 100] 100)

thm alpha_rtrm2_alpha_rassign.intros

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}

thm alpha2_inj

lemma alpha2_eqvt:

  "t \<approx>2 s \<Longrightarrow> (pi \<bullet> t) \<approx>2 (pi \<bullet> s)"

  "a \<approx>2b b \<Longrightarrow> (pi \<bullet> a) \<approx>2b (pi \<bullet> b)"

sorry

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_equivp}, []),

  (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}

thm alpha2_equivp

local_setup  {* define_quotient_type 

  [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),

   (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]

  ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}

local_setup {*

(fn ctxt => ctxt

 |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))

 |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))

 |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))

 |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))

 |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))

 |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))

*}

print_theorems

local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]

  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}

local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]

  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}

local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]

  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]

  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]

  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]

  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}

local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]

  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}

section {*** lets with many assignments ***}

datatype rtrm3 =

  rVr3 "name"

| rAp3 "rtrm3" "rtrm3"

| rLm3 "name" "rtrm3" --"bind (name) in (trm3)"

| rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"

and rassigns =

  rANil

| rACons "name" "rtrm3" "rassigns"

(* to be given by the user *)

primrec 

  bv3

where

  "bv3 rANil = {}"

| "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"

setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Terms.rtrm3", "Terms.rassigns"] *}

local_setup {* snd o define_fv_alpha "Terms.rtrm3"

  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],

   [[], [[], [], []]]] *}

print_theorems

notation

  alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and

  alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)

thm alpha_rtrm3_alpha_rassigns.intros

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}

thm alpha3_inj

lemma alpha3_eqvt:

  "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"

  "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"

sorry

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),

  (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}

thm alpha3_equivp

quotient_type

  trm3 = rtrm3 / alpha_rtrm3

and

  assigns = rassigns / alpha_rassigns

  by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))

section {*** lam with indirect list recursion ***}

datatype rtrm4 =

  rVr4 "name"

| rAp4 "rtrm4" "rtrm4 list"

| rLm4 "name" "rtrm4"  --"bind (name) in (trm)"

print_theorems

thm rtrm4.recs

(* there cannot be a clause for lists, as *)

(* permutations are  already defined in Nominal (also functions, options, and so on) *)

setup {* snd o define_raw_perms ["rtrm4"] ["Terms.rtrm4"] *}

(* "repairing" of the permute function *)

lemma repaired:

  fixes ts::"rtrm4 list"

  shows "permute_rtrm4_list p ts = p \<bullet> ts"

  apply(induct ts)

  apply(simp_all)

  done

thm permute_rtrm4_permute_rtrm4_list.simps

thm permute_rtrm4_permute_rtrm4_list.simps[simplified repaired]

local_setup {* snd o define_fv_alpha "Terms.rtrm4" [

  [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]], [[], [[], []]]  ] *}

print_theorems

notation

  alpha_rtrm4 ("_ \<approx>4 _" [100, 100] 100) and

  alpha_rtrm4_list ("_ \<approx>4l _" [100, 100] 100)

thm alpha_rtrm4_alpha_rtrm4_list.intros

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_inj}, []), (build_alpha_inj @{thms alpha_rtrm4_alpha_rtrm4_list.intros} @{thms rtrm4.distinct rtrm4.inject list.distinct list.inject} @{thms alpha_rtrm4.cases alpha_rtrm4_list.cases} ctxt)) ctxt)) *}

thm alpha4_inj

lemma alpha4_eqvt:

  "t \<approx>4 s \<Longrightarrow> (pi \<bullet> t) \<approx>4 (pi \<bullet> s)"

  "a \<approx>4l b \<Longrightarrow> (pi \<bullet> a) \<approx>4l (pi \<bullet> b)"

sorry

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha4_equivp}, []),

  (build_equivps [@{term alpha_rtrm4}, @{term alpha_rtrm4_list}] @{thm rtrm4.induct} @{thm alpha_rtrm4_alpha_rtrm4_list.induct} @{thms rtrm4.inject list.inject} @{thms alpha4_inj} @{thms rtrm4.distinct list.distinct} @{thms alpha_rtrm4_list.cases alpha_rtrm4.cases} @{thms alpha4_eqvt} ctxt)) ctxt)) *}

thm alpha4_equivp

quotient_type 

  qrtrm4 = rtrm4 / alpha_rtrm4 and

  qrtrm4list = "rtrm4 list" / alpha_rtrm4_list

  by (simp_all add: alpha4_equivp)

datatype rtrm5 =

  rVr5 "name"

| rAp5 "rtrm5" "rtrm5"

| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"

and rlts =

  rLnil

| rLcons "name" "rtrm5" "rlts"

primrec

  rbv5

where

  "rbv5 rLnil = {}"

| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"

setup {* snd o define_raw_perms ["rtrm5", "rlts"] ["Terms.rtrm5", "Terms.rlts"] *}

print_theorems

local_setup {* snd o define_fv_alpha "Terms.rtrm5" [

  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ] *}

print_theorems

(* Alternate version with additional binding of name in rlts in rLcons *)

(*local_setup {* snd o define_fv_alpha "Terms.rtrm5" [

  [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[(NONE,0)], [], [(NONE,0)]]]  ] *}

print_theorems*)

notation

  alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and

  alpha_rlts ("_ \<approx>l _" [100, 100] 100)

thm alpha_rtrm5_alpha_rlts.intros

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases} ctxt)) ctxt)) *}

thm alpha5_inj

lemma rbv5_eqvt[eqvt]:

  "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"

  apply (induct x)

  apply (simp_all add: eqvts atom_eqvt)

  done

lemma fv_rtrm5_rlts_eqvt[eqvt]:

  "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"

  "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"

  apply (induct x and l)

  apply (simp_all add: eqvts atom_eqvt)

  done

lemma alpha5_eqvt:

  "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)"

  "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)"

  apply (induct rule: alpha_rtrm5_alpha_rlts.inducts)

  apply (simp_all add: alpha5_inj)

  apply (tactic {* 

    ALLGOALS (

      TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI) THEN_ALL_NEW

      (etac @{thm alpha_gen_compose_eqvt})

    ) *})

  apply (simp_all only: eqvts atom_eqvt)

  done

local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_equivp}, []),

  (build_equivps [@{term alpha_rtrm5}, @{term alpha_rlts}] @{thm rtrm5_rlts.induct} @{thm alpha_rtrm5_alpha_rlts.induct} @{thms rtrm5.inject rlts.inject} @{thms alpha5_inj} @{thms rtrm5.distinct rlts.distinct} @{thms alpha_rtrm5.cases alpha_rlts.cases} @{thms alpha5_eqvt} ctxt)) ctxt)) *}

thm alpha5_equivp

quotient_type

  trm5 = rtrm5 / alpha_rtrm5

and

  lts = rlts / alpha_rlts

  by (auto intro: alpha5_equivp)

local_setup {*

(fn ctxt => ctxt

 |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))

 |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))

 |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))

 |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))

 |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))

 |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))

 |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5})))

*}

print_theorems

lemma alpha5_rfv:

  "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"