equal
deleted
inserted
replaced
356 shows "pders s r \<subseteq> subs r" |
356 shows "pders s r \<subseteq> subs r" |
357 apply(induct r arbitrary: s) |
357 apply(induct r arbitrary: s) |
358 apply(simp) |
358 apply(simp) |
359 apply(simp) |
359 apply(simp) |
360 apply(simp add: pders_CHAR) |
360 apply(simp add: pders_CHAR) |
|
361 (* SEQ case *) |
361 apply(simp) |
362 apply(simp) |
362 apply(rule subset_trans) |
363 apply(rule subset_trans) |
363 apply(rule pders_SEQ) |
364 apply(rule pders_SEQ) |
364 defer |
365 defer |
|
366 (* ALT case *) |
365 apply(simp) |
367 apply(simp) |
366 apply(rule impI) |
368 apply(rule impI) |
367 apply(rule conjI) |
369 apply(rule conjI) |
368 apply blast |
370 apply blast |
369 apply blast |
371 apply blast |
|
372 (* STAR case *) |
370 apply(case_tac s) |
373 apply(case_tac s) |
371 apply(simp) |
374 apply(simp) |
372 apply(rule subset_trans) |
375 apply(rule subset_trans) |
373 thm pders_STAR |
376 thm pders_STAR |
374 apply(rule pders_STAR) |
377 apply(rule pders_STAR) |
375 apply(simp) |
378 apply(simp) |
376 apply(simp) |
379 apply(auto simp add: pders_Set_def)[1] |
377 apply (smt UN_I UN_least Un_iff insertCI pders_Set_def subsetCE subsetI) |
|
378 apply(simp) |
380 apply(simp) |
379 apply(rule conjI) |
381 apply(rule conjI) |
380 apply blast |
382 apply blast |
381 by (metis Un_insert_right le_supI1 pders_Set_subsetI subset_trans sup_ge2) |
383 apply(auto simp add: pders_Set_def)[1] |
|
384 done |
382 |
385 |
383 fun size2 :: "rexp \<Rightarrow> nat" where |
386 fun size2 :: "rexp \<Rightarrow> nat" where |
384 "size2 ZERO = 1" | |
387 "size2 ZERO = 1" | |
385 "size2 ONE = 1" | |
388 "size2 ONE = 1" | |
386 "size2 (CHAR c) = 1" | |
389 "size2 (CHAR c) = 1" | |
401 shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
404 shows "\<forall>r1 \<in> subs r. size2 r1 \<le> Suc (size2 r * size2 r)" |
402 apply(induct r) |
405 apply(induct r) |
403 apply(simp) |
406 apply(simp) |
404 apply(simp) |
407 apply(simp) |
405 apply(simp) |
408 apply(simp) |
|
409 (* SEQ case *) |
406 apply(simp) |
410 apply(simp) |
407 apply(auto)[1] |
411 apply(auto)[1] |
408 apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
412 apply (smt Suc_n_not_le_n add.commute distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
409 apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2) |
413 apply (smt Suc_le_mono Suc_n_not_le_n le_trans nat_le_linear power2_eq_square power2_sum semiring_normalization_rules(23) trans_le_add2) |
410 apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
414 apply (smt Groups.add_ac(3) Suc_n_not_le_n distrib_left le_Suc_eq left_add_mult_distrib nat_le_linear trans_le_add1) |
|
415 (* ALT case *) |
411 apply(simp) |
416 apply(simp) |
412 apply(auto)[1] |
417 apply(auto)[1] |
413 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum) |
418 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n le_add2 linear order_trans power2_eq_square power2_sum) |
414 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1) |
419 apply (smt Groups.add_ac(2) Suc_le_mono Suc_n_not_le_n left_add_mult_distrib linear mult.commute order.trans trans_le_add1) |
|
420 (* STAR case *) |
415 apply(auto)[1] |
421 apply(auto)[1] |
416 apply(drule_tac x="r'" in bspec) |
422 apply(drule_tac x="r'" in bspec) |
417 apply(simp) |
423 apply(simp) |
418 apply(rule le_trans) |
424 apply(rule le_trans) |
419 apply(assumption) |
425 apply(assumption) |