diff -r 000000000000 -r 7949f97df77a ex/simult.ML --- /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();