923
|
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 |
val sexp_free_cs =
|
|
14 |
set_cs addSDs [Leaf_inject, Numb_inject, Scons_inject]
|
|
15 |
addSEs [Leaf_neq_Scons, Leaf_neq_Numb,
|
|
16 |
Numb_neq_Scons, Numb_neq_Leaf,
|
|
17 |
Scons_neq_Leaf, Scons_neq_Numb];
|
|
18 |
|
|
19 |
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
|
|
20 |
by (resolve_tac [select_equality] 1);
|
|
21 |
by (ALLGOALS (fast_tac sexp_free_cs));
|
|
22 |
qed "sexp_case_Leaf";
|
|
23 |
|
|
24 |
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
|
|
25 |
by (resolve_tac [select_equality] 1);
|
|
26 |
by (ALLGOALS (fast_tac sexp_free_cs));
|
|
27 |
qed "sexp_case_Numb";
|
|
28 |
|
|
29 |
goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
|
|
30 |
by (resolve_tac [select_equality] 1);
|
|
31 |
by (ALLGOALS (fast_tac sexp_free_cs));
|
|
32 |
qed "sexp_case_Scons";
|
|
33 |
|
|
34 |
|
|
35 |
(** Introduction rules for sexp constructors **)
|
|
36 |
|
|
37 |
val [prem] = goalw Sexp.thy [In0_def]
|
|
38 |
"M: sexp ==> In0(M) : sexp";
|
|
39 |
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
|
|
40 |
qed "sexp_In0I";
|
|
41 |
|
|
42 |
val [prem] = goalw Sexp.thy [In1_def]
|
|
43 |
"M: sexp ==> In1(M) : sexp";
|
|
44 |
by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
|
|
45 |
qed "sexp_In1I";
|
|
46 |
|
|
47 |
val sexp_cs = set_cs addIs sexp.intrs@[SigmaI, uprodI];
|
|
48 |
|
|
49 |
goal Sexp.thy "range(Leaf) <= sexp";
|
|
50 |
by (fast_tac sexp_cs 1);
|
|
51 |
qed "range_Leaf_subset_sexp";
|
|
52 |
|
|
53 |
val [major] = goal Sexp.thy "M$N : sexp ==> M: sexp & N: sexp";
|
|
54 |
by (rtac (major RS setup_induction) 1);
|
|
55 |
by (etac sexp.induct 1);
|
|
56 |
by (ALLGOALS
|
|
57 |
(fast_tac (set_cs addSEs [Scons_neq_Leaf,Scons_neq_Numb,Scons_inject])));
|
|
58 |
qed "Scons_D";
|
|
59 |
|
|
60 |
(** Introduction rules for 'pred_sexp' **)
|
|
61 |
|
|
62 |
goalw Sexp.thy [pred_sexp_def] "pred_sexp <= Sigma sexp (%u.sexp)";
|
|
63 |
by (fast_tac sexp_cs 1);
|
|
64 |
qed "pred_sexp_subset_Sigma";
|
|
65 |
|
|
66 |
(* <a,b> : pred_sexp^+ ==> a : sexp *)
|
|
67 |
val trancl_pred_sexpD1 =
|
|
68 |
pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
|
|
69 |
and trancl_pred_sexpD2 =
|
|
70 |
pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
|
|
71 |
|
|
72 |
val prems = goalw Sexp.thy [pred_sexp_def]
|
|
73 |
"[| M: sexp; N: sexp |] ==> <M, M$N> : pred_sexp";
|
|
74 |
by (fast_tac (set_cs addIs prems) 1);
|
|
75 |
qed "pred_sexpI1";
|
|
76 |
|
|
77 |
val prems = goalw Sexp.thy [pred_sexp_def]
|
|
78 |
"[| M: sexp; N: sexp |] ==> <N, M$N> : pred_sexp";
|
|
79 |
by (fast_tac (set_cs addIs prems) 1);
|
|
80 |
qed "pred_sexpI2";
|
|
81 |
|
|
82 |
(*Combinations involving transitivity and the rules above*)
|
|
83 |
val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
|
|
84 |
and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
|
|
85 |
|
|
86 |
val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
|
|
87 |
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
|
|
88 |
|
|
89 |
(*Proves goals of the form <M,N>:pred_sexp^+ provided M,N:sexp*)
|
|
90 |
val pred_sexp_simps =
|
|
91 |
sexp.intrs @
|
|
92 |
[pred_sexp_t1, pred_sexp_t2,
|
|
93 |
pred_sexp_trans1, pred_sexp_trans2, cut_apply];
|
|
94 |
val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps;
|
|
95 |
|
|
96 |
val major::prems = goalw Sexp.thy [pred_sexp_def]
|
|
97 |
"[| p : pred_sexp; \
|
|
98 |
\ !!M N. [| p = <M, M$N>; M: sexp; N: sexp |] ==> R; \
|
|
99 |
\ !!M N. [| p = <N, M$N>; M: sexp; N: sexp |] ==> R \
|
|
100 |
\ |] ==> R";
|
|
101 |
by (cut_facts_tac [major] 1);
|
|
102 |
by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
|
|
103 |
qed "pred_sexpE";
|
|
104 |
|
|
105 |
goal Sexp.thy "wf(pred_sexp)";
|
|
106 |
by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
|
|
107 |
by (etac sexp.induct 1);
|
|
108 |
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Scons_inject]) 3);
|
|
109 |
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Numb_neq_Scons]) 2);
|
|
110 |
by (fast_tac (HOL_cs addSEs [mp, pred_sexpE, Pair_inject, Leaf_neq_Scons]) 1);
|
|
111 |
qed "wf_pred_sexp";
|
|
112 |
|
|
113 |
(*** sexp_rec -- by wf recursion on pred_sexp ***)
|
|
114 |
|
|
115 |
(** conversion rules **)
|
|
116 |
|
|
117 |
val sexp_rec_unfold = wf_pred_sexp RS (sexp_rec_def RS def_wfrec);
|
|
118 |
|
|
119 |
|
|
120 |
goal Sexp.thy "sexp_rec (Leaf a) c d h = c(a)";
|
|
121 |
by (stac sexp_rec_unfold 1);
|
|
122 |
by (rtac sexp_case_Leaf 1);
|
|
123 |
qed "sexp_rec_Leaf";
|
|
124 |
|
|
125 |
goal Sexp.thy "sexp_rec (Numb k) c d h = d(k)";
|
|
126 |
by (stac sexp_rec_unfold 1);
|
|
127 |
by (rtac sexp_case_Numb 1);
|
|
128 |
qed "sexp_rec_Numb";
|
|
129 |
|
|
130 |
goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \
|
|
131 |
\ sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
|
|
132 |
by (rtac (sexp_rec_unfold RS trans) 1);
|
|
133 |
by (asm_simp_tac(HOL_ss addsimps
|
|
134 |
[sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
|
|
135 |
qed "sexp_rec_Scons";
|