--- 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();
-(* <a,b> : 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;
+(* <a,b> : 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 |] ==> <M, M$N> : pred_Sexp";
+val prems = goalw Sexp.thy [pred_sexp_def]
+ "[| M: sexp; N: sexp |] ==> <M, M$N> : 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 |] ==> <N, M$N> : pred_Sexp";
+val prems = goalw Sexp.thy [pred_sexp_def]
+ "[| M: sexp; N: sexp |] ==> <N, M$N> : 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 <M,N>: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 <M,N>: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, M$N>; M: Sexp; N: Sexp |] ==> R; \
-\ !!M N. [| p = <N, M$N>; M: Sexp; N: Sexp |] ==> R \
+val major::prems = goalw Sexp.thy [pred_sexp_def]
+ "[| p : pred_sexp; \
+\ !!M N. [| p = <M, M$N>; M: sexp; N: sexp |] ==> R; \
+\ !!M N. [| p = <N, M$N>; 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();