equal
deleted
inserted
replaced
120 apply blast |
120 apply blast |
121 done |
121 done |
122 |
122 |
123 lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t" |
123 lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t" |
124 apply (erule evaln.induct) |
124 apply (erule evaln.induct) |
125 apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *}) |
125 apply (auto elim!: Suc_le_D_lemma) |
126 apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) |
|
127 done |
126 done |
128 |
127 |
129 lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'" |
128 lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'" |
130 apply (erule evaln_nonstrict) |
129 apply (erule evaln_nonstrict) |
131 apply auto |
130 apply auto |