equal
deleted
inserted
replaced
138 done |
138 done |
139 |
139 |
140 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t" |
140 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t" |
141 apply (erule evalc.induct) |
141 apply (erule evalc.induct) |
142 apply (tactic {* ALLGOALS (REPEAT o etac exE) *}) |
142 apply (tactic {* ALLGOALS (REPEAT o etac exE) *}) |
143 apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *}) |
143 apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac, REPEAT o eresolve_tac [exE, conjE]]) *}) |
144 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) |
144 apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) |
145 done |
145 done |
146 |
146 |
147 lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)" |
147 lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)" |
148 apply (fast elim: evalc_evaln evaln_evalc) |
148 apply (fast elim: evalc_evaln evaln_evalc) |