diff -r d9527f97246e -r 89669c58e506 Sexp.ML --- a/Sexp.ML Thu Aug 25 10:47:33 1994 +0200 +++ b/Sexp.ML Thu Aug 25 11:01:45 1994 +0200 @@ -1,166 +1,135 @@ -(* Title: HOL/sexp +(* Title: HOL/Sexp ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -For sexp.thy. S-expressions. +S-expressions, general binary trees for defining recursive data structures *) open Sexp; -(** the sexp functional **) - -goal Sexp.thy "mono(%Z. range(Leaf) Un range(Numb) Un Z<*>Z)"; -by (REPEAT (ares_tac [monoI, subset_refl, Un_mono, uprod_mono] 1)); -val Sexp_fun_mono = result(); - -val Sexp_unfold = Sexp_fun_mono RS (Sexp_def RS def_lfp_Tarski); +(** sexp_case **) -(** Induction **) - -val major::prems = goal Sexp.thy - "[| ii: Sexp; !!a. P(Leaf(a)); !!k. P(Numb(k)); \ -\ !!i j. [| i: Sexp; j: Sexp; P(i); P(j) |] ==> P(i$j) \ -\ |] ==> P(ii)"; -by (rtac (major RS (Sexp_def RS def_induct)) 1); -by (rtac Sexp_fun_mono 1); -by (fast_tac (set_cs addIs prems addSEs [uprodE]) 1); -val Sexp_induct = result(); +val sexp_free_cs = + set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject] + addSEs [Leaf_neq_Scons, Leaf_neq_Numb, + Numb_neq_Scons, Numb_neq_Leaf, + Scons_neq_Leaf, Scons_neq_Numb]; -(** Sexp_case **) - -goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Leaf(a)) = c(a)"; -by (fast_tac (HOL_cs addIs [select_equality] - addSDs [Leaf_inject] - addSEs [Leaf_neq_Scons, Leaf_neq_Numb]) 1); -val Sexp_case_Leaf = result(); +goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Leaf(a)) = c(a)"; +by (resolve_tac [select_equality] 1); +by (ALLGOALS (fast_tac sexp_free_cs)); +val sexp_case_Leaf = result(); -goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, Numb(k)) = d(k)"; -by (fast_tac (HOL_cs addIs [select_equality] - addSDs [Numb_inject] - addSEs [Numb_neq_Scons, Numb_neq_Leaf]) 1); -val Sexp_case_Numb = result(); +goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, Numb(k)) = d(k)"; +by (resolve_tac [select_equality] 1); +by (ALLGOALS (fast_tac sexp_free_cs)); +val sexp_case_Numb = result(); -goalw Sexp.thy [Sexp_case_def] "Sexp_case(c, d, e, M$N) = e(M,N)"; -by (fast_tac (HOL_cs addIs [select_equality] - addSDs [Scons_inject] - addSEs [Scons_neq_Leaf, Scons_neq_Numb]) 1); -val Sexp_case_Scons = result(); +goalw Sexp.thy [sexp_case_def] "sexp_case(c, d, e, M$N) = e(M,N)"; +by (resolve_tac [select_equality] 1); +by (ALLGOALS (fast_tac sexp_free_cs)); +val sexp_case_Scons = result(); -(** Introduction rules for Sexp constructors **) - -val SexpI = Sexp_unfold RS equalityD2 RS subsetD; - -goal Sexp.thy "Leaf(a): Sexp"; -by (fast_tac (set_cs addIs [SexpI]) 1); -val Sexp_LeafI = result(); - -goal Sexp.thy "Numb(a): Sexp"; -by (fast_tac (set_cs addIs [SexpI]) 1); -val Sexp_NumbI = result(); - -val prems = goal Sexp.thy - "[| M: Sexp; N: Sexp |] ==> M$N : Sexp"; -by (fast_tac (set_cs addIs ([uprodI,SexpI]@prems)) 1); -val Sexp_SconsI = result(); +(** Introduction rules for sexp constructors **) val [prem] = goalw Sexp.thy [In0_def] - "M: Sexp ==> In0(M) : Sexp"; -by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1); -val Sexp_In0I = result(); + "M: sexp ==> In0(M) : sexp"; +by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1); +val sexp_In0I = result(); val [prem] = goalw Sexp.thy [In1_def] - "M: Sexp ==> In1(M) : Sexp"; -by (rtac (prem RS (Sexp_NumbI RS Sexp_SconsI)) 1); -val Sexp_In1I = result(); + "M: sexp ==> In1(M) : sexp"; +by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1); +val sexp_In1I = result(); + +val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI]; -goal Sexp.thy "range(Leaf) <= Sexp"; -by (fast_tac (set_cs addIs [SexpI]) 1); -val range_Leaf_subset_Sexp = result(); +goal Sexp.thy "range(Leaf) <= sexp"; +by (fast_tac sexp_cs 1); +val range_Leaf_subset_sexp = result(); -val [major] = goal Sexp.thy "M$N : Sexp ==> M: Sexp & N: Sexp"; +val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp"; by (rtac (major RS setup_induction) 1); -by (etac Sexp_induct 1); +by (etac sexp.induct 1); by (ALLGOALS (fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject]))); val Scons_D = result(); -(** Introduction rules for 'pred_Sexp' **) - -val sexp_cs = set_cs addIs [SigmaI, uprodI, SexpI]; +(** Introduction rules for 'pred_sexp' **) -goalw Sexp.thy [pred_Sexp_def] "pred_Sexp <= Sigma(Sexp, %u.Sexp)"; +goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma(sexp, %u.sexp)"; by (fast_tac sexp_cs 1); -val pred_Sexp_subset_Sigma = result(); +val pred_sexp_subset_Sigma = result(); -(* : pred_Sexp^+ ==> a : Sexp *) -val trancl_pred_SexpD1 = - pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1 -and trancl_pred_SexpD2 = - pred_Sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2; +(* : pred_sexp^+ ==> a : sexp *) +val trancl_pred_sexpD1 = + pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1 +and trancl_pred_sexpD2 = + pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2; -val prems = goalw Sexp.thy [pred_Sexp_def] - "[| M: Sexp; N: Sexp |] ==> : pred_Sexp"; +val prems = goalw Sexp.thy [pred_sexp_def] + "[| M: sexp; N: sexp |] ==> : pred_sexp"; by (fast_tac (set_cs addIs prems) 1); -val pred_SexpI1 = result(); +val pred_sexpI1 = result(); -val prems = goalw Sexp.thy [pred_Sexp_def] - "[| M: Sexp; N: Sexp |] ==> : pred_Sexp"; +val prems = goalw Sexp.thy [pred_sexp_def] + "[| M: sexp; N: sexp |] ==> : pred_sexp"; by (fast_tac (set_cs addIs prems) 1); -val pred_SexpI2 = result(); +val pred_sexpI2 = result(); (*Combinations involving transitivity and the rules above*) -val pred_Sexp_t1 = pred_SexpI1 RS r_into_trancl -and pred_Sexp_t2 = pred_SexpI2 RS r_into_trancl; +val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl +and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl; -val pred_Sexp_trans1 = pred_Sexp_t1 RSN (2, trans_trancl RS transD) -and pred_Sexp_trans2 = pred_Sexp_t2 RSN (2, trans_trancl RS transD); +val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD) +and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD); -(*Proves goals of the form :pred_Sexp^+ provided M,N:Sexp*) -val pred_Sexp_simps = - [Sexp_LeafI, Sexp_NumbI, Sexp_SconsI, - pred_Sexp_t1, pred_Sexp_t2, - pred_Sexp_trans1, pred_Sexp_trans2, cut_apply]; -val pred_Sexp_ss = HOL_ss addsimps pred_Sexp_simps; +(*Proves goals of the form :pred_sexp^+ provided M,N:sexp*) +val pred_sexp_simps = + sexp.intrs @ + [pred_sexp_t1, pred_sexp_t2, + pred_sexp_trans1, pred_sexp_trans2, cut_apply]; +val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps; -val major::prems = goalw Sexp.thy [pred_Sexp_def] - "[| p : pred_Sexp; \ -\ !!M N. [| p = ; M: Sexp; N: Sexp |] ==> R; \ -\ !!M N. [| p = ; M: Sexp; N: Sexp |] ==> R \ +val major::prems = goalw Sexp.thy [pred_sexp_def] + "[| p : pred_sexp; \ +\ !!M N. [| p = ; M: sexp; N: sexp |] ==> R; \ +\ !!M N. [| p = ; M: sexp; N: sexp |] ==> R \ \ |] ==> R"; by (cut_facts_tac [major] 1); by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1)); -val pred_SexpE = result(); +val pred_sexpE = result(); -goal Sexp.thy "wf(pred_Sexp)"; -by (rtac (pred_Sexp_subset_Sigma RS wfI) 1); -by (etac Sexp_induct 1); -by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Scons_inject]) 3); -by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Numb_neq_Scons]) 2); -by (fast_tac (HOL_cs addSEs [mp, pred_SexpE, Pair_inject, Leaf_neq_Scons]) 1); -val wf_pred_Sexp = result(); +goal Sexp.thy "wf(pred_sexp)"; +by (rtac (pred_sexp_subset_Sigma RS wfI) 1); +by (etac sexp.induct 1); +by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3); +by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2); +by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1); +val wf_pred_sexp = result(); -(*** Sexp_rec -- by wf recursion on pred_Sexp ***) +(*** sexp_rec -- by wf recursion on pred_sexp ***) (** conversion rules **) -val Sexp_rec_unfold = wf_pred_Sexp RS (Sexp_rec_def RS def_wfrec); +val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec); -goal Sexp.thy "Sexp_rec(Leaf(a), c, d, h) = c(a)"; -by (stac Sexp_rec_unfold 1); -by (rtac Sexp_case_Leaf 1); -val Sexp_rec_Leaf = result(); +goal Sexp.thy "sexp_rec(Leaf(a), c, d, h) = c(a)"; +by (stac sexp_rec_unfold 1); +by (rtac sexp_case_Leaf 1); +val sexp_rec_Leaf = result(); -goal Sexp.thy "Sexp_rec(Numb(k), c, d, h) = d(k)"; -by (stac Sexp_rec_unfold 1); -by (rtac Sexp_case_Numb 1); -val Sexp_rec_Numb = result(); +goal Sexp.thy "sexp_rec(Numb(k), c, d, h) = d(k)"; +by (stac sexp_rec_unfold 1); +by (rtac sexp_case_Numb 1); +val sexp_rec_Numb = result(); -goal Sexp.thy "!!M. [| M: Sexp; N: Sexp |] ==> \ -\ Sexp_rec(M$N, c, d, h) = h(M, N, Sexp_rec(M,c,d,h), Sexp_rec(N,c,d,h))"; -by (rtac (Sexp_rec_unfold RS trans) 1); +goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \ +\ sexp_rec(M$N, c, d, h) = h(M, N, sexp_rec(M,c,d,h), sexp_rec(N,c,d,h))"; +by (rtac (sexp_rec_unfold RS trans) 1); by (asm_simp_tac(HOL_ss addsimps - [Sexp_case_Scons,pred_SexpI1,pred_SexpI2,cut_apply])1); -val Sexp_rec_Scons = result(); + [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1); +val sexp_rec_Scons = result();