(* Title: HOL/IMPP/Natural.ML ID: $Id: Natural.ML,v 1.5 2005/09/17 18:14:31 wenzelm Exp $ Author: David von Oheimb, TUM Copyright 1999 TUM *) AddIs evalc.intros; AddIs evaln.intros; AddSEs evalc_elim_cases; AddSEs evaln_elim_cases; (* evaluation of com is deterministic *) Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; by (etac evalc.induct 1); by (thin_tac "<?c,s1> -c-> s2" 8); (*blast_tac needs Unify.search_bound := 40*) by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); qed_spec_mp "com_det"; Goal "<c,s> -n-> t ==> <c,s> -c-> t"; by (etac evaln.induct 1); by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac)); qed "evaln_evalc"; Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; by (cut_facts_tac (premises()) 1); by (ftac Suc_le_D 1); by (Clarify_tac 1); by (eresolve_tac (premises()) 1); qed "Suc_le_D_lemma"; Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"; by (etac evaln.induct 1); by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1])); by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac)); qed_spec_mp "evaln_nonstrict"; Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"; by (etac evaln_nonstrict 1); by Auto_tac; qed "evaln_Suc"; Goal "[| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |] ==> \ \ ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2"; by (cut_facts_tac [read_instantiate [("m","n1"),("n","n2")] nat_le_linear] 1); by (blast_tac (claset() addDs [evaln_nonstrict]) 1); qed "evaln_max2"; Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t"; by (etac evalc.induct 1); by (ALLGOALS (REPEAT o etac exE)); by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]])); by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac)); qed "evalc_evaln"; Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)"; by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1); qed "eval_eq";