theory Terms

imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"

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"

(* to be given by the user *)

primrec 

  bv1

where

  "bv1 (BUnit) = {}"

| "bv1 (BVr x) = {atom x}"

local_setup {* define_raw_fv "Terms.rtrm1"

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

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

print_theorems

setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Terms.rtrm1", "Terms.bp"] *}

inductive

  alpha1 :: "rtrm1 \<Rightarrow> rtrm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)"

| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2"

| a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s"

| a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2"

lemma alpha1_inj:

"(rVr1 a \<approx>1 rVr1 b) = (a = b)"

"(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"

"(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 fv_rtrm1 pi ({atom ab}, s)))"

"(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 fv_rtrm1 pi ((bv1 b2), s2))))"

apply -

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

apply rule apply (erule alpha1.cases) apply (simp_all add: alpha1.intros)

done

(* Shouyld we derive it? But bv is given by the user? *)

lemma bv1_eqvt[eqvt]:

  shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"

  apply (induct x)

done

lemma fv_rtrm1_eqvt[eqvt]:

    "(pi\<bullet>fv_rtrm1 t) = fv_rtrm1 (pi\<bullet>t)"

    "(pi\<bullet>fv_bp b) = fv_bp (pi\<bullet>b)"

  apply (induct t and b)

  apply (simp_all add: insert_eqvt atom_eqvt empty_eqvt union_eqvt Diff_eqvt bv1_eqvt)

  done

lemma alpha1_eqvt:

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

  apply (induct t s rule: alpha1.inducts)

  apply (simp_all add:eqvts alpha1_inj)

  apply (erule exE)

  apply (rule_tac x="pi \<bullet> pia" in exI)

  apply (simp add: alpha_gen)

  apply(erule conjE)+

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

  apply(simp add: atom_eqvt Diff_eqvt insert_eqvt empty_eqvt fv_rtrm1_eqvt)

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

  apply(simp add: atom_eqvt Diff_eqvt fv_rtrm1_eqvt insert_eqvt empty_eqvt)

  apply(simp add: permute_eqvt[symmetric])

  apply (erule exE)

  apply (rule_tac x="pi \<bullet> pia" in exI)

  apply (simp add: alpha_gen)

  apply(erule conjE)+

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])

  apply(simp add: fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

  apply(rule conjI)

  apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])

  apply(simp add: atom_eqvt fv_rtrm1_eqvt Diff_eqvt bv1_eqvt)

  apply(simp add: permute_eqvt[symmetric])

  done

lemma alpha1_equivp: "equivp alpha1" 

  sorry

quotient_type trm1 = rtrm1 / alpha1

  by (rule alpha1_equivp)

quotient_definition

  "Vr1 :: name \<Rightarrow> trm1"

is

  "rVr1"

quotient_definition

  "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"

is

  "rAp1"

quotient_definition

  "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1"

is

  "rLm1"

quotient_definition

  "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1"

is

  "rLt1"

quotient_definition

  "fv_trm1 :: trm1 \<Rightarrow> atom set"

is

  "fv_rtrm1"

lemma alpha_rfv1:

  shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"

  apply(induct rule: alpha1.induct)

  apply(simp_all add: alpha_gen.simps)

  sorry

lemma [quot_respect]:

 "(op = ===> alpha1) rVr1 rVr1"

 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"

 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"

 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"

apply (auto simp add: alpha1_inj)

apply (rule_tac x="0" in exI)

apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)

apply (rule_tac x="0" in exI)

apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)

done

lemma [quot_respect]:

  "(op = ===> alpha1 ===> alpha1) permute permute"

  by (simp add: alpha1_eqvt)

lemma [quot_respect]:

  "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"

  by (simp add: alpha_rfv1)

lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]

lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]

instantiation trm1 and bp :: pt

begin

quotient_definition

  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"

is

  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"

lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]

instance

apply default

apply(induct_tac [!] x rule: trm1_bp_inducts(1))

apply(simp_all)

done

end

lemmas fv_trm1 = fv_rtrm1_fv_bp.simps[quot_lifted]

lemmas fv_trm1_eqvt = fv_rtrm1_eqvt[quot_lifted]

lemmas alpha1_INJ = alpha1_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

lemma lm1_supp_pre:

  shows "(supp (atom x, t)) supports (Lm1 x t) "

apply(simp add: supports_def)

apply(fold fresh_def)

apply(simp add: fresh_Pair swap_fresh_fresh)

apply(clarify)

apply(subst swap_at_base_simps(3))

apply(simp_all add: fresh_atom)

done

lemma lt1_supp_pre:

  shows "(supp (x, t, s)) supports (Lt1 t x s) "

apply(simp add: supports_def)

apply(fold fresh_def)

apply(simp add: fresh_Pair swap_fresh_fresh)

done

lemma bp_supp: "finite (supp (bp :: bp))"

  apply (induct bp)

  apply(simp_all add: supp_def)

  apply (fold supp_def)

  apply (simp add: supp_at_base)

  apply(simp add: Collect_imp_eq)

  apply(simp add: Collect_neg_eq[symmetric])

  apply (fold supp_def)

  apply (simp)

  done

instance trm1 :: fs

apply default

apply(induct_tac x rule: trm1_bp_inducts(1))

apply(simp_all)

apply(simp add: supp_def alpha1_INJ eqvts)

apply(simp add: supp_def[symmetric] supp_at_base)

apply(simp only: supp_def alpha1_INJ eqvts permute_trm1)

apply(simp add: Collect_imp_eq Collect_neg_eq)

apply(rule supports_finite)

apply(rule lm1_supp_pre)

apply(simp add: supp_Pair supp_atom)

apply(rule supports_finite)

apply(rule lt1_supp_pre)

apply(simp add: supp_Pair supp_atom bp_supp)

done

lemma supp_fv:

  shows "supp t = fv_trm1 t"

apply(induct t rule: trm1_bp_inducts(1))

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)

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(simp (no_asm) add: supp_def)

apply(simp add: alpha1_INJ)

apply(simp add: Abs_eq_iff)

apply(simp add: alpha_gen)

apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt)

apply(simp add: Collect_imp_eq Collect_neg_eq)

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)"

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"

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}"

local_setup {* define_raw_fv "Terms.rtrm2"

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

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

print_theorems

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

inductive

  alpha2 :: "rtrm2 \<Rightarrow> rtrm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)

and

  alpha2a :: "rassign \<Rightarrow> rassign \<Rightarrow> bool" ("_ \<approx>2a _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (rVr2 a) \<approx>2 (rVr2 b)"

| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> rAp2 t1 s1 \<approx>2 rAp2 t2 s2"

| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha2 fv_rtrm2 pi ({atom b}, s))) \<Longrightarrow> rLm2 a t \<approx>2 rLm2 b s"

| a4: "\<lbrakk>\<exists>pi. ((rbv2 bt, t) \<approx>gen alpha2 fv_rtrm2 pi ((rbv2 bs), s));

        \<exists>pi. ((rbv2 bt, bt) \<approx>gen alpha2a fv_rassign pi (rbv2 bs, bs))\<rbrakk>

        \<Longrightarrow> rLt2 bt t \<approx>2 rLt2 bs s"

| a5: "\<lbrakk>a = b; t \<approx>2 s\<rbrakk> \<Longrightarrow> rAs a t \<approx>2a rAs b s" (* This way rbv2 can be lifted *)

lemma alpha2_equivp:

  "equivp alpha2"

  "equivp alpha2a"

  sorry

quotient_type

  trm2 = rtrm2 / alpha2

and

  assign = rassign / alpha2a

  by (auto intro: alpha2_equivp)

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

datatype trm3 =

  Vr3 "name"

| Ap3 "trm3" "trm3"

| Lm3 "name" "trm3" --"bind (name) in (trm3)"

| Lt3 "assigns" "trm3" --"bind (bv3 assigns) in (trm3)"

and assigns =

  ANil

| ACons "name" "trm3" "assigns"

(* to be given by the user *)

primrec 

  bv3

where

  "bv3 ANil = {}"

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

local_setup {* define_raw_fv "Terms.trm3"

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

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

print_theorems

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

inductive

  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [100, 100] 100)

and

  alpha3a :: "assigns \<Rightarrow> assigns \<Rightarrow> bool" ("_ \<approx>3a _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (Vr3 a) \<approx>3 (Vr3 b)"

| a2: "\<lbrakk>t1 \<approx>3 t2; s1 \<approx>3 s2\<rbrakk> \<Longrightarrow> Ap3 t1 s1 \<approx>3 Ap3 t2 s2"

| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha3 fv_rtrm3 pi ({atom b}, s))) \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"

| a4: "\<lbrakk>\<exists>pi. ((bv3 bt, t) \<approx>gen alpha3 fv_trm3 pi ((bv3 bs), s));

        \<exists>pi. ((bv3 bt, bt) \<approx>gen alpha3a fv_assign pi (bv3 bs, bs))\<rbrakk>

        \<Longrightarrow> Lt3 bt t \<approx>3 Lt3 bs s"

| a5: "ANil \<approx>3a ANil"

| a6: "\<lbrakk>a = b; t \<approx>3 s; tt \<approx>3a st\<rbrakk> \<Longrightarrow> ACons a t tt \<approx>3a ACons b s st"

lemma alpha3_equivp:

  "equivp alpha3"

  "equivp alpha3a"

  sorry

quotient_type

  qtrm3 = trm3 / alpha3

and

  qassigns = assigns / alpha3a

  by (auto intro: alpha3_equivp)

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

datatype trm4 =

  Vr4 "name"

| Ap4 "trm4" "trm4 list"

| Lm4 "name" "trm4"  --"bind (name) in (trm)"

print_theorems

thm trm4.recs

local_setup {* define_raw_fv "Terms.trm4" [

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

print_theorems

(* 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 ["trm4"] ["Terms.trm4"] *}

(* "repairing" of the permute function *)

lemma repaired:

  fixes ts::"trm4 list"

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

  apply(induct ts)

  apply(simp_all)

  done

thm permute_trm4_permute_trm4_list.simps

thm permute_trm4_permute_trm4_list.simps[simplified repaired]

inductive

    alpha4 :: "trm4 \<Rightarrow> trm4 \<Rightarrow> bool" ("_ \<approx>4 _" [100, 100] 100)

and alpha4list :: "trm4 list \<Rightarrow> trm4 list \<Rightarrow> bool" ("_ \<approx>4list _" [100, 100] 100) 

where

  a1: "a = b \<Longrightarrow> (Vr4 a) \<approx>4 (Vr4 b)"

| a2: "\<lbrakk>t1 \<approx>4 t2; s1 \<approx>4list s2\<rbrakk> \<Longrightarrow> Ap4 t1 s1 \<approx>4 Ap4 t2 s2"

| a3: "(\<exists>pi. (({atom a}, t) \<approx>gen alpha4 fv_rtrm4 pi ({atom b}, s))) \<Longrightarrow> Lm4 a t \<approx>4 Lm4 b s"

| a5: "[] \<approx>4list []"

| a6: "\<lbrakk>t \<approx>4 s; ts \<approx>4list ss\<rbrakk> \<Longrightarrow> (t#ts) \<approx>4list (s#ss)"

lemma alpha4_equivp: "equivp alpha4" sorry

lemma alpha4list_equivp: "equivp alpha4list" sorry

quotient_type 

  qtrm4 = trm4 / alpha4 and

  qtrm4list = "trm4 list" / alpha4list

  by (simp_all add: alpha4_equivp alpha4list_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)"

local_setup {* define_raw_fv "Terms.rtrm5" [

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

print_theorems

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

print_theorems

inductive

  alpha5 :: "rtrm5 \<Rightarrow> rtrm5 \<Rightarrow> bool" ("_ \<approx>5 _" [100, 100] 100)

and

  alphalts :: "rlts \<Rightarrow> rlts \<Rightarrow> bool" ("_ \<approx>l _" [100, 100] 100)

where

  a1: "a = b \<Longrightarrow> (rVr5 a) \<approx>5 (rVr5 b)"

| a2: "\<lbrakk>t1 \<approx>5 t2; s1 \<approx>5 s2\<rbrakk> \<Longrightarrow> rAp5 t1 s1 \<approx>5 rAp5 t2 s2"

| a3: "\<lbrakk>\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2)); 

        \<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))\<rbrakk>

        \<Longrightarrow> rLt5 l1 t1 \<approx>5 rLt5 l2 t2"

| a4: "rLnil \<approx>l rLnil"

| a5: "ls1 \<approx>l ls2 \<Longrightarrow> t1 \<approx>5 t2 \<Longrightarrow> n1 = n2 \<Longrightarrow> rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2"

print_theorems

lemma alpha5_inj:

  "((rVr5 a) \<approx>5 (rVr5 b)) = (a = b)"

  "(rAp5 t1 s1 \<approx>5 rAp5 t2 s2) = (t1 \<approx>5 t2 \<and> s1 \<approx>5 s2)"

  "(rLt5 l1 t1 \<approx>5 rLt5 l2 t2) = ((\<exists>pi. ((rbv5 l1, t1) \<approx>gen alpha5 fv_rtrm5 pi (rbv5 l2, t2))) \<and>

         (\<exists>pi. ((rbv5 l1, l1) \<approx>gen alphalts fv_rlts pi (rbv5 l2, l2))))"

  "rLnil \<approx>l rLnil"

  "(rLcons n1 t1 ls1 \<approx>l rLcons n2 t2 ls2) = (n1 = n2 \<and> ls1 \<approx>l ls2 \<and> t1 \<approx>5 t2)"

apply -

apply (simp_all add: alpha5_alphalts.intros)

apply rule

apply (erule alpha5.cases)

apply (simp_all add: alpha5_alphalts.intros)

apply rule

apply (erule alpha5.cases)

apply (simp_all add: alpha5_alphalts.intros)

apply rule

apply (erule alpha5.cases)

apply (simp_all add: alpha5_alphalts.intros)

apply rule

apply (erule alphalts.cases)

apply (simp_all add: alpha5_alphalts.intros)

done

lemma alpha5_equivps:

  shows "equivp alpha5"

  and   "equivp alphalts"

sorry

quotient_type

  trm5 = rtrm5 / alpha5

and

  lts = rlts / alphalts

  by (auto intro: alpha5_equivps)

quotient_definition

  "Vr5 :: name \<Rightarrow> trm5"

is

  "rVr5"

quotient_definition

  "Ap5 :: trm5 \<Rightarrow> trm5 \<Rightarrow> trm5"

is

  "rAp5"

quotient_definition

  "Lt5 :: lts \<Rightarrow> trm5 \<Rightarrow> trm5"

is

  "rLt5"

quotient_definition

  "Lnil :: lts"

is

  "rLnil"

quotient_definition

  "Lcons :: name \<Rightarrow> trm5 \<Rightarrow> lts \<Rightarrow> lts"

is

  "rLcons"

quotient_definition

   "fv_trm5 :: trm5 \<Rightarrow> atom set"

is

  "fv_rtrm5"

quotient_definition

   "fv_lts :: lts \<Rightarrow> atom set"

is

  "fv_rlts"

quotient_definition

   "bv5 :: lts \<Rightarrow> atom set"