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