equal
deleted
inserted
replaced
1 |
1 |
2 theory Sulzmann |
2 theory Sulzmann |
3 imports "Lexer" |
3 imports "Lexer" "~~/src/HOL/Library/Multiset" |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sulzmann's "Ordering" of Values *} |
7 section {* Sulzmann's "Ordering" of Values *} |
8 |
8 |
80 | "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in |
80 | "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in |
81 let (vs, ds'') = decode' ds' (STAR r) |
81 let (vs, ds'') = decode' ds' (STAR r) |
82 in (Stars_add v vs, ds''))" |
82 in (Stars_add v vs, ds''))" |
83 by pat_completeness auto |
83 by pat_completeness auto |
84 |
84 |
|
85 termination |
|
86 apply(size_change) |
|
87 oops |
|
88 |
85 term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))" |
89 term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))" |
86 |
90 |
87 lemma decode'_smaller: |
91 lemma decode'_smaller: |
88 assumes "decode'_dom (ds, r)" |
92 assumes "decode'_dom (ds, r)" |
89 shows "length (snd (decode' ds r)) \<le> length ds" |
93 shows "length (snd (decode' ds r)) \<le> length ds" |