src/HOL/IMPP/Natural.ML
changeset 17477 ceb42ea2f223
parent 13453 af96f2568406
     1.1 --- a/src/HOL/IMPP/Natural.ML	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/Natural.ML	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -4,21 +4,8 @@
     1.4      Copyright   1999 TUM
     1.5  *)
     1.6  
     1.7 -open Natural;
     1.8 -
     1.9 -AddIs evalc.intrs;
    1.10 -AddIs evaln.intrs;
    1.11 -
    1.12 -val evalc_elim_cases = map evalc.mk_cases
    1.13 -   ["<SKIP,s> -c-> t", "<X:==a,s> -c-> t", "<LOCAL Y:=a IN c,s> -c-> t", 
    1.14 -    "<c1;;c2,s> -c-> t","<IF b THEN c1 ELSE c2,s> -c-> t",
    1.15 -    "<BODY P,s> -c-> s1", "<X:=CALL P(a),s> -c-> s1"];
    1.16 -val evaln_elim_cases = map evaln.mk_cases
    1.17 -   ["<SKIP,s> -n-> t", "<X:==a,s> -n-> t", "<LOCAL Y:=a IN c,s> -n-> t",
    1.18 -    "<c1;;c2,s> -n-> t","<IF b THEN c1 ELSE c2,s> -n-> t",
    1.19 -    "<BODY P,s> -n-> s1", "<X:=CALL P(a),s> -n-> s1"];
    1.20 -val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
    1.21 -val evaln_WHILE_case = evaln.mk_cases "<WHILE b DO c,s> -n-> t";
    1.22 +AddIs evalc.intros;
    1.23 +AddIs evaln.intros;
    1.24  
    1.25  AddSEs evalc_elim_cases;
    1.26  AddSEs evaln_elim_cases;
    1.27 @@ -33,7 +20,7 @@
    1.28  
    1.29  Goal "<c,s> -n-> t ==> <c,s> -c-> t";
    1.30  by (etac evaln.induct 1);
    1.31 -by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac));
    1.32 +by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac));
    1.33  qed "evaln_evalc";
    1.34  
    1.35  Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
    1.36 @@ -46,7 +33,7 @@
    1.37  Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
    1.38  by (etac evaln.induct 1);
    1.39  by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
    1.40 -by (ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW atac));
    1.41 +by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac));
    1.42  qed_spec_mp "evaln_nonstrict";
    1.43  
    1.44  Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
    1.45 @@ -64,7 +51,7 @@
    1.46  by (etac evalc.induct 1);
    1.47  by (ALLGOALS (REPEAT o etac exE));
    1.48  by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
    1.49 -by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intrs THEN_ALL_NEW atac));
    1.50 +by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac));
    1.51  qed "evalc_evaln";
    1.52  
    1.53  Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";