# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264178686 -3600
# Node ID b8e43414c5aad5bc6d4f675c4c7611ce3c8aad37
# Parent  b1f55dd64481b212440a66ff829b1f556c9540ae
Proper alpha equivalence for Sigma calculus.

diff -r b1f55dd64481 -r b8e43414c5aa Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Thu Jan 21 19:52:46 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Fri Jan 22 17:44:46 2010 +0100
@@ -12,13 +12,16 @@
 and rmethod =
   rSig "name" "robj"
 
-(* Need to fix it, just 2 random rules *)
 inductive
     alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100)
 and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100)
 where
   a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)"
-| a2: "a = b \<and> c = d \<Longrightarrow> rSig a c \<approx>m rSig b d"
+| a2: "rObj [] \<approx>o rObj []"
+| a3: "rObj t1 \<approx>o rObj t2 \<Longrightarrow> m1 \<approx>m r2 \<Longrightarrow> rObj ((l1, m1) # t1) \<approx>o rObj ((l2, m2) # t2)"
+| a4: "x \<approx>o y \<Longrightarrow> rInv x l1 \<approx>o rInv y l2"
+| a5: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx>o s \<and> (pi \<bullet> a) = b)
+       \<Longrightarrow> rSig a t \<approx>m rSig b s"
 
 lemma alpha_equivps:
   shows "equivp alpha_obj"