# HG changeset patch # User lcp # Date 777804453 -7200 # Node ID d9527f97246ea16420bd43031ca901ac8d979c77 # Parent 872f866e630fa3f3f2c2f6cba1d59c7ea2e1eed9 INSTALLATION OF INDUCTIVE DEFINITIONS HOL/ex/MT.thy: now mentions dependence upon Sum.thy HOL/ex/Acc: new example, borrowed & adapted from ZF HOL/ex/Simult, ex/Term: updated refs to Sexp intr rules HOL/Sexp,List,LList,ex/Term: converted as follows node *set -> item Sexp -> sexp LList_corec -> LList_ -> llist_ LList\> -> llist List_case -> List_rec -> List_ -> list_ List\> -> list Term_rec -> Term_ -> term_ Term\> -> term diff -r 872f866e630f -r d9527f97246e ex/Acc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/Acc.ML Thu Aug 25 10:47:33 1994 +0200 @@ -0,0 +1,63 @@ +(* Title: HOL/ex/Acc + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +open Acc; + +(*The intended introduction rule*) +val prems = goal Acc.thy + "[| !!b. :r ==> b: acc(r) |] ==> a: acc(r)"; +by (fast_tac (set_cs addIs (prems @ + map (rewrite_rule [pred_def]) acc.intrs)) 1); +val accI = result(); + +goal Acc.thy "!!a b r. [| b: acc(r); : r |] ==> a: acc(r)"; +by (etac acc.elim 1); +by (rewtac pred_def); +by (fast_tac set_cs 1); +val acc_downward = result(); + +val [major,indhyp] = goal Acc.thy + "[| a : acc(r); \ +\ !!x. [| x: acc(r); ALL y. :r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (rtac (major RS acc.induct) 1); +by (rtac indhyp 1); +by (resolve_tac acc.intrs 1); +by (rewtac pred_def); +by (fast_tac set_cs 2); +be (Int_lower1 RS Pow_mono RS subsetD) 1; +val acc_induct = result(); + + +val [major] = goal Acc.thy "r <= Sigma(acc(r), %u. acc(r)) ==> wf(r)"; +by (rtac (major RS wfI) 1); +by (etac acc.induct 1); +by (rewtac pred_def); +by (fast_tac set_cs 1); +val acc_wfI = result(); + +val [major] = goal Acc.thy "wf(r) ==> ALL x. : r | :r --> y: acc(r)"; +by (rtac (major RS wf_induct) 1); +br (impI RS allI) 1; +br accI 1; +by (fast_tac set_cs 1); +val acc_wfD_lemma = result(); + +val [major] = goal Acc.thy "wf(r) ==> r <= Sigma(acc(r), %u. acc(r))"; +by (rtac subsetI 1); +by (res_inst_tac [("p", "x")] PairE 1); +by (fast_tac (set_cs addSIs [SigmaI, + major RS acc_wfD_lemma RS spec RS mp]) 1); +val acc_wfD = result(); + +goal Acc.thy "wf(r) = (r <= Sigma(acc(r), %u. acc(r)))"; +by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); +val wf_acc_iff = result(); diff -r 872f866e630f -r d9527f97246e ex/Acc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ex/Acc.thy Thu Aug 25 10:47:33 1994 +0200 @@ -0,0 +1,26 @@ +(* Title: HOL/ex/Acc.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +Acc = WF + + +consts + pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) + acc :: "('a * 'a)set => 'a set" (*Accessible part*) + +defs + pred_def "pred(x,r) == {y. :r}" + +inductive "acc(r)" + intrs + pred "pred(a,r): Pow(acc(r)) ==> a: acc(r)" + monos "[Pow_mono]" + +end diff -r 872f866e630f -r d9527f97246e ex/PL.ML --- a/ex/PL.ML Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/PL.ML Thu Aug 25 10:47:33 1994 +0200 @@ -101,8 +101,7 @@ \ !!x. P(((x->false)->false)->x); \ \ !!x y. [| H |- x->y; H |- x; P(x->y); P(x) |] ==> P(y) \ \ |] ==> P(a)"; -by (rtac (major RS (thms_def RS def_induct)) 1); -by (rtac thms_bnd_mono 1); +by (rtac ([thms_def, thms_bnd_mono, major] MRS def_induct) 1); by (rewrite_tac rule_defs); by (fast_tac (set_cs addIs prems) 1); val conseq_induct = result(); @@ -267,7 +266,7 @@ goal PL.thy "hyps(p,t) : Fin(UN v:{x.True}. {#v, #v->false})"; by (PL.pl.induct_tac "p" 1); by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN' - fast_tac (set_cs addSIs [Fin_0I, Fin_insertI, Fin_UnI]))); + fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI]))); val hyps_finite = result(); val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; diff -r 872f866e630f -r d9527f97246e ex/ROOT.ML --- a/ex/ROOT.ML Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/ROOT.ML Thu Aug 25 10:47:33 1994 +0200 @@ -20,6 +20,7 @@ time_use_thy "Puzzle"; time_use_thy "NatSum"; time_use "ex/set.ML"; +time_use_thy "Acc"; time_use_thy "PL"; time_use_thy "Term"; time_use_thy "Simult"; diff -r 872f866e630f -r d9527f97246e ex/Simult.ML --- a/ex/Simult.ML Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/Simult.ML Thu Aug 25 10:47:33 1994 +0200 @@ -3,13 +3,11 @@ 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 +simpler because it uses list as a new type former. The approach in this file may be superior for other simultaneous recursions. *) @@ -29,15 +27,15 @@ 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"; +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] +by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I, sexp_In1I] addSEs [PartE]) 1); -val TF_Sexp = result(); +val TF_sexp = result(); -(* A <= Sexp ==> TF(A) <= Sexp *) -val TF_subset_Sexp = standard - (TF_mono RS (TF_Sexp RSN (2,subset_trans))); +(* 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 **) @@ -51,8 +49,7 @@ \ !!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 (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1); by (fast_tac (set_cs addIs (prems@[PartI]) addEs [usumE, uprodE, PartE]) 1); val TF_induct = result(); @@ -228,19 +225,19 @@ val Fcons_inject = standard (Fcons_Fcons_eq RS iffD1 RS conjE); -(*** TF_rec -- by wf recursion on pred_Sexp ***) +(*** 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); + wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec); (** conversion rules for TF_rec **) goalw Simult.thy [TCONS_def] - "!!M N. [| M: Sexp; N: Sexp |] ==> \ + "!!M N. [| 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 (HOL_ss addsimps [Case_In0, Split]) 1); -by (asm_simp_tac (pred_Sexp_ss addsimps [In0_def]) 1); +by (asm_simp_tac (pred_sexp_ss addsimps [In0_def]) 1); val TF_rec_TCONS = result(); goalw Simult.thy [FNIL_def] "TF_rec(FNIL,b,c,d) = c"; @@ -249,29 +246,29 @@ val TF_rec_FNIL = result(); goalw Simult.thy [FCONS_def] - "!!M N. [| M: Sexp; N: Sexp |] ==> \ + "!!M N. [| 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 (pred_Sexp_ss addsimps [CONS_def,In1_def]) 1); +by (asm_simp_tac (pred_sexp_ss addsimps [CONS_def,In1_def]) 1); val TF_rec_FCONS = result(); (*** 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), +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), +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_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]; + 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] diff -r 872f866e630f -r d9527f97246e ex/Simult.thy --- a/ex/Simult.thy Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/Simult.thy Thu Aug 25 10:47:33 1994 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/ex/simult +(* Title: HOL/ex/Simult ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge @@ -6,8 +6,11 @@ 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 +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 = List + @@ -18,27 +21,38 @@ arities tree,forest :: (term)term consts - TF :: "'a node set set => 'a node set set" - FNIL :: "'a node set" - TCONS,FCONS :: "['a node set, 'a node set] => 'a node set" - Rep_Tree :: "'a tree => 'a node set" - Abs_Tree :: "'a node set => 'a tree" - Rep_Forest :: "'a forest => 'a node set" - Abs_Forest :: "'a node set => 'a forest" + 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 node set, ['a node set , 'a node set, 'b]=>'b, \ -\ 'b, ['a node set , 'a node set, 'b, 'b]=>'b] => 'b" + 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" -rules +defs + (*the concrete constants*) + TCONS_def "TCONS(M,N) == In0(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)))" - (*faking a type definition for tree...*) + +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" @@ -48,18 +62,11 @@ Abs_Forest_inverse "z: Part(TF(range(Leaf)),In1) ==> Rep_Forest(Abs_Forest(z)) = z" - (*the concrete constants*) - TCONS_def "TCONS(M,N) == In0(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)))" +defs (*recursion*) TF_rec_def - "TF_rec(M,b,c,d) == wfrec(trancl(pred_Sexp), M, \ + "TF_rec(M,b,c,d) == wfrec(trancl(pred_sexp), M, \ \ Case(Split(%x y g. b(x,y,g(y))), \ \ List_case(%g.c, %x y g. d(x,y,g(x),g(y)))))" diff -r 872f866e630f -r d9527f97246e ex/Term.ML --- a/ex/Term.ML Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/Term.ML Thu Aug 25 10:47:33 1994 +0200 @@ -1,9 +1,9 @@ -(* Title: HOL/ex/term +(* Title: HOL/ex/Term ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -For term.thy. illustrates List functor +Terms over a given alphabet -- function applications; illustrates list functor (essentially the same type as in Trees & Forests) *) @@ -11,85 +11,83 @@ (*** Monotonicity and unfolding of the function ***) -goal Term.thy "mono(%Z. A <*> List(Z))"; -by (REPEAT (ares_tac [monoI, subset_refl, List_mono, uprod_mono] 1)); -val Term_fun_mono = result(); +goal Term.thy "term(A) = A <*> list(term(A))"; +by (fast_tac (univ_cs addSIs (equalityI :: term.intrs) + addEs [term.elim]) 1); +val term_unfold = result(); -val Term_unfold = Term_fun_mono RS (Term_def RS def_lfp_Tarski); - -(*This justifies using Term in other recursive type definitions*) -goalw Term.thy [Term_def] "!!A B. A<=B ==> Term(A) <= Term(B)"; -by (REPEAT (ares_tac [lfp_mono, subset_refl, List_mono, uprod_mono] 1)); -val Term_mono = result(); +(*This justifies using term in other recursive type definitions*) +goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)"; +by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1)); +val term_mono = result(); -(** Type checking rules -- Term creates well-founded sets **) +(** Type checking -- term creates well-founded sets **) -val prems = goalw Term.thy [Term_def] "Term(Sexp) <= Sexp"; +goalw Term.thy term.defs "term(sexp) <= sexp"; by (rtac lfp_lowerbound 1); -by (fast_tac (univ_cs addIs [Sexp_SconsI, List_Sexp RS subsetD]) 1); -val Term_Sexp = result(); +by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1); +val term_sexp = result(); -(* A <= Sexp ==> Term(A) <= Sexp *) -val Term_subset_Sexp = standard - (Term_mono RS (Term_Sexp RSN (2,subset_trans))); +(* A <= sexp ==> term(A) <= sexp *) +val term_subset_sexp = standard ([term_mono, term_sexp] MRS subset_trans); -(** Elimination -- structural induction on the set Term(A) **) +(** Elimination -- structural induction on the set term(A) **) -(*Induction for the set Term(A) *) +(*Induction for the set term(A) *) val [major,minor] = goal Term.thy - "[| M: Term(A); \ -\ !!x zs. [| x: A; zs: List(Term(A)); zs: List({x.R(x)}) \ + "[| M: term(A); \ +\ !!x zs. [| x: A; zs: list(term(A)); zs: list({x.R(x)}) \ \ |] ==> R(x$zs) \ \ |] ==> R(M)"; -by (rtac (major RS (Term_def RS def_induct)) 1); -by (rtac Term_fun_mono 1); -by (REPEAT (eresolve_tac ([uprodE, ssubst, minor] @ - ([Int_lower1,Int_lower2] RL [List_mono RS subsetD])) 1)); -val Term_induct = result(); +by (rtac (major RS term.induct) 1); +by (REPEAT (eresolve_tac ([minor] @ + ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); +(*Proof could also use mono_Int RS subsetD RS IntE *) +val term_induct = result(); -(*Induction on Term(A) followed by induction on List *) +(*Induction on term(A) followed by induction on list *) val major::prems = goal Term.thy - "[| M: Term(A); \ + "[| M: term(A); \ \ !!x. [| x: A |] ==> R(x$NIL); \ -\ !!x z zs. [| x: A; z: Term(A); zs: List(Term(A)); R(x$zs) \ +\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); R(x$zs) \ \ |] ==> R(x $ CONS(z,zs)) \ \ |] ==> R(M)"; -by (rtac (major RS Term_induct) 1); -by (etac List_induct 1); +by (rtac (major RS term_induct) 1); +by (etac list.induct 1); by (REPEAT (ares_tac prems 1)); -val Term_induct2 = result(); +val term_induct2 = result(); (*** Structural Induction on the abstract type 'a term ***) val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons]; -val Rep_Term_in_Sexp = - Rep_Term RS (range_Leaf_subset_Sexp RS Term_subset_Sexp RS subsetD); +val Rep_term_in_sexp = + Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); (*Induction for the abstract type 'a term*) -val prems = goalw Term.thy [App_def,Rep_TList_def,Abs_TList_def] +val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] "[| !!x ts. list_all(R,ts) ==> R(App(x,ts)) \ \ |] ==> R(t)"; -by (rtac (Rep_Term_inverse RS subst) 1); (*types force good instantiation*) -by (res_inst_tac [("P","Rep_Term(t) : Sexp")] conjunct2 1); -by (rtac (Rep_Term RS Term_induct) 1); -by (REPEAT (ares_tac [conjI, Sexp_SconsI, Term_subset_Sexp RS - List_subset_Sexp,range_Leaf_subset_Sexp] 1 +by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*) +by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1); +by (rtac (Rep_term RS term_induct) 1); +by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS + list_subset_sexp, range_Leaf_subset_sexp] 1 ORELSE etac rev_subsetD 1)); -by (eres_inst_tac [("A1","Term(?u)"), ("f1","Rep_Term"), ("g1","Abs_Term")] +by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")] (Abs_map_inverse RS subst) 1); -by (rtac (range_Leaf_subset_Sexp RS Term_subset_Sexp) 1); -by (etac Abs_Term_inverse 1); +by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1); +by (etac Abs_term_inverse 1); by (etac rangeE 1); by (hyp_subst_tac 1); by (resolve_tac prems 1); -by (etac List_induct 1); +by (etac list.induct 1); by (etac CollectE 2); by (stac Abs_map_CONS 2); by (etac conjunct1 2); by (etac rev_subsetD 2); -by (rtac List_subset_Sexp 2); +by (rtac list_subset_sexp 2); by (fast_tac set_cs 2); by (ALLGOALS (asm_simp_tac list_all_ss)); val term_induct = result(); @@ -111,66 +109,56 @@ rename_last_tac a ["1","s"] (i+1)]; -(** Introduction rule for Term **) -(* c : A <*> List(Term(A)) ==> c : Term(A) *) -val TermI = standard (Term_unfold RS equalityD2 RS subsetD); - -(*The constant APP is not declared; it is simply . *) -val prems = goal Term.thy "[| M: A; N : List(Term(A)) |] ==> M$N : Term(A)"; -by (REPEAT (resolve_tac (prems@[TermI, ListI, uprodI]) 1)); -val APP_I = result(); - - -(*** Term_rec -- by wf recursion on pred_Sexp ***) +(*** Term_rec -- by wf recursion on pred_sexp ***) val Term_rec_unfold = - wf_pred_Sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); + wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); (** conversion rules **) val [prem] = goal Term.thy - "N: List(Term(A)) ==> \ -\ !M. : pred_Sexp^+ --> \ -\ Abs_map(cut(h, pred_Sexp^+, M), N) = \ + "N: list(term(A)) ==> \ +\ !M. : pred_sexp^+ --> \ +\ Abs_map(cut(h, pred_sexp^+, M), N) = \ \ Abs_map(h,N)"; -by (rtac (prem RS List_induct) 1); +by (rtac (prem RS list.induct) 1); by (simp_tac list_all_ss 1); by (strip_tac 1); -by (etac (pred_Sexp_CONS_D RS conjE) 1); -by (asm_simp_tac (list_all_ss addsimps [trancl_pred_SexpD1, cut_apply]) 1); +by (etac (pred_sexp_CONS_D RS conjE) 1); +by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1); val Abs_map_lemma = result(); -val [prem1,prem2,A_subset_Sexp] = goal Term.thy - "[| M: Sexp; N: List(Term(A)); A<=Sexp |] ==> \ +val [prem1,prem2,A_subset_sexp] = goal Term.thy + "[| M: sexp; N: list(term(A)); A<=sexp |] ==> \ \ Term_rec(M$N, d) = d(M, N, Abs_map(%Z. Term_rec(Z,d), N))"; by (rtac (Term_rec_unfold RS trans) 1); by (simp_tac (HOL_ss addsimps [Split, - prem2 RS Abs_map_lemma RS spec RS mp, pred_SexpI2 RS r_into_trancl, - prem1, prem2 RS rev_subsetD, List_subset_Sexp, - Term_subset_Sexp, A_subset_Sexp])1); + prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl, + prem1, prem2 RS rev_subsetD, list_subset_sexp, + term_subset_sexp, A_subset_sexp])1); val Term_rec = result(); (*** term_rec -- by Term_rec ***) local val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy) - [("f","Rep_Term")] Rep_map_type; - val Rep_TList = Rep_Term RS Rep_map_type1; - val Rep_Term_rec = range_Leaf_subset_Sexp RSN (2,Rep_TList RSN(2,Term_rec)); + [("f","Rep_term")] Rep_map_type; + val Rep_Tlist = Rep_term RS Rep_map_type1; + val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec)); - (*Now avoids conditional rewriting with the premise N: List(Term(A)), + (*Now avoids conditional rewriting with the premise N: list(term(A)), since A will be uninstantiated and will cause rewriting to fail. *) val term_rec_ss = HOL_ss - addsimps [Rep_TList RS (rangeI RS APP_I RS Abs_Term_inverse), - Rep_Term_in_Sexp, Rep_Term_rec, Rep_Term_inverse, + addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse), + Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf, Inv_f_f, - Abs_Rep_map, map_ident, Sexp_LeafI] + Abs_Rep_map, map_ident, sexp.LeafI] in val term_rec = prove_goalw Term.thy - [term_rec_def, App_def, Rep_TList_def, Abs_TList_def] + [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def] "term_rec(App(f,ts), d) = d(f, ts, map (%t. term_rec(t,d), ts))" (fn _ => [simp_tac term_rec_ss 1]) diff -r 872f866e630f -r d9527f97246e ex/Term.thy --- a/ex/Term.thy Wed Aug 24 18:49:29 1994 +0200 +++ b/ex/Term.thy Thu Aug 25 10:47:33 1994 +0200 @@ -1,12 +1,12 @@ -(* Title: HOL/ex/term +(* Title: HOL/ex/Term ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge -Terms over a given alphabet -- function applications; illustrates List functor +Terms over a given alphabet -- function applications; illustrates list functor (essentially the same type as in Trees & Forests) -There is no constructor APP because it is simply cons (.) +There is no constructor APP because it is simply cons ($) *) Term = List + @@ -16,33 +16,40 @@ arities term :: (term)term consts - Term :: "'a node set set => 'a node set set" - Rep_Term :: "'a term => 'a node set" - Abs_Term :: "'a node set => 'a term" - Rep_TList :: "'a term list => 'a node set" - Abs_TList :: "'a node set => 'a term list" + term :: "'a item set => 'a item set" + Rep_term :: "'a term => 'a item" + Abs_term :: "'a item => 'a term" + Rep_Tlist :: "'a term list => 'a item" + Abs_Tlist :: "'a item => 'a term list" App :: "['a, ('a term)list] => 'a term" - Term_rec :: - "['a node set, ['a node set , 'a node set, 'b list]=>'b] => 'b" + Term_rec :: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b" term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b" -rules - Term_def "Term(A) == lfp(%Z. A <*> List(Z))" - (*faking a type definition for term...*) - Rep_Term "Rep_Term(n): Term(range(Leaf))" - Rep_Term_inverse "Abs_Term(Rep_Term(t)) = t" - Abs_Term_inverse "M: Term(range(Leaf)) ==> Rep_Term(Abs_Term(M)) = M" - (*defining abstraction/representation functions for term list...*) - Rep_TList_def "Rep_TList == Rep_map(Rep_Term)" - Abs_TList_def "Abs_TList == Abs_map(Abs_Term)" - (*defining the abstract constants*) - App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))" - (*list recursion*) +inductive "term(A)" + intrs + APP_I "[| M: A; N : list(term(A)) |] ==> M$N : term(A)" + monos "[list_mono]" + +defs + (*defining abstraction/representation functions for term list...*) + Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" + Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" + + (*defining the abstract constants*) + App_def "App(a,ts) == Abs_term(Leaf(a) $ Rep_Tlist(ts))" + + (*list recursion*) Term_rec_def - "Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \ + "Term_rec(M,d) == wfrec(trancl(pred_sexp), M, \ \ Split(%x y g. d(x,y, Abs_map(g,y))))" term_rec_def "term_rec(t,d) == \ -\ Term_rec(Rep_Term(t), %x y r. d(Inv(Leaf,x), Abs_TList(y), r))" +\ Term_rec(Rep_term(t), %x y r. d(Inv(Leaf,x), Abs_Tlist(y), r))" + +rules + (*faking a type definition for term...*) + Rep_term "Rep_term(n): term(range(Leaf))" + Rep_term_inverse "Abs_term(Rep_term(t)) = t" + Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M" end