equal
deleted
inserted
replaced
16 | "rerase (AONE _) = RONE" |
16 | "rerase (AONE _) = RONE" |
17 | "rerase (ACHAR _ c) = RCHAR c" |
17 | "rerase (ACHAR _ c) = RCHAR c" |
18 | "rerase (AALTs bs rs) = RALTS (map rerase rs)" |
18 | "rerase (AALTs bs rs) = RALTS (map rerase rs)" |
19 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" |
19 | "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)" |
20 | "rerase (ASTAR _ r) = RSTAR (rerase r)" |
20 | "rerase (ASTAR _ r) = RSTAR (rerase r)" |
|
21 | "rerase (ANTIMES _ r n) = RNTIMES (rerase r) n" |
21 |
22 |
22 lemma eq1_rerase: |
23 lemma eq1_rerase: |
23 shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)" |
24 shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)" |
24 apply(induct x y rule: eq1.induct) |
25 apply(induct x y rule: eq1.induct) |
25 apply(auto) |
26 apply(auto) |