33 and method = rmethod / alpha_method |
33 and method = rmethod / alpha_method |
34 by (auto intro: alpha_equivps) |
34 by (auto intro: alpha_equivps) |
35 |
35 |
36 quotient_definition |
36 quotient_definition |
37 "Var :: name \<Rightarrow> obj" |
37 "Var :: name \<Rightarrow> obj" |
38 as |
38 is |
39 "rVar" |
39 "rVar" |
40 |
40 |
41 quotient_definition |
41 quotient_definition |
42 "Obj :: (string \<times> method) list \<Rightarrow> obj" |
42 "Obj :: (string \<times> method) list \<Rightarrow> obj" |
43 as |
43 is |
44 "rObj" |
44 "rObj" |
45 |
45 |
46 quotient_definition |
46 quotient_definition |
47 "Inv :: obj \<Rightarrow> string \<Rightarrow> obj" |
47 "Inv :: obj \<Rightarrow> string \<Rightarrow> obj" |
48 as |
48 is |
49 "rInv" |
49 "rInv" |
50 |
50 |
51 quotient_definition |
51 quotient_definition |
52 "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj" |
52 "Upd :: obj \<Rightarrow> string \<Rightarrow> method \<Rightarrow> obj" |
53 as |
53 is |
54 "rUpd" |
54 "rUpd" |
55 |
55 |
56 quotient_definition |
56 quotient_definition |
57 "Sig :: name \<Rightarrow> obj \<Rightarrow> method" |
57 "Sig :: name \<Rightarrow> obj \<Rightarrow> method" |
58 as |
58 is |
59 "rSig" |
59 "rSig" |
60 |
60 |
61 overloading |
61 overloading |
62 perm_obj \<equiv> "perm :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" (unchecked) |
62 perm_obj \<equiv> "perm :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" (unchecked) |
63 perm_method \<equiv> "perm :: 'x prm \<Rightarrow> method \<Rightarrow> method" (unchecked) |
63 perm_method \<equiv> "perm :: 'x prm \<Rightarrow> method \<Rightarrow> method" (unchecked) |
64 begin |
64 begin |
65 |
65 |
66 quotient_definition |
66 quotient_definition |
67 "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" |
67 "perm_obj :: 'x prm \<Rightarrow> obj \<Rightarrow> obj" |
68 as |
68 is |
69 "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)" |
69 "(perm::'x prm \<Rightarrow> robj \<Rightarrow> robj)" |
70 |
70 |
71 quotient_definition |
71 quotient_definition |
72 "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method" |
72 "perm_method :: 'x prm \<Rightarrow> method \<Rightarrow> method" |
73 as |
73 is |
74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
74 "(perm::'x prm \<Rightarrow> rmethod \<Rightarrow> rmethod)" |
75 |
75 |
76 end |
76 end |
77 |
77 |
78 |
78 |