src/HOL/Induct/Comb.ML
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 5148 74919e8f221c
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/ex/comb.ML
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1996  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
Combinatory Logic example: the Church-Rosser Theorem
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
Curiously, combinators do not include free variables.
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
Example taken from
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
    J. Camilleri and T. F. Melham.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
    Report 265, University of Cambridge Computer Laboratory, 1992.
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
HOL system proofs may be found in
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
open Comb;
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
(*** Reflexive/Transitive closure preserves the Church-Rosser property 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
val [_, spec_mp] = [spec] RL [mp];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
    27
Goalw [diamond_def]
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
    28
    "[| diamond(r);  (x,y):r^* |] ==> \ 
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
by (etac rtrancl_induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
4301
ed343192de45 Changes to AddIs improve performance of Blast_tac
paulson
parents: 4089
diff changeset
    33
                          addSDs [spec_mp]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
by (rtac (impI RS allI RS allI) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
by (etac rtrancl_induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
by (slow_best_tac  (*Seems to be a brittle, undirected search*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
            addEs [major RS diamond_strip_lemmaE]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
qed "diamond_rtrancl";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
(*** Results about Contraction ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
(*Derive a case for each combinator constructor*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
val K_contractE = contract.mk_cases comb.simps "K -1-> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
val S_contractE = contract.mk_cases comb.simps "S -1-> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
AddSIs [contract.K, contract.S];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
AddIs  [contract.Ap1, contract.Ap2];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
AddSEs [K_contractE, S_contractE, Ap_contractE];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    58
Goalw [I_def] "I -1-> z ==> P";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
qed "I_contract_E";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
AddSEs [I_contract_E];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    63
Goal "K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
3120
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
qed "K1_contractD";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
AddSEs [K1_contractD];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    68
Goal "x ---> y ==> x#z ---> y#z";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
by (etac rtrancl_induct 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3724
diff changeset
    70
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
qed "Ap_reduce1";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    73
Goal "x ---> y ==> z#x ---> z#y";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
by (etac rtrancl_induct 1);
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3724
diff changeset
    75
by (ALLGOALS (blast_tac (claset() addIs [r_into_rtrancl, rtrancl_trans])));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
qed "Ap_reduce2";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
(** Counterexample to the diamond property for -1-> **)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
    80
Goal "K#I#(I#I) -1-> I";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
by (rtac contract.K 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
qed "KIII_contract1";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
    84
Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
qed "KIII_contract2";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    87
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
    88
Goal "K#I#((K#I)#(K#I)) -1-> I";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    89
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    90
qed "KIII_contract3";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    91
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
    92
Goalw [diamond_def] "~ diamond(contract)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3724
diff changeset
    93
by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    94
qed "not_diamond_contract";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    95
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    96
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    97
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    98
(*** Results about Parallel Contraction ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    99
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   100
(*Derive a case for each combinator constructor*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   101
val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   102
val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   103
val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   104
4301
ed343192de45 Changes to AddIs improve performance of Blast_tac
paulson
parents: 4089
diff changeset
   105
AddSIs [parcontract.refl, parcontract.K, parcontract.S];
ed343192de45 Changes to AddIs improve performance of Blast_tac
paulson
parents: 4089
diff changeset
   106
AddIs  [parcontract.Ap];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   107
AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   108
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   109
(*** Basic properties of parallel contraction ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   110
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   111
Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   112
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   113
qed "K1_parcontractD";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   114
AddSDs [K1_parcontractD];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   115
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   116
Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   117
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   118
qed "S1_parcontractD";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   119
AddSDs [S1_parcontractD];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   120
5148
74919e8f221c More tidying and removal of "\!\!... from Goal commands
paulson
parents: 5143
diff changeset
   121
Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   122
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   123
qed "S2_parcontractD";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   124
AddSDs [S2_parcontractD];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   125
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   126
(*The rules above are not essential but make proofs much faster*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   127
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   128
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   129
(*Church-Rosser property for parallel contraction*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   130
Goalw [diamond_def] "diamond parcontract";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   131
by (rtac (impI RS allI RS allI) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   132
by (etac parcontract.induct 1 THEN prune_params_tac);
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3207
diff changeset
   133
by Safe_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   134
by (ALLGOALS Blast_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   135
qed "diamond_parcontract";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   136
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   137
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   138
(*** Equivalence of x--->y and x===>y ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   139
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   140
Goal "contract <= parcontract";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   141
by (rtac subsetI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   142
by (split_all_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   143
by (etac contract.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   144
by (ALLGOALS Blast_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   145
qed "contract_subset_parcontract";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   146
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   147
(*Reductions: simply throw together reflexivity, transitivity and
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   148
  the one-step reductions*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   149
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   150
AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   151
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   152
(*Example only: not used*)
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   153
Goalw [I_def] "I#x ---> x";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   154
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   155
qed "reduce_I";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   156
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   157
Goal "parcontract <= contract^*";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   158
by (rtac subsetI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   159
by (split_all_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   160
by (etac parcontract.induct 1 THEN prune_params_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   161
by (ALLGOALS Blast_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   162
qed "parcontract_subset_reduce";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   163
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   164
Goal "contract^* = parcontract^*";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   165
by (REPEAT 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   166
    (resolve_tac [equalityI, 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   167
                  contract_subset_parcontract RS rtrancl_mono, 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   168
                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   169
qed "reduce_eq_parreduce";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   170
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4301
diff changeset
   171
Goal "diamond(contract^*)";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3724
diff changeset
   172
by (simp_tac (simpset() addsimps [reduce_eq_parreduce, diamond_rtrancl, 
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   173
                                 diamond_parcontract]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   174
qed "diamond_reduce";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   175
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   176
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   177
writeln"Reached end of file.";