# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264263918 -3600
# Node ID 2cb5745f403eb35b0953c76f2962a8c56876bb5e
# Parent  a7bf638e9af329b06be9d27c70a0642d622385c0
The alpha equivalence relations for structures in 'Terms'

diff -r a7bf638e9af3 -r 2cb5745f403e Quot/Examples/Terms.thy
--- a/Quot/Examples/Terms.thy	Sat Jan 23 15:41:54 2010 +0100
+++ b/Quot/Examples/Terms.thy	Sat Jan 23 17:25:18 2010 +0100
@@ -57,6 +57,25 @@
 
 end
 
+inductive
+  alpha1 :: "trm1 \<Rightarrow> trm1 \<Rightarrow> bool" ("_ \<approx>1 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Vr1 a) \<approx>1 (Vr1 b)"
+| a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> Ap1 t1 s1 \<approx>1 Ap1 t2 s2"
+| a3: "\<exists>pi::name prm. (fv_trm1 t - {a} = fv_trm1 s - {b} \<and> (fv_trm1 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>1 s \<and> (pi \<bullet> a) = b)
+       \<Longrightarrow> Lm1 a t \<approx>1 Lm1 b s"
+| a4: "\<exists>pi::name prm.(
+         t1 \<approx>1 t2 \<and>
+         (fv_trm1 s1 - fv_bp b1 = fv_trm1 s2 - fv_bp b2) \<and>
+         (fv_trm1 s1 - fv_bp b1) \<sharp>* pi \<and>
+         (pi \<bullet> s1 = s2)                    (* Optional: \<and> (pi \<bullet> b1 = b2) *)
+       ) \<Longrightarrow> Lt1 b1 t1 s1 \<approx>1 Lt1 b2 t2 s2"
+
+lemma alpha1_equivp: "equivp alpha1" sorry
+
+quotient_type qtrm1 = trm1 / alpha1
+  by (rule alpha1_equivp)
+
 
 section {*** lets with single assignments ***}
 
@@ -101,6 +120,23 @@
 
 end
 
+inductive
+  alpha2 :: "trm2 \<Rightarrow> trm2 \<Rightarrow> bool" ("_ \<approx>2 _" [100, 100] 100)
+where
+  a1: "a = b \<Longrightarrow> (Vr2 a) \<approx>2 (Vr2 b)"
+| a2: "\<lbrakk>t1 \<approx>2 t2; s1 \<approx>2 s2\<rbrakk> \<Longrightarrow> Ap2 t1 s1 \<approx>2 Ap2 t2 s2"
+| a3: "\<exists>pi::name prm. (fv_trm2 t - {a} = fv_trm2 s - {b} \<and> (fv_trm2 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>2 s \<and> (pi \<bullet> a) = b)
+       \<Longrightarrow> Lm2 a t \<approx>2 Lm2 b s"
+| a4: "\<exists>pi::name prm. (
+         fv_trm2 t1 - fv_assign b1 = fv_trm2 t2 - fv_assign b2 \<and>
+         (fv_trm2 t1 - fv_assign b1) \<sharp>* pi \<and>
+         pi \<bullet> t1 = t2       (* \<and> (pi \<bullet> b1 = b2) *)
+       ) \<Longrightarrow> Lt2 b1 t1 \<approx>2 Lt2 b2 t2"
+
+lemma alpha2_equivp: "equivp alpha2" sorry
+
+quotient_type qtrm2 = trm2 / alpha2
+  by (rule alpha2_equivp)
 
 section {*** lets with many assignments ***}
 
@@ -148,5 +184,22 @@
 
 end
 
+inductive
+  alpha3 :: "trm3 \<Rightarrow> trm3 \<Rightarrow> bool" ("_ \<approx>3 _" [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::name prm. (fv_trm3 t - {a} = fv_trm3 s - {b} \<and> (fv_trm3 t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>3 s \<and> (pi \<bullet> a) = b)
+       \<Longrightarrow> Lm3 a t \<approx>3 Lm3 b s"
+| a4: "\<exists>pi::name prm. (
+         fv_trm3 t1 - fv_assigns b1 = fv_trm3 t2 - fv_assigns b2 \<and>
+         (fv_trm3 t1 - fv_assigns b1) \<sharp>* pi \<and>
+         pi \<bullet> t1 = t2      (* \<and> (pi \<bullet> b1 = b2)  *)
+       ) \<Longrightarrow> Lt3 b1 t1 \<approx>3 Lt3 b2 t2"
 
-end
\ No newline at end of file
+lemma alpha3_equivp: "equivp alpha3" sorry
+
+quotient_type qtrm3 = trm3 / alpha3
+  by (rule alpha3_equivp)
+
+end