17 |
17 |
18 consts |
18 consts |
19 Ssub :: "i" |
19 Ssub :: "i" |
20 Scomp :: "i" |
20 Scomp :: "i" |
21 Sreg :: "i" |
21 Sreg :: "i" |
22 union_aux :: "i=>i" |
|
23 regular :: "i=>o" |
|
24 |
|
25 (*syntax??*) |
|
26 un :: "[i,i]=>i" (infixl 70) |
|
27 "<==" :: "[i,i]=>o" (infixl 70) |
|
28 "~" :: "[i,i]=>o" (infixl 70) |
|
29 |
22 |
|
23 abbreviation |
|
24 Ssub_rel (infixl "<==" 70) where |
|
25 "a<==b == <a,b> \<in> Ssub" |
30 |
26 |
31 translations |
27 abbreviation |
32 "a<==b" == "<a,b> \<in> Ssub" |
28 Scomp_rel (infixl "~" 70) where |
33 "a ~ b" == "<a,b> \<in> Scomp" |
29 "a ~ b == <a,b> \<in> Scomp" |
34 "regular(a)" == "a \<in> Sreg" |
|
35 |
30 |
|
31 abbreviation |
|
32 "regular(a) == a \<in> Sreg" |
36 |
33 |
|
34 consts union_aux :: "i=>i" |
37 primrec (*explicit lambda is required because both arguments of "un" vary*) |
35 primrec (*explicit lambda is required because both arguments of "un" vary*) |
38 "union_aux(Var(n)) = |
36 "union_aux(Var(n)) = |
39 (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))" |
37 (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))" |
40 |
38 |
41 "union_aux(Fun(u)) = |
39 "union_aux(Fun(u)) = |
45 "union_aux(App(b,f,a)) = |
43 "union_aux(App(b,f,a)) = |
46 (\<lambda>t \<in> redexes. |
44 (\<lambda>t \<in> redexes. |
47 redexes_case(%j. 0, %y. 0, |
45 redexes_case(%j. 0, %y. 0, |
48 %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))" |
46 %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))" |
49 |
47 |
50 defs |
48 definition |
51 union_def: "u un v == union_aux(u)`v" |
49 union (infixl "un" 70) where |
|
50 "u un v == union_aux(u)`v" |
52 |
51 |
53 syntax (xsymbols) |
52 notation (xsymbols) |
54 "op un" :: "[i,i]=>i" (infixl "\<squnion>" 70) |
53 union (infixl "\<squnion>" 70) and |
55 "op <==" :: "[i,i]=>o" (infixl "\<Longleftarrow>" 70) |
54 Ssub_rel (infixl "\<Longleftarrow>" 70) and |
56 "op ~" :: "[i,i]=>o" (infixl "\<sim>" 70) |
55 Scomp_rel (infixl "\<sim>" 70) |
|
56 |
57 |
57 |
58 inductive |
58 inductive |
59 domains "Ssub" <= "redexes*redexes" |
59 domains "Ssub" <= "redexes*redexes" |
60 intros |
60 intros |
61 Sub_Var: "n \<in> nat ==> Var(n)<== Var(n)" |
61 Sub_Var: "n \<in> nat ==> Var(n)<== Var(n)" |