1 (* Title: HOL/Sexp |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 S-expressions, general binary trees for defining recursive data structures |
|
7 *) |
|
8 |
|
9 open Sexp; |
|
10 |
|
11 (** sexp_case **) |
|
12 |
|
13 Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)"; |
|
14 by (Blast_tac 1); |
|
15 qed "sexp_case_Leaf"; |
|
16 |
|
17 Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)"; |
|
18 by (Blast_tac 1); |
|
19 qed "sexp_case_Numb"; |
|
20 |
|
21 Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N"; |
|
22 by (Blast_tac 1); |
|
23 qed "sexp_case_Scons"; |
|
24 |
|
25 Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons]; |
|
26 |
|
27 |
|
28 (** Introduction rules for sexp constructors **) |
|
29 |
|
30 val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp"; |
|
31 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1); |
|
32 qed "sexp_In0I"; |
|
33 |
|
34 val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp"; |
|
35 by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1); |
|
36 qed "sexp_In1I"; |
|
37 |
|
38 AddIs sexp.intrs; |
|
39 |
|
40 Goal "range(Leaf) <= sexp"; |
|
41 by (Blast_tac 1); |
|
42 qed "range_Leaf_subset_sexp"; |
|
43 |
|
44 val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp"; |
|
45 by (rtac (major RS setup_induction) 1); |
|
46 by (etac sexp.induct 1); |
|
47 by (ALLGOALS Blast_tac); |
|
48 qed "Scons_D"; |
|
49 |
|
50 (** Introduction rules for 'pred_sexp' **) |
|
51 |
|
52 Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp"; |
|
53 by (Blast_tac 1); |
|
54 qed "pred_sexp_subset_Sigma"; |
|
55 |
|
56 (* (a,b) : pred_sexp^+ ==> a : sexp *) |
|
57 val trancl_pred_sexpD1 = |
|
58 pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1 |
|
59 and trancl_pred_sexpD2 = |
|
60 pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2; |
|
61 |
|
62 Goalw [pred_sexp_def] |
|
63 "!!M. [| M: sexp; N: sexp |] ==> (M, Scons M N) : pred_sexp"; |
|
64 by (Blast_tac 1); |
|
65 qed "pred_sexpI1"; |
|
66 |
|
67 Goalw [pred_sexp_def] |
|
68 "!!M. [| M: sexp; N: sexp |] ==> (N, Scons M N) : pred_sexp"; |
|
69 by (Blast_tac 1); |
|
70 qed "pred_sexpI2"; |
|
71 |
|
72 (*Combinations involving transitivity and the rules above*) |
|
73 val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl |
|
74 and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl; |
|
75 |
|
76 val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD) |
|
77 and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD); |
|
78 |
|
79 (*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) |
|
80 Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2, |
|
81 pred_sexp_trans1, pred_sexp_trans2, cut_apply]); |
|
82 |
|
83 val major::prems = goalw Sexp.thy [pred_sexp_def] |
|
84 "[| p : pred_sexp; \ |
|
85 \ !!M N. [| p = (M, Scons M N); M: sexp; N: sexp |] ==> R; \ |
|
86 \ !!M N. [| p = (N, Scons M N); M: sexp; N: sexp |] ==> R \ |
|
87 \ |] ==> R"; |
|
88 by (cut_facts_tac [major] 1); |
|
89 by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1)); |
|
90 qed "pred_sexpE"; |
|
91 |
|
92 Goal "wf(pred_sexp)"; |
|
93 by (rtac (pred_sexp_subset_Sigma RS wfI) 1); |
|
94 by (etac sexp.induct 1); |
|
95 by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE]))); |
|
96 qed "wf_pred_sexp"; |
|
97 |
|
98 |
|
99 (*** sexp_rec -- by wf recursion on pred_sexp ***) |
|
100 |
|
101 Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \ |
|
102 \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))"; |
|
103 by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1); |
|
104 |
|
105 (* sexp_rec a c d e = |
|
106 sexp_case c d |
|
107 (%N1 N2. |
|
108 e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1) |
|
109 (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a |
|
110 *) |
|
111 bind_thm("sexp_rec_unfold", |
|
112 [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec); |
|
113 |
|
114 (** conversion rules **) |
|
115 |
|
116 Goal "sexp_rec (Leaf a) c d h = c(a)"; |
|
117 by (stac sexp_rec_unfold 1); |
|
118 by (rtac sexp_case_Leaf 1); |
|
119 qed "sexp_rec_Leaf"; |
|
120 |
|
121 Goal "sexp_rec (Numb k) c d h = d(k)"; |
|
122 by (stac sexp_rec_unfold 1); |
|
123 by (rtac sexp_case_Numb 1); |
|
124 qed "sexp_rec_Numb"; |
|
125 |
|
126 Goal "[| M: sexp; N: sexp |] ==> \ |
|
127 \ sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)"; |
|
128 by (rtac (sexp_rec_unfold RS trans) 1); |
|
129 by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1); |
|
130 qed "sexp_rec_Scons"; |
|