author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 13079  e7738aa7267f 
child 18413  50c0c118e96d 
permissions  rwrr 
8840  1 
(* Title: HOL/Induct/Sexp.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Sexpressions, general binary trees for defining recursive data 

7 
structures by hand. 

8 
*) 

9 

16417  10 
theory Sexp imports Datatype_Universe Inductive begin 
8840  11 
consts 
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

12 
sexp :: "'a item set" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

13 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

14 
inductive sexp 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

15 
intros 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

16 
LeafI: "Leaf(a) \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

17 
NumbI: "Numb(i) \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

18 
SconsI: "[ M \<in> sexp; N \<in> sexp ] ==> Scons M N \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

19 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

20 
constdefs 
8840  21 

22 
sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 

23 
'a item] => 'b" 

11481  24 
"sexp_case c d e M == THE z. (EX x. M=Leaf(x) & z=c(x)) 
25 
 (EX k. M=Numb(k) & z=d(k)) 

26 
 (EX N1 N2. M = Scons N1 N2 & z=e N1 N2)" 

8840  27 

13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

28 
pred_sexp :: "('a item * 'a item)set" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

29 
"pred_sexp == \<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)}" 
8840  30 

13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

31 
sexp_rec :: "['a item, 'a=>'b, nat=>'b, 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

32 
['a item, 'a item, 'b, 'b]=>'b] => 'b" 
8840  33 
"sexp_rec M c d e == wfrec pred_sexp 
34 
(%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

35 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

36 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

37 
(** sexp_case **) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

38 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

39 
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

40 
by (simp add: sexp_case_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

41 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

42 
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

43 
by (simp add: sexp_case_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

44 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

45 
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

46 
by (simp add: sexp_case_def) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

47 

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 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

50 
(** Introduction rules for sexp constructors **) 
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 
lemma sexp_In0I: "M \<in> sexp ==> In0(M) \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

53 
apply (simp add: In0_def) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

54 
apply (erule sexp.NumbI [THEN sexp.SconsI]) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

55 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

56 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

57 
lemma sexp_In1I: "M \<in> sexp ==> In1(M) \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

58 
apply (simp add: In1_def) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

59 
apply (erule sexp.NumbI [THEN sexp.SconsI]) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

60 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

61 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

62 
declare sexp.intros [intro,simp] 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

63 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

64 
lemma range_Leaf_subset_sexp: "range(Leaf) <= sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

65 
by blast 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

66 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

67 
lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

68 
apply (erule setup_induction) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

69 
apply (erule sexp.induct, blast+) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

70 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

71 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

72 
(** Introduction rules for 'pred_sexp' **) 
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 
lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

75 
by (simp add: pred_sexp_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

76 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

77 
(* (a,b) \<in> pred_sexp^+ ==> a \<in> sexp *) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

78 
lemmas trancl_pred_sexpD1 = 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

79 
pred_sexp_subset_Sigma 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

80 
[THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD1] 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

81 
and trancl_pred_sexpD2 = 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

82 
pred_sexp_subset_Sigma 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

83 
[THEN trancl_subset_Sigma, THEN subsetD, THEN SigmaD2] 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

84 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

85 
lemma pred_sexpI1: 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

86 
"[ 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

87 
by (simp add: pred_sexp_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

88 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

89 
lemma pred_sexpI2: 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

90 
"[ 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

91 
by (simp add: pred_sexp_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

92 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

93 
(*Combinations involving transitivity and the rules above*) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

94 
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

95 
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

96 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

97 
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

98 
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

99 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

100 
(*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

101 
declare cut_apply [simp] 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

102 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

103 
lemma pred_sexpE: 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

104 
"[ p \<in> pred_sexp; 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

105 
!!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

106 
!!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

107 
] ==> R" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

108 
by (simp add: pred_sexp_def, blast) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

109 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

110 
lemma wf_pred_sexp: "wf(pred_sexp)" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

111 
apply (rule pred_sexp_subset_Sigma [THEN wfI]) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

112 
apply (erule sexp.induct) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

113 
apply (blast elim!: pred_sexpE)+ 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

114 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

115 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

116 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

117 
(*** sexp_rec  by wf recursion on pred_sexp ***) 
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 
lemma sexp_rec_unfold_lemma: 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

120 
"(%M. sexp_rec M c d e) == 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

121 
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

122 
by (simp add: sexp_rec_def) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

123 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

124 
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

125 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

126 
(* sexp_rec a c d e = 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

127 
sexp_case c d 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

128 
(%N1 N2. 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

129 
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

130 
(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

131 
*) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

132 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

133 
(** conversion rules **) 
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 
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

136 
apply (subst sexp_rec_unfold) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

137 
apply (rule sexp_case_Leaf) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

138 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

139 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

140 
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

141 
apply (subst sexp_rec_unfold) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

142 
apply (rule sexp_case_Numb) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

143 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

144 

e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

145 
lemma sexp_rec_Scons: "[ M \<in> sexp; N \<in> sexp ] ==> 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

146 
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

147 
apply (rule sexp_rec_unfold [THEN trans]) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

148 
apply (simp add: pred_sexpI1 pred_sexpI2) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

149 
done 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

150 

8840  151 
end 