--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ex/Simult.ML Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,319 @@
+(* Title: HOL/ex/simult.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+For simult.thy.
+
+Primitives for simultaneous recursive type definitions
+ includes worked example of trees & forests
+
+This is essentially the same data structure that on ex/term.ML, which is
+simpler because it uses List as a new type former. The approach in this
+file may be superior for other simultaneous recursions.
+*)
+
+open Simult;
+
+(*** General rules for Part ***)
+
+val prems = goalw Simult.thy [Part_def] "h(a) : A ==> h(a) : Part(A,h)";
+by (cfast_tac prems 1);
+val PartI = result();
+
+val major::prems = goalw Simult.thy [Part_def]
+ "[| a : Part(A,h); !!z. [| a : A; a=h(z) |] ==> P \
+\ |] ==> P";
+by (rtac (major RS CollectE) 1);
+by (etac conjE 1);
+by (etac exE 1);
+by (REPEAT (ares_tac prems 1));
+val PartE = result();
+
+goal Simult.thy "!!A B. A<=B ==> Part(A,h) <= Part(B,h)";
+by (fast_tac (set_cs addSIs [PartI] addSEs [PartE]) 1);
+val Part_mono = result();
+
+val [prem] = goal Simult.thy "A<=B ==> Part(A,h) <= B";
+by (fast_tac (set_cs addSIs [PartI, prem RS subsetD] addSEs [PartE]) 1);
+val Part_subset = result();
+
+
+(*** Monotonicity and unfolding of the function ***)
+
+goal Simult.thy "mono(%Z. A <*> Part(Z,In1) \
+\ <+> ({Numb(0)} <+> Part(Z,In0) <*> Part(Z,In1)))";
+by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
+ Part_mono] 1));
+val TF_fun_mono = result();
+
+val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
+
+goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
+by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
+val TF_mono = result();
+
+goalw Simult.thy [TF_def] "TF(Sexp) <= Sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (univ_cs addIs [Sexp_NumbI,Sexp_In0I,Sexp_In1I,Sexp_SconsI]
+ addSEs [PartE]) 1);
+val TF_Sexp = result();
+
+(* A <= Sexp ==> TF(A) <= Sexp *)
+val TF_subset_Sexp = standard
+ (TF_mono RS (TF_Sexp RSN (2,subset_trans)));
+
+
+(** Elimination -- structural induction on the set TF **)
+
+val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
+
+val major::prems = goalw Simult.thy TF_Rep_defs
+ "[| i: TF(A); \
+\ !!M N. [| M: A; N: Part(TF(A),In1); R(N) |] ==> R(TCONS(M,N)); \
+\ R(FNIL); \
+\ !!M N. [| M: Part(TF(A),In0); N: Part(TF(A),In1); R(M); R(N) \
+\ |] ==> R(FCONS(M,N)) \
+\ |] ==> R(i)";
+by (rtac (major RS (TF_def RS def_induct)) 1);
+by (rtac TF_fun_mono 1);
+by (fast_tac (set_cs addIs (prems@[PartI])
+ addEs [usumE, uprodE, PartE]) 1);
+val TF_induct = result();
+
+(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
+val prems = goalw Simult.thy [Part_def]
+ "! M: TF(A). (M: Part(TF(A),In0) --> P(M)) & (M: Part(TF(A),In1) --> Q(M)) \
+\ ==> (! M: Part(TF(A),In0). P(M)) & (! M: Part(TF(A),In1). Q(M))";
+by (cfast_tac prems 1);
+val TF_induct_lemma = result();
+
+val uplus_cs = set_cs addSIs [PartI]
+ addSDs [In0_inject, In1_inject]
+ addSEs [In0_neq_In1, In1_neq_In0, PartE];
+
+(*Could prove ~ TCONS(M,N) : Part(TF(A),In1) etc. *)
+
+(*Induction on TF with separate predicates P, Q*)
+val prems = goalw Simult.thy TF_Rep_defs
+ "[| !!M N. [| M: A; N: Part(TF(A),In1); Q(N) |] ==> P(TCONS(M,N)); \
+\ Q(FNIL); \
+\ !!M N. [| M: Part(TF(A),In0); N: Part(TF(A),In1); P(M); Q(N) \
+\ |] ==> Q(FCONS(M,N)) \
+\ |] ==> (! M: Part(TF(A),In0). P(M)) & (! N: Part(TF(A),In1). Q(N))";
+by (rtac (ballI RS TF_induct_lemma) 1);
+by (etac TF_induct 1);
+by (rewrite_goals_tac TF_Rep_defs);
+by (ALLGOALS (fast_tac (uplus_cs addIs prems)));
+(*29 secs??*)
+val Tree_Forest_induct = result();
+
+(*Induction for the abstract types 'a tree, 'a forest*)
+val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
+ "[| !!x ts. Q(ts) ==> P(Tcons(x,ts)); \
+\ Q(Fnil); \
+\ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons(t,ts)) \
+\ |] ==> (! t. P(t)) & (! ts. Q(ts))";
+by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
+ ("Q1","%z.Q(Abs_Forest(z))")]
+ (Tree_Forest_induct RS conjE) 1);
+(*Instantiates ?A1 to range(Leaf). *)
+by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst,
+ Rep_Forest_inverse RS subst]
+ addSIs [Rep_Tree,Rep_Forest]) 4);
+(*Cannot use simplifier: the rewrites work in the wrong direction!*)
+by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst,
+ Abs_Forest_inverse RS subst]
+ addSIs prems)));
+val tree_forest_induct = result();
+
+
+
+(*** Isomorphisms ***)
+
+goal Simult.thy "inj(Rep_Tree)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Tree_inverse 1);
+val inj_Rep_Tree = result();
+
+goal Simult.thy "inj_onto(Abs_Tree,Part(TF(range(Leaf)),In0))";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_Tree_inverse 1);
+val inj_onto_Abs_Tree = result();
+
+goal Simult.thy "inj(Rep_Forest)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Forest_inverse 1);
+val inj_Rep_Forest = result();
+
+goal Simult.thy "inj_onto(Abs_Forest,Part(TF(range(Leaf)),In1))";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_Forest_inverse 1);
+val inj_onto_Abs_Forest = result();
+
+(** Introduction rules for constructors **)
+
+(* c : A <*> Part(TF(A),In1)
+ <+> {Numb(0)} <+> Part(TF(A),In0) <*> Part(TF(A),In1) ==> c : TF(A) *)
+val TF_I = TF_unfold RS equalityD2 RS subsetD;
+
+(*For reasoning about the representation*)
+val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I]
+ addSEs [Scons_inject];
+
+val prems = goalw Simult.thy TF_Rep_defs
+ "[| a: A; M: Part(TF(A),In1) |] ==> TCONS(a,M) : Part(TF(A),In0)";
+by (fast_tac (TF_Rep_cs addIs prems) 1);
+val TCONS_I = result();
+
+(* FNIL is a TF(A) -- this also justifies the type definition*)
+goalw Simult.thy TF_Rep_defs "FNIL: Part(TF(A),In1)";
+by (fast_tac TF_Rep_cs 1);
+val FNIL_I = result();
+
+val prems = goalw Simult.thy TF_Rep_defs
+ "[| M: Part(TF(A),In0); N: Part(TF(A),In1) |] ==> \
+\ FCONS(M,N) : Part(TF(A),In1)";
+by (fast_tac (TF_Rep_cs addIs prems) 1);
+val FCONS_I = result();
+
+(** Injectiveness of TCONS and FCONS **)
+
+goalw Simult.thy TF_Rep_defs "(TCONS(K,M)=TCONS(L,N)) = (K=L & M=N)";
+by (fast_tac TF_Rep_cs 1);
+val TCONS_TCONS_eq = result();
+val TCONS_inject = standard (TCONS_TCONS_eq RS iffD1 RS conjE);
+
+goalw Simult.thy TF_Rep_defs "(FCONS(K,M)=FCONS(L,N)) = (K=L & M=N)";
+by (fast_tac TF_Rep_cs 1);
+val FCONS_FCONS_eq = result();
+val FCONS_inject = standard (FCONS_FCONS_eq RS iffD1 RS conjE);
+
+(** Distinctness of TCONS, FNIL and FCONS **)
+
+goalw Simult.thy TF_Rep_defs "~ TCONS(M,N) = FNIL";
+by (fast_tac TF_Rep_cs 1);
+val TCONS_not_FNIL = result();
+val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
+
+val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
+val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
+
+goalw Simult.thy TF_Rep_defs "~ FCONS(M,N) = FNIL";
+by (fast_tac TF_Rep_cs 1);
+val FCONS_not_FNIL = result();
+val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
+
+val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
+val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
+
+goalw Simult.thy TF_Rep_defs "~ TCONS(M,N) = FCONS(K,L)";
+by (fast_tac TF_Rep_cs 1);
+val TCONS_not_FCONS = result();
+val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
+
+val TCONS_neq_FCONS = standard (TCONS_not_FCONS RS notE);
+val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
+
+(*???? Too many derived rules ????
+ Automatically generate symmetric forms? Always expand TF_Rep_defs? *)
+
+(** Injectiveness of Tcons and Fcons **)
+
+(*For reasoning about abstract constructors*)
+val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I]
+ addSEs [TCONS_inject, FCONS_inject,
+ TCONS_neq_FNIL, FNIL_neq_TCONS,
+ FCONS_neq_FNIL, FNIL_neq_FCONS,
+ TCONS_neq_FCONS, FCONS_neq_TCONS]
+ addSDs [inj_onto_Abs_Tree RS inj_ontoD,
+ inj_onto_Abs_Forest RS inj_ontoD,
+ inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
+ Leaf_inject];
+
+goalw Simult.thy [Tcons_def] "(Tcons(x,xs)=Tcons(y,ys)) = (x=y & xs=ys)";
+by (fast_tac TF_cs 1);
+val Tcons_Tcons_eq = result();
+val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
+
+goalw Simult.thy [Fcons_def,Fnil_def] "~ Fcons(x,xs) = Fnil";
+by (fast_tac TF_cs 1);
+val Fcons_not_Fnil = result();
+
+val Fcons_neq_Fnil = standard (Fcons_not_Fnil RS notE);;
+val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
+
+
+(** Injectiveness of Fcons **)
+
+goalw Simult.thy [Fcons_def] "(Fcons(x,xs)=Fcons(y,ys)) = (x=y & xs=ys)";
+by (fast_tac TF_cs 1);
+val Fcons_Fcons_eq = result();
+val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE);
+
+
+(*** TF_rec -- by wf recursion on pred_Sexp ***)
+
+val TF_rec_unfold =
+ wf_pred_Sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+
+(** conversion rules for TF_rec **)
+
+val prems = goalw Simult.thy [TCONS_def]
+ "[| M: Sexp; N: Sexp |] ==> \
+\ TF_rec(TCONS(M,N),b,c,d) = b(M, N, TF_rec(N,b,c,d))";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (rtac (Case_In0 RS trans) 1);
+by (rtac (Split RS trans) 1);
+by (rewtac In0_def);
+by (simp_tac (pred_Sexp_ss addsimps prems) 1);
+val TF_rec_TCONS = result();
+
+goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (rtac (Case_In1 RS trans) 1);
+by (rtac List_case_NIL 1);
+val TF_rec_FNIL = result();
+
+val prems = goalw Simult.thy [FCONS_def]
+ "[| M: Sexp; N: Sexp |] ==> \
+\ TF_rec(FCONS(M,N),b,c,d) = d(M, N, TF_rec(M,b,c,d), TF_rec(N,b,c,d))";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (rtac (Case_In1 RS trans) 1);
+by (rtac (List_case_CONS RS trans) 1);
+by (rewrite_goals_tac [CONS_def,In1_def]);
+by (simp_tac (pred_Sexp_ss addsimps prems) 1);
+val TF_rec_FCONS = result();
+
+
+(*** tree_rec, forest_rec -- by TF_rec ***)
+
+val Rep_Tree_in_Sexp =
+ Rep_Tree RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS
+ Part_subset RS subsetD);
+val Rep_Forest_in_Sexp =
+ Rep_Forest RS (range_Leaf_subset_Sexp RS TF_subset_Sexp RS
+ Part_subset RS subsetD);
+
+val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
+ TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
+ Rep_Tree_inverse, Rep_Forest_inverse,
+ Abs_Tree_inverse, Abs_Forest_inverse,
+ inj_Leaf, Inv_f_f, Sexp_LeafI, range_eqI,
+ Rep_Tree_in_Sexp, Rep_Forest_in_Sexp];
+val tf_rec_ss = HOL_ss addsimps tf_rec_simps;
+
+goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
+ "tree_rec(Tcons(a,tf),b,c,d) = b(a,tf,forest_rec(tf,b,c,d))";
+by (simp_tac tf_rec_ss 1);
+val tree_rec_Tcons = result();
+
+goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec(Fnil,b,c,d) = c";
+by (simp_tac tf_rec_ss 1);
+val forest_rec_Fnil = result();
+
+goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
+ "forest_rec(Fcons(t,tf),b,c,d) = \
+\ d(t,tf,tree_rec(t,b,c,d), forest_rec(tf,b,c,d))";
+by (simp_tac tf_rec_ss 1);
+val forest_rec_Cons = result();