equal
deleted
inserted
replaced
331 also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pders_set_UNIV1_le_awidth) |
331 also have "\<dots> \<le> Suc (awidth r)" by(simp add: card_pders_set_UNIV1_le_awidth) |
332 finally show ?thesis by(simp add: pders_Set_UNIV) |
332 finally show ?thesis by(simp add: pders_Set_UNIV) |
333 qed |
333 qed |
334 |
334 |
335 text\<open>Antimirov's Corollary 3.5:\<close> |
335 text\<open>Antimirov's Corollary 3.5:\<close> |
336 |
336 (*W stands for word set*) |
337 corollary card_pders_set_le_awidth: |
337 corollary card_pders_set_le_awidth: |
338 shows "card (pders_Set A r) \<le> awidth r + 1" |
338 shows "card (pders_Set W r) \<le> awidth r + 1" |
339 proof - |
339 proof - |
340 have "card (pders_Set A r) \<le> card (pders_Set UNIV r)" |
340 have "card (pders_Set W r) \<le> card (pders_Set UNIV r)" |
341 by (simp add: card_mono finite_pders_set pders_Set_subset) |
341 by (simp add: card_mono finite_pders_set pders_Set_subset) |
342 also have "... \<le> awidth r + 1" |
342 also have "... \<le> awidth r + 1" |
343 by (rule card_pders_set_UNIV_le_awidth) |
343 by (rule card_pders_set_UNIV_le_awidth) |
344 finally show "card (pders_Set A r) \<le> awidth r + 1" by simp |
344 finally show "card (pders_Set W r) \<le> awidth r + 1" by simp |
345 qed |
345 qed |
346 |
346 |
347 (* other result by antimirov *) |
347 (* other result by antimirov *) |
348 |
348 |
349 lemma card_pders_awidth: |
349 lemma card_pders_awidth: |
600 lemma alternative_pder: |
600 lemma alternative_pder: |
601 shows "pderso s r = pders s r" |
601 shows "pderso s r = pders s r" |
602 sledgehammer |
602 sledgehammer |
603 oops |
603 oops |
604 |
604 |
|
605 lemma pdero_result: |
|
606 shows "pdero c (STAR (ALT (CH c) (SEQ (CH c) (CH c)))) = {SEQ (CH c)(STAR (ALT (CH c) (SEQ (CH c) (CH c)))),(STAR (ALT (CH c) (SEQ (CH c) (CH c))))}" |
|
607 apply(simp) |
|
608 by auto |
|
609 |
|
610 fun concatLen :: "rexp \<Rightarrow> nat" where |
|
611 "concatLen ZERO = 0" | |
|
612 "concatLen ONE = 0" | |
|
613 "concatLen (CH c) = 0" | |
|
614 "concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" | |
|
615 " concatLen (ALT v1 v2) = max (concatLen v1) (concatLen v2)" | |
|
616 " concatLen (STAR v) = Suc (concatLen v)" |
|
617 |
|
618 |
605 |
619 |
606 export_code height pders subs pderso in Scala module_name Pders |
620 export_code height pders subs pderso in Scala module_name Pders |
607 export_code pdero pderso in Scala module_name Pderso |
621 export_code pdero pderso in Scala module_name Pderso |
608 export_code pdero pderso in Scala module_name Pderso |
622 export_code pdero pderso in Scala module_name Pderso |
609 |
623 |