src/HOL/IMPP/Natural.ML
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 13453 af96f2568406
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/Natural.ML
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb, TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13453
diff changeset
     7
AddIs evalc.intros;
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13453
diff changeset
     8
AddIs evaln.intros;
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     9
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    10
AddSEs evalc_elim_cases;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
AddSEs evaln_elim_cases;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
(* evaluation of com is deterministic *)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    14
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 9442
diff changeset
    15
by (etac evalc.induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
by (thin_tac "<?c,s1> -c-> s2" 8);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
(*blast_tac needs Unify.search_bound := 40*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    18
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    19
qed_spec_mp "com_det";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    20
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    21
Goal "<c,s> -n-> t ==> <c,s> -c-> t";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 9442
diff changeset
    22
by (etac evaln.induct 1);
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13453
diff changeset
    23
by (ALLGOALS (resolve_tac evalc.intros THEN_ALL_NEW atac));
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    24
qed "evaln_evalc";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
by (cut_facts_tac (premises()) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    28
by (ftac Suc_le_D 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    29
by (Clarify_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    30
by (eresolve_tac (premises()) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
qed "Suc_le_D_lemma";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    32
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
Goal "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 9442
diff changeset
    34
by (etac evaln.induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
by (ALLGOALS (EVERY'[strip_tac,TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]));
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13453
diff changeset
    36
by (ALLGOALS (resolve_tac evaln.intros THEN_ALL_NEW atac));
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    37
qed_spec_mp "evaln_nonstrict";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    38
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
Goal "<c,s> -n-> s' ==> <c,s> -Suc n-> s'";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 9442
diff changeset
    40
by (etac evaln_nonstrict 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
by Auto_tac;
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    42
qed "evaln_Suc";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    43
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
Goal "[| <c1,s1> -n1-> t1;  <c2,s2> -n2-> t2 |] ==> \
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    45
\   ? n. <c1,s1> -n -> t1 & <c2,s2> -n -> t2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    46
by (cut_facts_tac [read_instantiate [("m","n1"),("n","n2")] nat_le_linear] 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
by (blast_tac (claset() addDs [evaln_nonstrict]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    48
qed "evaln_max2";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    49
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    50
Goal "<c,s> -c-> t ==> ? n. <c,s> -n-> t";
10962
cda180b1e2e0 deleted several obsolete lemmas from NatArith.ML
paulson
parents: 9442
diff changeset
    51
by (etac evalc.induct 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    52
by (ALLGOALS (REPEAT o etac exE));
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    53
by (TRYALL(EVERY'[datac evaln_max2 1, REPEAT o eresolve_tac [exE, conjE]]));
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 13453
diff changeset
    54
by (ALLGOALS (rtac exI THEN' resolve_tac evaln.intros THEN_ALL_NEW atac));
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    55
qed "evalc_evaln";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    56
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    57
Goal "<c,s> -c-> t = (? n. <c,s> -n-> t)";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    58
by (fast_tac (claset() addEs [evalc_evaln, evaln_evalc]) 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    59
qed "eval_eq";