equal
deleted
inserted
replaced
475 prefer 2 apply assumption |
475 prefer 2 apply assumption |
476 back back back back |
476 back back back back |
477 apply (rule_tac x = "schA" in spec) |
477 apply (rule_tac x = "schA" in spec) |
478 apply (rule_tac x = "schB" in spec) |
478 apply (rule_tac x = "schB" in spec) |
479 apply (rule_tac x = "tr" in spec) |
479 apply (rule_tac x = "tr" in spec) |
480 apply (tactic "thin_tac' 5 1") |
480 apply (tactic "thin_tac' @{context} 5 1") |
481 apply (rule nat_less_induct) |
481 apply (rule nat_less_induct) |
482 apply (rule allI)+ |
482 apply (rule allI)+ |
483 apply (rename_tac tr schB schA) |
483 apply (rename_tac tr schB schA) |
484 apply (intro strip) |
484 apply (intro strip) |
485 apply (erule conjE)+ |
485 apply (erule conjE)+ |
486 |
486 |
487 apply (case_tac "Forall (%x. x:act B & x~:act A) tr") |
487 apply (case_tac "Forall (%x. x:act B & x~:act A) tr") |
488 |
488 |
489 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
489 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
490 apply (tactic "thin_tac' 5 1") |
490 apply (tactic "thin_tac' @{context} 5 1") |
491 |
491 |
492 |
492 |
493 apply (case_tac "Finite tr") |
493 apply (case_tac "Finite tr") |
494 |
494 |
495 (* both sides of this equation are nil *) |
495 (* both sides of this equation are nil *) |
695 prefer 2 apply assumption |
695 prefer 2 apply assumption |
696 back back back back |
696 back back back back |
697 apply (rule_tac x = "schA" in spec) |
697 apply (rule_tac x = "schA" in spec) |
698 apply (rule_tac x = "schB" in spec) |
698 apply (rule_tac x = "schB" in spec) |
699 apply (rule_tac x = "tr" in spec) |
699 apply (rule_tac x = "tr" in spec) |
700 apply (tactic "thin_tac' 5 1") |
700 apply (tactic "thin_tac' @{context} 5 1") |
701 apply (rule nat_less_induct) |
701 apply (rule nat_less_induct) |
702 apply (rule allI)+ |
702 apply (rule allI)+ |
703 apply (rename_tac tr schB schA) |
703 apply (rename_tac tr schB schA) |
704 apply (intro strip) |
704 apply (intro strip) |
705 apply (erule conjE)+ |
705 apply (erule conjE)+ |
706 |
706 |
707 apply (case_tac "Forall (%x. x:act A & x~:act B) tr") |
707 apply (case_tac "Forall (%x. x:act A & x~:act B) tr") |
708 |
708 |
709 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
709 apply (rule seq_take_lemma [THEN iffD2, THEN spec]) |
710 apply (tactic "thin_tac' 5 1") |
710 apply (tactic "thin_tac' @{context} 5 1") |
711 |
711 |
712 apply (case_tac "Finite tr") |
712 apply (case_tac "Finite tr") |
713 |
713 |
714 (* both sides of this equation are nil *) |
714 (* both sides of this equation are nil *) |
715 apply (subgoal_tac "schB=nil") |
715 apply (subgoal_tac "schB=nil") |