equal
deleted
inserted
replaced
1578 theorem blexersimp_correctness: |
1578 theorem blexersimp_correctness: |
1579 shows "lexer r s = blexer_simp r s" |
1579 shows "lexer r s = blexer_simp r s" |
1580 using blexer_correctness main_main by auto |
1580 using blexer_correctness main_main by auto |
1581 |
1581 |
1582 |
1582 |
|
1583 |
|
1584 export_code blexer_simp blexer lexer bders bders_simp in Scala module_name VerifiedLexers |
|
1585 |
|
1586 |
1583 unused_thms |
1587 unused_thms |
1584 |
1588 |
1585 |
1589 |
|
1590 inductive aggressive:: "arexp \<Rightarrow> arexp \<Rightarrow> bool" ("_ \<leadsto>? _" [99, 99] 99) |
|
1591 where |
|
1592 "ASEQ bs (AALTs bs1 rs) r \<leadsto>? AALTs (bs@bs1) (map (\<lambda>r'. ASEQ [] r' r) rs) " |
|
1593 |
|
1594 |
|
1595 |
1586 end |
1596 end |