src/HOL/Induct/Exp.ML
author paulson
Wed, 07 May 1997 12:50:26 +0200
changeset 3120 c58423c20740
child 3144 04b0d8941365
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Induct/Exp
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
open Exp;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
val eval_elim_cases = map (eval.mk_cases exp.simps)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
   ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
    "(Op f a1 a2,sigma)  -|-> (n,s')",
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
    "(VALOF c RESULTIS e, s) -|-> (n, s1)"
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
   ];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
AddSEs eval_elim_cases;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
(** Make the induction rule look nicer -- though eta_contract makes the new
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
    version look worse than it is...**)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
goal thy "{((e,s),(n,s')). P e s n s'} = \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
\         Collect (split (%v. split (split P v)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
by (rtac Collect_cong 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
by (split_all_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
by (Simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
val split_lemma = result();
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
(*New induction rule.  Note the form of the VALOF induction hypothesis*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
val major::prems = goal thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
  "[| (e,s) -|-> (n,s');                                         \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
\     !!n s. P (N n) s n s;                                      \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
\     !!s x. P (X x) s (s x) s;                                  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
\     !!e0 e1 f n0 n1 s s0 s1.                                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
\        [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
\           (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
\        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
\     !!c e n s s0 s1.                                           \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
\        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
\           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
\        ==> P (VALOF c RESULTIS e) s n s1                       \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
\  |] ==> P e s n s'";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
by (rtac (major RS eval.induct) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
by (blast_tac (!claset addIs prems) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
by (blast_tac (!claset addIs prems) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
by (blast_tac (!claset addIs prems) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
qed "eval_induct";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
(*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
  using eval restricted to its functional part.  Note that the execution
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
  functional on the argument (c,s).
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
goal thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
    "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
\         ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
by (etac exec.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
by (ALLGOALS Full_simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
by (Blast_tac 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
by (rewtac Unique_def);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    70
by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
by (etac exec_WHILE_case 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
qed "com_Unique";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
(*Expression evaluation is functional, or deterministic*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
goal thy "Function eval";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
by (simp_tac (!simpset addsimps [Function_def]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
by (REPEAT (rtac allI 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
by (rtac impI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
by (etac eval_induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
by (dtac com_Unique 4);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    84
by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
by (ALLGOALS Blast_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
qed "Function_eval";