# HG changeset patch # User berghofe # Date 909140077 -7200 # Node ID 8a1be8e50d9fa3b3bfd3e4bc65c31e638d76fdbc # Parent 6b8bb85c384808ae55185d1291aae8dc93869e44 Removed obsolete theory Simult (see theory Term). diff -r 6b8bb85c3848 -r 8a1be8e50d9f src/HOL/Induct/Simult.ML --- a/src/HOL/Induct/Simult.ML Fri Oct 23 12:31:23 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,291 +0,0 @@ -(* Title: HOL/ex/Simult.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -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. -*) - -(*** Monotonicity and unfolding of the function ***) - -Goal "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)); -qed "TF_fun_mono"; - -val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski); - -Goalw [TF_def] "A<=B ==> TF(A) <= TF(B)"; -by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1)); -qed "TF_mono"; - -Goalw [TF_def] "TF(sexp) <= sexp"; -by (rtac lfp_lowerbound 1); -by (blast_tac (claset() addIs sexp.intrs@[sexp_In0I, sexp_In1I] - addSEs [PartE]) 1); -qed "TF_sexp"; - -(* 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 ([TF_def, TF_fun_mono, major] MRS def_induct) 1); -by (blast_tac (claset() addIs prems@[PartI] addEs [usumE, uprodE, PartE]) 1); -qed "TF_induct"; - -(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*) -Goalw [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 (Blast_tac 1); -qed "TF_induct_lemma"; - -(*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 (blast_tac (claset() addIs prems))); -qed "Tree_Forest_induct"; - -(*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 (claset() 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 (claset() addSEs [Abs_Tree_inverse RS subst, - Abs_Forest_inverse RS subst] - addSIs prems))); -qed "tree_forest_induct"; - - - -(*** Isomorphisms ***) - -Goal "inj(Rep_Tree)"; -by (rtac inj_inverseI 1); -by (rtac Rep_Tree_inverse 1); -qed "inj_Rep_Tree"; - -Goal "inj_on Abs_Tree (Part (TF(range Leaf)) In0)"; -by (rtac inj_on_inverseI 1); -by (etac Abs_Tree_inverse 1); -qed "inj_on_Abs_Tree"; - -Goal "inj(Rep_Forest)"; -by (rtac inj_inverseI 1); -by (rtac Rep_Forest_inverse 1); -qed "inj_Rep_Forest"; - -Goal "inj_on Abs_Forest (Part (TF(range Leaf)) In1)"; -by (rtac inj_on_inverseI 1); -by (etac Abs_Forest_inverse 1); -qed "inj_on_Abs_Forest"; - -(** 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*) -AddIs [TF_I, uprodI, usum_In0I, usum_In1I]; -AddSEs [Scons_inject]; - -Goalw TF_Rep_defs - "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0"; -by (Blast_tac 1); -qed "TCONS_I"; - -(* FNIL is a TF(A) -- this also justifies the type definition*) -Goalw TF_Rep_defs "FNIL: Part (TF A) In1"; -by (Blast_tac 1); -qed "FNIL_I"; - -Goalw TF_Rep_defs - "[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \ -\ FCONS M N : Part (TF A) In1"; -by (Blast_tac 1); -qed "FCONS_I"; - -(** Injectiveness of TCONS and FCONS **) - -Goalw TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)"; -by (Blast_tac 1); -qed "TCONS_TCONS_eq"; -bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE)); - -Goalw TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)"; -by (Blast_tac 1); -qed "FCONS_FCONS_eq"; -bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE)); - -(** Distinctness of TCONS, FNIL and FCONS **) - -Goalw TF_Rep_defs "TCONS M N ~= FNIL"; -by (Blast_tac 1); -qed "TCONS_not_FNIL"; -bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym)); - -bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE)); -val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL; - -Goalw TF_Rep_defs "FCONS M N ~= FNIL"; -by (Blast_tac 1); -qed "FCONS_not_FNIL"; -bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym)); - -bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE)); -val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL; - -Goalw TF_Rep_defs "TCONS M N ~= FCONS K L"; -by (Blast_tac 1); -qed "TCONS_not_FCONS"; -bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym)); - -bind_thm ("TCONS_neq_FCONS", (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*) -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_on_Abs_Tree RS inj_onD, - inj_on_Abs_Forest RS inj_onD, - inj_Rep_Tree RS injD, inj_Rep_Forest RS injD, - Leaf_inject]; - -Goalw [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)"; -by (Blast_tac 1); -qed "Tcons_Tcons_eq"; -bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE)); - -Goalw [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil"; -by (Blast_tac 1); -qed "Fcons_not_Fnil"; - -bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE); -val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil; - - -(** Injectiveness of Fcons **) - -Goalw [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)"; -by (Blast_tac 1); -qed "Fcons_Fcons_eq"; -bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE); - - -(*** TF_rec -- by wf recursion on pred_sexp ***) - -Goal - "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \ - \ (%g. Case (Split(%x y. b x y (g y))) \ - \ (List_case c (%x y. d x y (g x) (g y))))"; -by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1); -val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS - ((result() RS eq_reflection) RS def_wfrec); - -(*--------------------------------------------------------------------------- - * Old: - * val TF_rec_unfold = - * wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec); - *---------------------------------------------------------------------------*) - -(** conversion rules for TF_rec **) - -Goalw [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 (simp_tac (simpset() addsimps [Case_In0, Split]) 1); -by (asm_simp_tac (simpset() addsimps [In0_def]) 1); -qed "TF_rec_TCONS"; - -Goalw [FNIL_def] "TF_rec FNIL b c d = c"; -by (rtac (TF_rec_unfold RS trans) 1); -by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1); -qed "TF_rec_FNIL"; - -Goalw [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 (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1); -by (asm_simp_tac (simpset() addsimps [CONS_def,In1_def]) 1); -qed "TF_rec_FCONS"; - - -(*** tree_rec, forest_rec -- by TF_rec ***) - -val Rep_Tree_in_sexp = - [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans), - Rep_Tree] MRS subsetD; -val Rep_Forest_in_sexp = - [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans), - Rep_Forest] MRS subsetD; - -val tf_rec_ss = HOL_ss addsimps - [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]; - -Goalw [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); -qed "tree_rec_Tcons"; - -Goalw [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c"; -by (simp_tac tf_rec_ss 1); -qed "forest_rec_Fnil"; - -Goalw [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); -qed "forest_rec_Cons"; diff -r 6b8bb85c3848 -r 8a1be8e50d9f src/HOL/Induct/Simult.thy --- a/src/HOL/Induct/Simult.thy Fri Oct 23 12:31:23 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -(* Title: HOL/ex/Simult - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -A simultaneous recursive type definition: 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. - -The inductive definition package does not help defining this sort of mutually -recursive data structure because it uses Inl, Inr instead of In0, In1. -*) - -Simult = SList + - -types 'a tree - 'a forest - -arities tree,forest :: (term)term - -consts - TF :: 'a item set => 'a item set - FNIL :: 'a item - TCONS,FCONS :: ['a item, 'a item] => 'a item - Rep_Tree :: 'a tree => 'a item - Abs_Tree :: 'a item => 'a tree - Rep_Forest :: 'a forest => 'a item - Abs_Forest :: 'a item => 'a forest - Tcons :: ['a, 'a forest] => 'a tree - Fcons :: ['a tree, 'a forest] => 'a forest - Fnil :: 'a forest - TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b, - 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b - tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b, - 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b - forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b, - 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b - -defs - (*the concrete constants*) - TCONS_def "TCONS M N == In0 (Scons M N)" - FNIL_def "FNIL == In1(NIL)" - FCONS_def "FCONS M N == In1(CONS M N)" - (*the abstract constants*) - Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))" - Fnil_def "Fnil == Abs_Forest(FNIL)" - Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))" - - TF_def "TF(A) == lfp(%Z. A <*> Part Z In1 - <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))" - -rules - (*faking a type definition for tree...*) - Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0" - Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t" - Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z" - (*faking a type definition for forest...*) - Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1" - Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" - Abs_Forest_inverse - "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z" - - -defs - (*recursion*) - TF_rec_def - "TF_rec M b c d == wfrec (trancl pred_sexp) - (%g. Case (Split(%x y. b x y (g y))) - (List_case c (%x y. d x y (g x) (g y)))) M" - - tree_rec_def - "tree_rec t b c d == - TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) - c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" - - forest_rec_def - "forest_rec tf b c d == - TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) - c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" -end