446 prefer 2 apply assumption |
446 prefer 2 apply assumption |
447 back back back back |
447 back back back back |
448 apply (rule_tac x = "schA" in spec) |
448 apply (rule_tac x = "schA" in spec) |
449 apply (rule_tac x = "schB" in spec) |
449 apply (rule_tac x = "schB" in spec) |
450 apply (rule_tac x = "tr" in spec) |
450 apply (rule_tac x = "tr" in spec) |
451 apply (tactic "thin_tac' @{context} 5 1") |
451 apply (tactic "thin_tac' \<^context> 5 1") |
452 apply (rule nat_less_induct) |
452 apply (rule nat_less_induct) |
453 apply (rule allI)+ |
453 apply (rule allI)+ |
454 apply (rename_tac tr schB schA) |
454 apply (rename_tac tr schB schA) |
455 apply (intro strip) |
455 apply (intro strip) |
456 apply (erule conjE)+ |
456 apply (erule conjE)+ |
457 |
457 |
458 apply (case_tac "Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr") |
458 apply (case_tac "Forall (\<lambda>x. x \<in> act B \<and> x \<notin> act A) tr") |
459 |
459 |
460 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
460 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
461 apply (tactic "thin_tac' @{context} 5 1") |
461 apply (tactic "thin_tac' \<^context> 5 1") |
462 |
462 |
463 |
463 |
464 apply (case_tac "Finite tr") |
464 apply (case_tac "Finite tr") |
465 |
465 |
466 text \<open>both sides of this equation are \<open>nil\<close>\<close> |
466 text \<open>both sides of this equation are \<open>nil\<close>\<close> |
664 prefer 2 apply assumption |
664 prefer 2 apply assumption |
665 back back back back |
665 back back back back |
666 apply (rule_tac x = "schA" in spec) |
666 apply (rule_tac x = "schA" in spec) |
667 apply (rule_tac x = "schB" in spec) |
667 apply (rule_tac x = "schB" in spec) |
668 apply (rule_tac x = "tr" in spec) |
668 apply (rule_tac x = "tr" in spec) |
669 apply (tactic "thin_tac' @{context} 5 1") |
669 apply (tactic "thin_tac' \<^context> 5 1") |
670 apply (rule nat_less_induct) |
670 apply (rule nat_less_induct) |
671 apply (rule allI)+ |
671 apply (rule allI)+ |
672 apply (rename_tac tr schB schA) |
672 apply (rename_tac tr schB schA) |
673 apply (intro strip) |
673 apply (intro strip) |
674 apply (erule conjE)+ |
674 apply (erule conjE)+ |
675 |
675 |
676 apply (case_tac "Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr") |
676 apply (case_tac "Forall (\<lambda>x. x \<in> act A \<and> x \<notin> act B) tr") |
677 |
677 |
678 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
678 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
679 apply (tactic "thin_tac' @{context} 5 1") |
679 apply (tactic "thin_tac' \<^context> 5 1") |
680 |
680 |
681 apply (case_tac "Finite tr") |
681 apply (case_tac "Finite tr") |
682 |
682 |
683 text \<open>both sides of this equation are \<open>nil\<close>\<close> |
683 text \<open>both sides of this equation are \<open>nil\<close>\<close> |
684 apply (subgoal_tac "schB = nil") |
684 apply (subgoal_tac "schB = nil") |