author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44918  6a80fbc4e72c 
child 55017  2df6ad1dbd66 
permissions  rwrr 
8840  1 
(* Title: HOL/Induct/Sexp.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

3 
Copyright 1992 University of Cambridge 

4 

5 
Sexpressions, general binary trees for defining recursive data 

6 
structures by hand. 

7 
*) 

8 

44014
88bd7d74a2c1
moved recursion combinator to HOL/Library/Wfrec.thy  it is so fundamental and wellknown that it should survive recdef
krauss
parents:
44013
diff
changeset

9 
theory Sexp imports Main "~~/src/HOL/Library/Wfrec" begin 
20801  10 

41818  11 
type_synonym 'a item = "'a Datatype.item" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

12 
abbreviation "Leaf == Datatype.Leaf" 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

13 
abbreviation "Numb == Datatype.Numb" 
20801  14 

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

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

18 
LeafI: "Leaf(a) \<in> sexp" 
23746  19 
 NumbI: "Numb(i) \<in> sexp" 
20 
 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

21 

19736  22 
definition 
8840  23 
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

24 
'a item] => 'b" where 
20801  25 
"sexp_case c d e M = (THE z. (EX x. M=Leaf(x) & z=c(x)) 
26 
 (EX k. M=Numb(k) & z=d(k)) 

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

8840  28 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

29 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

30 
pred_sexp :: "('a item * 'a item)set" where 
19736  31 
"pred_sexp = (\<Union>M \<in> sexp. \<Union>N \<in> sexp. {(M, Scons M N), (N, Scons M N)})" 
8840  32 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

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

34 
sexp_rec :: "['a item, 'a=>'b, nat=>'b, 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20820
diff
changeset

35 
['a item, 'a item, 'b, 'b]=>'b] => 'b" where 
19736  36 
"sexp_rec M c d e = wfrec pred_sexp 
8840  37 
(%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

38 

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 
(** sexp_case **) 
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_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

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_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

46 
by (simp add: sexp_case_def, blast) 
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 
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

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

50 

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

54 

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

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

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

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

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

59 

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

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

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

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

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

64 

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

65 
declare sexp.intros [intro,simp] 
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 range_Leaf_subset_sexp: "range(Leaf) <= sexp" 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

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

69 

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

70 
lemma Scons_D: "Scons M N \<in> sexp ==> M \<in> sexp & N \<in> sexp" 
18413  71 
by (induct S == "Scons M N" set: sexp) auto 
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

72 

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

73 
(** Introduction rules for 'pred_sexp' **) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

74 

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

75 
lemma pred_sexp_subset_Sigma: "pred_sexp <= sexp <*> sexp" 
44918  76 
by (simp add: pred_sexp_def) blast 
13079
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

77 

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

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

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

80 
pred_sexp_subset_Sigma 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23746
diff
changeset

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

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

83 
pred_sexp_subset_Sigma 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
23746
diff
changeset

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

85 

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

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

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

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

89 

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

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

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

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

93 

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

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

95 
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

96 
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

97 

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

98 
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

99 
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

100 

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

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

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

103 

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

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

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

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

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

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

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

110 

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

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

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

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

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

115 
done 
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 

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

118 
(*** sexp_rec  by wf recursion on pred_sexp ***) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

119 

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

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

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

122 
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

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

124 

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

125 
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

126 

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

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

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

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

130 
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

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

132 
*) 
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 
(** conversion rules **) 
e7738aa7267f
conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents:
11481
diff
changeset

135 

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

136 
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

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

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

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

140 

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

141 
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

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

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

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

145 

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

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

147 
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

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

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

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

151 

8840  152 
end 