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