src/HOL/Induct/Simult.ML
author paulson
Wed May 07 12:50:26 1997 +0200 (1997-05-07)
changeset 3120 c58423c20740
child 3842 b55686a7b22c
permissions -rw-r--r--
New directory to contain examples of (co)inductive definitions
paulson@3120
     1
(*  Title:      HOL/ex/Simult.ML
paulson@3120
     2
    ID:         $Id$
paulson@3120
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@3120
     4
    Copyright   1993  University of Cambridge
paulson@3120
     5
paulson@3120
     6
Primitives for simultaneous recursive type definitions
paulson@3120
     7
  includes worked example of trees & forests
paulson@3120
     8
paulson@3120
     9
This is essentially the same data structure that on ex/term.ML, which is
paulson@3120
    10
simpler because it uses list as a new type former.  The approach in this
paulson@3120
    11
file may be superior for other simultaneous recursions.
paulson@3120
    12
*)
paulson@3120
    13
paulson@3120
    14
open Simult;
paulson@3120
    15
paulson@3120
    16
(*** Monotonicity and unfolding of the function ***)
paulson@3120
    17
paulson@3120
    18
goal Simult.thy "mono(%Z.  A <*> Part Z In1 \
paulson@3120
    19
\                      <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))";
paulson@3120
    20
by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
paulson@3120
    21
                      Part_mono] 1));
paulson@3120
    22
qed "TF_fun_mono";
paulson@3120
    23
paulson@3120
    24
val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
paulson@3120
    25
paulson@3120
    26
goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
paulson@3120
    27
by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
paulson@3120
    28
qed "TF_mono";
paulson@3120
    29
paulson@3120
    30
goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
paulson@3120
    31
by (rtac lfp_lowerbound 1);
paulson@3120
    32
by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
paulson@3120
    33
                      addSEs [PartE]) 1);
paulson@3120
    34
qed "TF_sexp";
paulson@3120
    35
paulson@3120
    36
(* A <= sexp ==> TF(A) <= sexp *)
paulson@3120
    37
val TF_subset_sexp = standard
paulson@3120
    38
    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
paulson@3120
    39
paulson@3120
    40
paulson@3120
    41
(** Elimination -- structural induction on the set TF **)
paulson@3120
    42
paulson@3120
    43
val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
paulson@3120
    44
paulson@3120
    45
val major::prems = goalw Simult.thy TF_Rep_defs
paulson@3120
    46
 "[| i: TF(A);  \
paulson@3120
    47
\    !!M N. [| M: A;  N: Part (TF A) In1;  R(N) |] ==> R(TCONS M N);    \
paulson@3120
    48
\    R(FNIL);                   \
paulson@3120
    49
\    !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  R(M);  R(N) \
paulson@3120
    50
\            |] ==> R(FCONS M N)    \
paulson@3120
    51
\    |] ==> R(i)";
paulson@3120
    52
by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
paulson@3120
    53
by (blast_tac (!claset addIs (prems@[PartI])
paulson@3120
    54
                       addEs [usumE, uprodE, PartE]) 1);
paulson@3120
    55
qed "TF_induct";
paulson@3120
    56
paulson@3120
    57
(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
paulson@3120
    58
goalw Simult.thy [Part_def]
paulson@3120
    59
 "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
paulson@3120
    60
\                   (M: Part (TF A) In1 --> Q(M)) \
paulson@3120
    61
\  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
paulson@3120
    62
by (Blast_tac 1);
paulson@3120
    63
qed "TF_induct_lemma";
paulson@3120
    64
paulson@3120
    65
(*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
paulson@3120
    66
paulson@3120
    67
(*Induction on TF with separate predicates P, Q*)
paulson@3120
    68
val prems = goalw Simult.thy TF_Rep_defs
paulson@3120
    69
    "[| !!M N. [| M: A;  N: Part (TF A) In1;  Q(N) |] ==> P(TCONS M N); \
paulson@3120
    70
\       Q(FNIL);        \
paulson@3120
    71
\       !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  P(M);  Q(N) \
paulson@3120
    72
\               |] ==> Q(FCONS M N)     \
paulson@3120
    73
\    |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))";
paulson@3120
    74
by (rtac (ballI RS TF_induct_lemma) 1);
paulson@3120
    75
by (etac TF_induct 1);
paulson@3120
    76
by (rewrite_goals_tac TF_Rep_defs);
paulson@3120
    77
	(*Blast_tac needs this type instantiation in order to preserve the
paulson@3120
    78
          right overloading of equality.  The injectiveness properties for
paulson@3120
    79
          type 'a item hold only for set types.*)
paulson@3120
    80
val PartE' = read_instantiate [("'a", "?'c set")] PartE;
paulson@3120
    81
by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
paulson@3120
    82
qed "Tree_Forest_induct";
paulson@3120
    83
paulson@3120
    84
(*Induction for the abstract types 'a tree, 'a forest*)
paulson@3120
    85
val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
paulson@3120
    86
    "[| !!x ts. Q(ts) ==> P(Tcons x ts);     \
paulson@3120
    87
\       Q(Fnil);        \
paulson@3120
    88
\       !!t ts. [| P(t);  Q(ts) |] ==> Q(Fcons t ts)    \
paulson@3120
    89
\    |] ==> (! t. P(t)) & (! ts. Q(ts))";
paulson@3120
    90
by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
paulson@3120
    91
                  ("Q1","%z.Q(Abs_Forest(z))")] 
paulson@3120
    92
    (Tree_Forest_induct RS conjE) 1);
paulson@3120
    93
(*Instantiates ?A1 to range(Leaf). *)
paulson@3120
    94
by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
paulson@3120
    95
			      Rep_Forest_inverse RS subst] 
paulson@3120
    96
                       addSIs [Rep_Tree,Rep_Forest]) 4);
paulson@3120
    97
(*Cannot use simplifier: the rewrites work in the wrong direction!*)
paulson@3120
    98
by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
paulson@3120
    99
					Abs_Forest_inverse RS subst] 
paulson@3120
   100
                                addSIs prems)));
paulson@3120
   101
qed "tree_forest_induct";
paulson@3120
   102
paulson@3120
   103
paulson@3120
   104
paulson@3120
   105
(*** Isomorphisms ***)
paulson@3120
   106
paulson@3120
   107
goal Simult.thy "inj(Rep_Tree)";
paulson@3120
   108
by (rtac inj_inverseI 1);
paulson@3120
   109
by (rtac Rep_Tree_inverse 1);
paulson@3120
   110
qed "inj_Rep_Tree";
paulson@3120
   111
paulson@3120
   112
goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
paulson@3120
   113
by (rtac inj_onto_inverseI 1);
paulson@3120
   114
by (etac Abs_Tree_inverse 1);
paulson@3120
   115
qed "inj_onto_Abs_Tree";
paulson@3120
   116
paulson@3120
   117
goal Simult.thy "inj(Rep_Forest)";
paulson@3120
   118
by (rtac inj_inverseI 1);
paulson@3120
   119
by (rtac Rep_Forest_inverse 1);
paulson@3120
   120
qed "inj_Rep_Forest";
paulson@3120
   121
paulson@3120
   122
goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
paulson@3120
   123
by (rtac inj_onto_inverseI 1);
paulson@3120
   124
by (etac Abs_Forest_inverse 1);
paulson@3120
   125
qed "inj_onto_Abs_Forest";
paulson@3120
   126
paulson@3120
   127
(** Introduction rules for constructors **)
paulson@3120
   128
paulson@3120
   129
(* c : A <*> Part (TF A) In1 
paulson@3120
   130
        <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *)
paulson@3120
   131
val TF_I = TF_unfold RS equalityD2 RS subsetD;
paulson@3120
   132
paulson@3120
   133
(*For reasoning about the representation*)
paulson@3120
   134
AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
paulson@3120
   135
AddSEs [Scons_inject];
paulson@3120
   136
paulson@3120
   137
goalw Simult.thy TF_Rep_defs
paulson@3120
   138
    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
paulson@3120
   139
by (Blast_tac 1);
paulson@3120
   140
qed "TCONS_I";
paulson@3120
   141
paulson@3120
   142
(* FNIL is a TF(A) -- this also justifies the type definition*)
paulson@3120
   143
goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
paulson@3120
   144
by (Blast_tac 1);
paulson@3120
   145
qed "FNIL_I";
paulson@3120
   146
paulson@3120
   147
goalw Simult.thy TF_Rep_defs
paulson@3120
   148
    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
paulson@3120
   149
\         FCONS M N : Part (TF A) In1";
paulson@3120
   150
by (Blast_tac 1);
paulson@3120
   151
qed "FCONS_I";
paulson@3120
   152
paulson@3120
   153
(** Injectiveness of TCONS and FCONS **)
paulson@3120
   154
paulson@3120
   155
goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
paulson@3120
   156
by (Blast_tac 1);
paulson@3120
   157
qed "TCONS_TCONS_eq";
paulson@3120
   158
bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
paulson@3120
   159
paulson@3120
   160
goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
paulson@3120
   161
by (Blast_tac 1);
paulson@3120
   162
qed "FCONS_FCONS_eq";
paulson@3120
   163
bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
paulson@3120
   164
paulson@3120
   165
(** Distinctness of TCONS, FNIL and FCONS **)
paulson@3120
   166
paulson@3120
   167
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
paulson@3120
   168
by (Blast_tac 1);
paulson@3120
   169
qed "TCONS_not_FNIL";
paulson@3120
   170
bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
paulson@3120
   171
paulson@3120
   172
bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
paulson@3120
   173
val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
paulson@3120
   174
paulson@3120
   175
goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
paulson@3120
   176
by (Blast_tac 1);
paulson@3120
   177
qed "FCONS_not_FNIL";
paulson@3120
   178
bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
paulson@3120
   179
paulson@3120
   180
bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
paulson@3120
   181
val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
paulson@3120
   182
paulson@3120
   183
goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
paulson@3120
   184
by (Blast_tac 1);
paulson@3120
   185
qed "TCONS_not_FCONS";
paulson@3120
   186
bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
paulson@3120
   187
paulson@3120
   188
bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
paulson@3120
   189
val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
paulson@3120
   190
paulson@3120
   191
(*???? Too many derived rules ????
paulson@3120
   192
  Automatically generate symmetric forms?  Always expand TF_Rep_defs? *)
paulson@3120
   193
paulson@3120
   194
(** Injectiveness of Tcons and Fcons **)
paulson@3120
   195
paulson@3120
   196
(*For reasoning about abstract constructors*)
paulson@3120
   197
AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
paulson@3120
   198
AddSEs [TCONS_inject, FCONS_inject,
paulson@3120
   199
                           TCONS_neq_FNIL, FNIL_neq_TCONS,
paulson@3120
   200
                           FCONS_neq_FNIL, FNIL_neq_FCONS,
paulson@3120
   201
                           TCONS_neq_FCONS, FCONS_neq_TCONS];
paulson@3120
   202
AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
paulson@3120
   203
                           inj_onto_Abs_Forest RS inj_ontoD,
paulson@3120
   204
                           inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
paulson@3120
   205
                           Leaf_inject];
paulson@3120
   206
paulson@3120
   207
goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
paulson@3120
   208
by (Blast_tac 1);
paulson@3120
   209
qed "Tcons_Tcons_eq";
paulson@3120
   210
bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
paulson@3120
   211
paulson@3120
   212
goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
paulson@3120
   213
by (Blast_tac 1);
paulson@3120
   214
qed "Fcons_not_Fnil";
paulson@3120
   215
paulson@3120
   216
bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
paulson@3120
   217
val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
paulson@3120
   218
paulson@3120
   219
paulson@3120
   220
(** Injectiveness of Fcons **)
paulson@3120
   221
paulson@3120
   222
goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
paulson@3120
   223
by (Blast_tac 1);
paulson@3120
   224
qed "Fcons_Fcons_eq";
paulson@3120
   225
bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
paulson@3120
   226
paulson@3120
   227
paulson@3120
   228
(*** TF_rec -- by wf recursion on pred_sexp ***)
paulson@3120
   229
paulson@3120
   230
goal Simult.thy
paulson@3120
   231
   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
paulson@3120
   232
                         \       (%g. Case (Split(%x y. b x y (g y))) \
paulson@3120
   233
                         \           (List_case c (%x y. d x y (g x) (g y))))";
paulson@3120
   234
by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
paulson@3120
   235
val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
paulson@3120
   236
                    ((result() RS eq_reflection) RS def_wfrec);
paulson@3120
   237
paulson@3120
   238
(*---------------------------------------------------------------------------
paulson@3120
   239
 * Old: 
paulson@3120
   240
 * val TF_rec_unfold =
paulson@3120
   241
 *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
paulson@3120
   242
 *---------------------------------------------------------------------------*)
paulson@3120
   243
paulson@3120
   244
(** conversion rules for TF_rec **)
paulson@3120
   245
paulson@3120
   246
goalw Simult.thy [TCONS_def]
paulson@3120
   247
    "!!M N. [| M: sexp;  N: sexp |] ==>         \
paulson@3120
   248
\           TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
paulson@3120
   249
by (rtac (TF_rec_unfold RS trans) 1);
paulson@3120
   250
by (simp_tac (!simpset addsimps [Case_In0, Split]) 1);
paulson@3120
   251
by (asm_simp_tac (!simpset addsimps [In0_def]) 1);
paulson@3120
   252
qed "TF_rec_TCONS";
paulson@3120
   253
paulson@3120
   254
goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c";
paulson@3120
   255
by (rtac (TF_rec_unfold RS trans) 1);
paulson@3120
   256
by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
paulson@3120
   257
qed "TF_rec_FNIL";
paulson@3120
   258
paulson@3120
   259
goalw Simult.thy [FCONS_def]
paulson@3120
   260
 "!!M N. [| M: sexp;  N: sexp |] ==>    \
paulson@3120
   261
\        TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
paulson@3120
   262
by (rtac (TF_rec_unfold RS trans) 1);
paulson@3120
   263
by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
paulson@3120
   264
by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1);
paulson@3120
   265
qed "TF_rec_FCONS";
paulson@3120
   266
paulson@3120
   267
paulson@3120
   268
(*** tree_rec, forest_rec -- by TF_rec ***)
paulson@3120
   269
paulson@3120
   270
val Rep_Tree_in_sexp =
paulson@3120
   271
    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
paulson@3120
   272
     Rep_Tree] MRS subsetD;
paulson@3120
   273
val Rep_Forest_in_sexp =
paulson@3120
   274
    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
paulson@3120
   275
     Rep_Forest] MRS subsetD;
paulson@3120
   276
paulson@3120
   277
val tf_rec_ss = HOL_ss addsimps
paulson@3120
   278
  [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
paulson@3120
   279
   TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
paulson@3120
   280
   Rep_Tree_inverse, Rep_Forest_inverse,
paulson@3120
   281
   Abs_Tree_inverse, Abs_Forest_inverse,
paulson@3120
   282
   inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
paulson@3120
   283
   Rep_Tree_in_sexp, Rep_Forest_in_sexp];
paulson@3120
   284
paulson@3120
   285
goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
paulson@3120
   286
    "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)";
paulson@3120
   287
by (simp_tac tf_rec_ss 1);
paulson@3120
   288
qed "tree_rec_Tcons";
paulson@3120
   289
paulson@3120
   290
goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c";
paulson@3120
   291
by (simp_tac tf_rec_ss 1);
paulson@3120
   292
qed "forest_rec_Fnil";
paulson@3120
   293
paulson@3120
   294
goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
paulson@3120
   295
    "forest_rec (Fcons t tf) b c d = \
paulson@3120
   296
\    d t tf (tree_rec t b c d) (forest_rec tf b c d)";
paulson@3120
   297
by (simp_tac tf_rec_ss 1);
paulson@3120
   298
qed "forest_rec_Cons";