equal
deleted
inserted
replaced
1 theory LamEx |
1 theory LamEx |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" |
2 imports "../Nominal2_Atoms" "../Nominal2_Eqvt" "../Nominal2_Supp" "../Abs" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 datatype rlam = |
7 datatype rlam = |
85 apply(simp add: Diff_eqvt) |
85 apply(simp add: Diff_eqvt) |
86 apply(simp add: permute_set_eq atom_eqvt) |
86 apply(simp add: permute_set_eq atom_eqvt) |
87 done |
87 done |
88 |
88 |
89 inductive |
89 inductive |
90 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100) |
90 alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx>a _" [100, 100] 100) |
91 where |
91 where |
92 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
92 a1: "a = b \<Longrightarrow> (rVar a) \<approx>a (rVar b)" |
93 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
93 | a2: "\<lbrakk>t1 \<approx>a t2; s1 \<approx>a s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx>a rApp t2 s2" |
94 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s) |
94 | a3: "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>a s) |
95 \<Longrightarrow> rLam a t \<approx> rLam b s" |
95 \<Longrightarrow> rLam a t \<approx>a rLam b s" |
96 |
96 |
97 lemma a3_inverse: |
97 lemma a3_inverse: |
98 assumes "rLam a t \<approx> rLam b s" |
98 assumes "rLam a t \<approx> rLam b s" |
99 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)" |
99 shows "\<exists>pi. (rfv t - {atom a} = rfv s - {atom b} \<and> (rfv t - {atom a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s)" |
100 using assms |
100 using assms |