src/HOL/Induct/Com.ML
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 5143 b94cd208f073
child 5223 4cb05273f764
permissions -rw-r--r--
Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
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/Com
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: Commands
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 Com;
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
AddIs exec.intrs;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
val exec_elim_cases = map (exec.mk_cases exp.simps)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
   ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
    "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
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
val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
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
AddSEs exec_elim_cases;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
(*This theorem justifies using "exec" in the inductive definition of "eval"*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    22
Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
by (rtac lfp_mono 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
by (REPEAT (ares_tac basic_monos 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
qed "exec_mono";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
Unify.trace_bound := 30;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
Unify.search_bound := 60;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
(*Command execution is functional (deterministic) provided evaluation is*)
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    32
Goal "Function ev ==> Function(exec ev)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    33
by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
by (REPEAT (rtac allI 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
by (rtac impI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
by (etac exec.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
by (Blast_tac 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
by (rewrite_goals_tac [Function_def, Unique_def]);
3142
a6f73a02c619 Made a slow proof slightly faster
paulson
parents: 3120
diff changeset
    40
by (thin_tac "(?c,s1) -[ev]-> s2" 5);
4390
57e16404c2a9 ugly patch for new Blast_tac
paulson
parents: 4089
diff changeset
    41
by (rotate_tac 1 5);   (*PATCH to avoid very slow proof*)
3142
a6f73a02c619 Made a slow proof slightly faster
paulson
parents: 3120
diff changeset
    42
(*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*)
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    43
by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
qed "Function_exec";
3147
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    45
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    46
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    47
Goalw [assign_def] "(s[v/x])x = v";
3147
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    48
by (Simp_tac 1);
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    49
qed "assign_same";
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    50
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    51
Goalw [assign_def] "y~=x ==> (s[v/x])y = s y";
3147
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    52
by (Asm_simp_tac 1);
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    53
qed "assign_different";
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    54
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    55
Goalw [assign_def] "s[s x/x] = s";
3457
a8ab7c64817c Ran expandshort
paulson
parents: 3147
diff changeset
    56
by (rtac ext 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4390
diff changeset
    57
by (Simp_tac 1);
3147
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    58
qed "assign_triv";
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    59
49f2614732ea New theorems about "assign"
paulson
parents: 3142
diff changeset
    60
Addsimps [assign_same, assign_different, assign_triv];