src/HOL/Sexp.ML
 author paulson Sat Nov 01 12:59:06 1997 +0100 (1997-11-01) changeset 4059 59c1422c9da5 parent 3029 db0e9b30dc92 child 4089 96fba19bcbe2 permissions -rw-r--r--
New Blast_tac (and minor tidying...)
1 (*  Title:      HOL/Sexp
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Copyright   1994  University of Cambridge
6 S-expressions, general binary trees for defining recursive data structures
7 *)
9 open Sexp;
11 (** sexp_case **)
13 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
14 by (blast_tac (!claset addSIs [select_equality]) 1);
15 qed "sexp_case_Leaf";
17 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
18 by (blast_tac (!claset addSIs [select_equality]) 1);
19 qed "sexp_case_Numb";
21 goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M\$N) = e M N";
22 by (blast_tac (!claset addSIs [select_equality]) 1);
23 qed "sexp_case_Scons";
26 (** Introduction rules for sexp constructors **)
28 val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
29 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
30 qed "sexp_In0I";
32 val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
33 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
34 qed "sexp_In1I";
38 goal Sexp.thy "range(Leaf) <= sexp";
39 by (Blast_tac 1);
40 qed "range_Leaf_subset_sexp";
42 val [major] = goal Sexp.thy "M\$N : sexp ==> M: sexp & N: sexp";
43 by (rtac (major RS setup_induction) 1);
44 by (etac sexp.induct 1);
45 by (ALLGOALS Blast_tac);
46 qed "Scons_D";
48 (** Introduction rules for 'pred_sexp' **)
50 goalw Sexp.thy [pred_sexp_def] "pred_sexp <= sexp Times sexp";
51 by (Blast_tac 1);
52 qed "pred_sexp_subset_Sigma";
54 (* (a,b) : pred_sexp^+ ==> a : sexp *)
55 val trancl_pred_sexpD1 =
56     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
57 and trancl_pred_sexpD2 =
58     pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
60 goalw Sexp.thy [pred_sexp_def]
61     "!!M. [| M: sexp;  N: sexp |] ==> (M, M\$N) : pred_sexp";
62 by (Blast_tac 1);
63 qed "pred_sexpI1";
65 goalw Sexp.thy [pred_sexp_def]
66     "!!M. [| M: sexp;  N: sexp |] ==> (N, M\$N) : pred_sexp";
67 by (Blast_tac 1);
68 qed "pred_sexpI2";
70 (*Combinations involving transitivity and the rules above*)
71 val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
72 and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
74 val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
75 and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
77 (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
78 Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
79                         pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
81 val major::prems = goalw Sexp.thy [pred_sexp_def]
82     "[| p : pred_sexp;                                       \
83 \       !!M N. [| p = (M, M\$N);  M: sexp;  N: sexp |] ==> R; \
84 \       !!M N. [| p = (N, M\$N);  M: sexp;  N: sexp |] ==> R  \
85 \    |] ==> R";
86 by (cut_facts_tac [major] 1);
87 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
88 qed "pred_sexpE";
90 goal Sexp.thy "wf(pred_sexp)";
91 by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
92 by (etac sexp.induct 1);
93 by (ALLGOALS (blast_tac (!claset addSEs [allE, pred_sexpE])));
94 qed "wf_pred_sexp";
97 (*** sexp_rec -- by wf recursion on pred_sexp ***)
99 goal Sexp.thy
100    "(%M. sexp_rec M c d e) = wfrec pred_sexp \
101                        \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
102 by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
103 bind_thm("sexp_rec_unfold",
104 	 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
106 (** conversion rules **)
108 goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
109 by (stac sexp_rec_unfold 1);
110 by (rtac sexp_case_Leaf 1);
111 qed "sexp_rec_Leaf";
113 goal Sexp.thy "sexp_rec (Numb k) c d h = d(k)";
114 by (stac sexp_rec_unfold 1);
115 by (rtac sexp_case_Numb 1);
116 qed "sexp_rec_Numb";
118 goal Sexp.thy "!!M. [| M: sexp;  N: sexp |] ==> \
119 \    sexp_rec (M\$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
120 by (rtac (sexp_rec_unfold RS trans) 1);
121 by (asm_simp_tac (!simpset addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
122     1);
123 qed "sexp_rec_Scons";