equal
deleted
inserted
replaced
10 | rInv "robj" "string" |
10 | rInv "robj" "string" |
11 | rUpd "robj" "string" "rmethod" |
11 | rUpd "robj" "string" "rmethod" |
12 and rmethod = |
12 and rmethod = |
13 rSig "name" "robj" |
13 rSig "name" "robj" |
14 |
14 |
15 (* Need to fix it, just 2 random rules *) |
|
16 inductive |
15 inductive |
17 alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100) |
16 alpha_obj :: "robj \<Rightarrow> robj \<Rightarrow> bool" ("_ \<approx>o _" [100, 100] 100) |
18 and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100) |
17 and alpha_method :: "rmethod \<Rightarrow> rmethod \<Rightarrow> bool" ("_ \<approx>m _" [100, 100] 100) |
19 where |
18 where |
20 a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)" |
19 a1: "a = b \<Longrightarrow> (rVar a) \<approx>o (rVar b)" |
21 | a2: "a = b \<and> c = d \<Longrightarrow> rSig a c \<approx>m rSig b d" |
20 | a2: "rObj [] \<approx>o rObj []" |
|
21 | a3: "rObj t1 \<approx>o rObj t2 \<Longrightarrow> m1 \<approx>m r2 \<Longrightarrow> rObj ((l1, m1) # t1) \<approx>o rObj ((l2, m2) # t2)" |
|
22 | a4: "x \<approx>o y \<Longrightarrow> rInv x l1 \<approx>o rInv y l2" |
|
23 | 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) |
|
24 \<Longrightarrow> rSig a t \<approx>m rSig b s" |
22 |
25 |
23 lemma alpha_equivps: |
26 lemma alpha_equivps: |
24 shows "equivp alpha_obj" |
27 shows "equivp alpha_obj" |
25 and "equivp alpha_method" |
28 and "equivp alpha_method" |
26 sorry |
29 sorry |