author  wenzelm 
Thu, 13 Apr 2006 12:00:50 +0200  
changeset 19414  a21431e996bf 
parent 15674  4a1d07bb53e2 
child 22591  7d1015d59f24 
permissions  rwrr 
10769  1 
(* Title: TFL/dcterm.ML 
2 
ID: $Id$ 

3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 
*) 

6 

7 
(* 

8 
* Derived efficient cterm destructors. 

9 
**) 

10 

11 
signature DCTERM = 

12 
sig 

13 
val dest_comb: cterm > cterm * cterm 

14 
val dest_abs: string option > cterm > cterm * cterm 

15 
val capply: cterm > cterm > cterm 

16 
val cabs: cterm > cterm > cterm 

17 
val mk_conj: cterm * cterm > cterm 

18 
val mk_disj: cterm * cterm > cterm 

19 
val mk_exists: cterm * cterm > cterm 

20 
val dest_conj: cterm > cterm * cterm 

21 
val dest_const: cterm > {Name: string, Ty: typ} 

22 
val dest_disj: cterm > cterm * cterm 

23 
val dest_eq: cterm > cterm * cterm 

24 
val dest_exists: cterm > cterm * cterm 

25 
val dest_forall: cterm > cterm * cterm 

26 
val dest_imp: cterm > cterm * cterm 

27 
val dest_let: cterm > cterm * cterm 

28 
val dest_neg: cterm > cterm 

29 
val dest_pair: cterm > cterm * cterm 

30 
val dest_var: cterm > {Name:string, Ty:typ} 

31 
val is_conj: cterm > bool 

32 
val is_cons: cterm > bool 

33 
val is_disj: cterm > bool 

34 
val is_eq: cterm > bool 

35 
val is_exists: cterm > bool 

36 
val is_forall: cterm > bool 

37 
val is_imp: cterm > bool 

38 
val is_let: cterm > bool 

39 
val is_neg: cterm > bool 

40 
val is_pair: cterm > bool 

41 
val list_mk_disj: cterm list > cterm 

42 
val strip_abs: cterm > cterm list * cterm 

43 
val strip_comb: cterm > cterm * cterm list 

44 
val strip_disj: cterm > cterm list 

45 
val strip_exists: cterm > cterm list * cterm 

46 
val strip_forall: cterm > cterm list * cterm 

47 
val strip_imp: cterm > cterm list * cterm 

48 
val drop_prop: cterm > cterm 

49 
val mk_prop: cterm > cterm 

50 
end; 

51 

52 
structure Dcterm: DCTERM = 

53 
struct 

54 

55 
structure U = Utils; 

56 

57 
fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg}; 

58 

59 

60 
fun dest_comb t = Thm.dest_comb t 

61 
handle CTERM msg => raise ERR "dest_comb" msg; 

62 

63 
fun dest_abs a t = Thm.dest_abs a t 

64 
handle CTERM msg => raise ERR "dest_abs" msg; 

65 

66 
fun capply t u = Thm.capply t u 

67 
handle CTERM msg => raise ERR "capply" msg; 

68 

69 
fun cabs a t = Thm.cabs a t 

70 
handle CTERM msg => raise ERR "cabs" msg; 

71 

72 

73 
(* 

15674
4a1d07bb53e2
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset

74 
* Some simple constructor functions. 
10769  75 
**) 
76 

77 
val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const; 

78 

79 
fun mk_exists (r as (Bvar, Body)) = 

80 
let val ty = #T(rep_cterm Bvar) 

81 
val c = mk_hol_const("Ex", (ty > HOLogic.boolT) > HOLogic.boolT) 

82 
in capply c (uncurry cabs r) end; 

83 

84 

85 
local val c = mk_hol_const("op &", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

86 
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 

87 
end; 

88 

89 
local val c = mk_hol_const("op ", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

90 
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 

91 
end; 

92 

93 

94 
(* 

95 
* The primitives. 

96 
**) 

97 
fun dest_const ctm = 

98 
(case #t(rep_cterm ctm) 

99 
of Const(s,ty) => {Name = s, Ty = ty} 

100 
 _ => raise ERR "dest_const" "not a constant"); 

101 

102 
fun dest_var ctm = 

103 
(case #t(rep_cterm ctm) 

104 
of Var((s,i),ty) => {Name=s, Ty=ty} 

105 
 Free(s,ty) => {Name=s, Ty=ty} 

106 
 _ => raise ERR "dest_var" "not a variable"); 

107 

108 

109 
(* 

110 
* Derived destructor operations. 

111 
**) 

112 

113 
fun dest_monop expected tm = 

114 
let 

115 
fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected); 

116 
val (c, N) = dest_comb tm handle U.ERR _ => err (); 

117 
val name = #Name (dest_const c handle U.ERR _ => err ()); 

118 
in if name = expected then N else err () end; 

119 

120 
fun dest_binop expected tm = 

121 
let 

122 
fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected); 

123 
val (M, N) = dest_comb tm handle U.ERR _ => err () 

124 
in (dest_monop expected M, N) handle U.ERR _ => err () end; 

125 

126 
fun dest_binder expected tm = 

15531  127 
dest_abs NONE (dest_monop expected tm) 
10769  128 
handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected); 
129 

130 

131 
val dest_neg = dest_monop "not" 

132 
val dest_pair = dest_binop "Pair"; 

133 
val dest_eq = dest_binop "op =" 

134 
val dest_imp = dest_binop "op >" 

135 
val dest_conj = dest_binop "op &" 

136 
val dest_disj = dest_binop "op " 

137 
val dest_cons = dest_binop "Cons" 

138 
val dest_let = Library.swap o dest_binop "Let"; 

13182  139 
val dest_select = dest_binder "Hilbert_Choice.Eps" 
10769  140 
val dest_exists = dest_binder "Ex" 
141 
val dest_forall = dest_binder "All" 

142 

143 
(* Query routines *) 

144 

145 
val is_eq = can dest_eq 

146 
val is_imp = can dest_imp 

147 
val is_select = can dest_select 

148 
val is_forall = can dest_forall 

149 
val is_exists = can dest_exists 

150 
val is_neg = can dest_neg 

151 
val is_conj = can dest_conj 

152 
val is_disj = can dest_disj 

153 
val is_pair = can dest_pair 

154 
val is_let = can dest_let 

155 
val is_cons = can dest_cons 

156 

157 

158 
(* 

159 
* Iterated creation. 

160 
**) 

161 
val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm)); 

162 

163 
(* 

164 
* Iterated destruction. (To the "right" in a term.) 

165 
**) 

166 
fun strip break tm = 

167 
let fun dest (p as (ctm,accum)) = 

168 
let val (M,N) = break ctm 

169 
in dest (N, M::accum) 

170 
end handle U.ERR _ => p 

171 
in dest (tm,[]) 

172 
end; 

173 

174 
fun rev2swap (x,l) = (rev l, x); 

175 

176 
val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *) 

177 
val strip_imp = rev2swap o strip dest_imp 

15531  178 
val strip_abs = rev2swap o strip (dest_abs NONE) 
10769  179 
val strip_forall = rev2swap o strip dest_forall 
180 
val strip_exists = rev2swap o strip dest_exists 

181 

182 
val strip_disj = rev o (op::) o strip dest_disj 

183 

184 

185 
(* 

186 
* Going into and out of prop 

187 
**) 

188 

189 
fun mk_prop ctm = 

190 
let val {t, sign, ...} = Thm.rep_cterm ctm in 

191 
if can HOLogic.dest_Trueprop t then ctm 

192 
else Thm.cterm_of sign (HOLogic.mk_Trueprop t) 

193 
end 

194 
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg 

195 
 TERM (msg, _) => raise ERR "mk_prop" msg; 

196 

197 
fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm; 

198 

199 

200 
end; 