author | wenzelm |
Mon, 12 Jul 2010 21:38:37 +0200 | |
changeset 37781 | 2fbbf0a48cef |
parent 32960 | 69916a850301 |
child 41818 | 6d4c3ee8219d |
permissions | -rw-r--r-- |
8840 | 1 |
(* Title: HOL/Induct/Sexp.thy |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
Copyright 1992 University of Cambridge |
|
4 |
||
5 |
S-expressions, general binary trees for defining recursive data |
|
6 |
structures by hand. |
|
7 |
*) |
|
8 |
||
20801 | 9 |
theory Sexp imports Main begin |
10 |
||
11 |
types |
|
20820
58693343905f
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
wenzelm
parents:
20801
diff
changeset
|
12 |
'a item = "'a Datatype.item" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
13 |
abbreviation "Leaf == Datatype.Leaf" |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
14 |
abbreviation "Numb == Datatype.Numb" |
20801 | 15 |
|
23746 | 16 |
inductive_set |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
17 |
sexp :: "'a item set" |
23746 | 18 |
where |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
19 |
LeafI: "Leaf(a) \<in> sexp" |
23746 | 20 |
| NumbI: "Numb(i) \<in> sexp" |
21 |
| SconsI: "[| M \<in> sexp; N \<in> sexp |] ==> Scons M N \<in> sexp" |
|
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
22 |
|
19736 | 23 |
definition |
8840 | 24 |
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
25 |
'a item] => 'b" where |
20801 | 26 |
"sexp_case c d e M = (THE z. (EX x. M=Leaf(x) & z=c(x)) |
27 |
| (EX k. M=Numb(k) & z=d(k)) |
|
28 |
| (EX N1 N2. M = Scons N1 N2 & z=e N1 N2))" |
|
8840 | 29 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
30 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
31 |
pred_sexp :: "('a item * 'a item)set" where |
19736 | 32 |
"pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})" |
8840 | 33 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
34 |
definition |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
35 |
sexp_rec :: "['a item, 'a=>'b, nat=>'b, |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset
|
36 |
['a item, 'a item, 'b, 'b]=>'b] => 'b" where |
19736 | 37 |
"sexp_rec M c d e = wfrec pred_sexp |
8840 | 38 |
(%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M" |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
39 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
40 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
41 |
(** sexp_case **) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
42 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
43 |
lemma sexp_case_Leaf [simp]: "sexp_case c d e (Leaf a) = c(a)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
44 |
by (simp add: sexp_case_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
45 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
46 |
lemma sexp_case_Numb [simp]: "sexp_case c d e (Numb k) = d(k)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
47 |
by (simp add: sexp_case_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
48 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
49 |
lemma sexp_case_Scons [simp]: "sexp_case c d e (Scons M N) = e M N" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
50 |
by (simp add: sexp_case_def) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
51 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
52 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
53 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
54 |
(** Introduction rules for sexp constructors **) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
55 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
56 |
lemma sexp_In0I: "M \<in> sexp ==> In0(M) \<in> sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
57 |
apply (simp add: In0_def) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
58 |
apply (erule sexp.NumbI [THEN sexp.SconsI]) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
59 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
60 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
61 |
lemma sexp_In1I: "M \<in> sexp ==> In1(M) \<in> sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
62 |
apply (simp add: In1_def) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
63 |
apply (erule sexp.NumbI [THEN sexp.SconsI]) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
64 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
65 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
66 |
declare sexp.intros [intro,simp] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
67 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
68 |
lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
69 |
by blast |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
70 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
71 |
lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp" |
18413 | 72 |
by (induct S == "Scons M N" set: sexp) auto |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
73 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
74 |
(** Introduction rules for 'pred_sexp' **) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
75 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
76 |
lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
77 |
by (simp add: pred_sexp_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
78 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
79 |
(* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
80 |
lemmas trancl_pred_sexpD1 = |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
81 |
pred_sexp_subset_Sigma |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
82 |
[THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1] |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
83 |
and trancl_pred_sexpD2 = |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
84 |
pred_sexp_subset_Sigma |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
85 |
[THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2] |
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
86 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
87 |
lemma pred_sexpI1: |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
88 |
"[| M \<in> sexp; N \<in> sexp |] ==> (M, Scons M N) \<in> pred_sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
89 |
by (simp add: pred_sexp_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
90 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
91 |
lemma pred_sexpI2: |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
92 |
"[| M \<in> sexp; N \<in> sexp |] ==> (N, Scons M N) \<in> pred_sexp" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
93 |
by (simp add: pred_sexp_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
94 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
95 |
(*Combinations involving transitivity and the rules above*) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
96 |
lemmas pred_sexp_t1 [simp] = pred_sexpI1 [THEN r_into_trancl] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
97 |
and pred_sexp_t2 [simp] = pred_sexpI2 [THEN r_into_trancl] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
98 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
99 |
lemmas pred_sexp_trans1 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t1] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
100 |
and pred_sexp_trans2 [simp] = trans_trancl [THEN transD, OF _ pred_sexp_t2] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
101 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
102 |
(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
103 |
declare cut_apply [simp] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
104 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
105 |
lemma pred_sexpE: |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
106 |
"[| p \<in> pred_sexp; |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
107 |
!!M N. [| p = (M, Scons M N); M \<in> sexp; N \<in> sexp |] ==> R; |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
108 |
!!M N. [| p = (N, Scons M N); M \<in> sexp; N \<in> sexp |] ==> R |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
109 |
|] ==> R" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
110 |
by (simp add: pred_sexp_def, blast) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
111 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
112 |
lemma wf_pred_sexp: "wf(pred_sexp)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
113 |
apply (rule pred_sexp_subset_Sigma [THEN wfI]) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
114 |
apply (erule sexp.induct) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
115 |
apply (blast elim!: pred_sexpE)+ |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
116 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
117 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
118 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
119 |
(*** sexp_rec -- by wf recursion on pred_sexp ***) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
120 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
121 |
lemma sexp_rec_unfold_lemma: |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
122 |
"(%M. sexp_rec M c d e) == |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
123 |
wfrec pred_sexp (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
124 |
by (simp add: sexp_rec_def) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
125 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
126 |
lemmas sexp_rec_unfold = def_wfrec [OF sexp_rec_unfold_lemma wf_pred_sexp] |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
127 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
128 |
(* sexp_rec a c d e = |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
129 |
sexp_case c d |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
130 |
(%N1 N2. |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
131 |
e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
132 |
(cut (%M. sexp_rec M c d e) pred_sexp a N2)) a |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
133 |
*) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
134 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
135 |
(** conversion rules **) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
136 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
137 |
lemma sexp_rec_Leaf: "sexp_rec (Leaf a) c d h = c(a)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
138 |
apply (subst sexp_rec_unfold) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
139 |
apply (rule sexp_case_Leaf) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
140 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
141 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
142 |
lemma sexp_rec_Numb: "sexp_rec (Numb k) c d h = d(k)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
143 |
apply (subst sexp_rec_unfold) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
144 |
apply (rule sexp_case_Numb) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
145 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
146 |
|
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
147 |
lemma sexp_rec_Scons: "[| M \<in> sexp; N \<in> sexp |] ==> |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
148 |
sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)" |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
149 |
apply (rule sexp_rec_unfold [THEN trans]) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
150 |
apply (simp add: pred_sexpI1 pred_sexpI2) |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
151 |
done |
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset
|
152 |
|
8840 | 153 |
end |