author  lcp 
Fri, 12 Aug 1994 12:51:34 +0200  
changeset 516  1957113f0d7d 
parent 466  08d1cce222e1 
child 543  e961b2092869 
permissions  rwrr 
0  1 
(* Title: ZF/indsyntax.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Abstract Syntax functions for Inductive Definitions 

7 
*) 

8 

516  9 
(*The structure protects these items from redeclaration (somewhat!). The 
10 
datatype definitions in theory files refer to these items by name! 

11 
*) 

12 
structure Ind_Syntax = 

13 
struct 

14 
(*Make a definition lhs==rhs, checking that vars on lhs contain those of rhs*) 

15 
fun mk_defpair (lhs, rhs) = 

454
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

16 
let val Const(name, _) = head_of lhs 
0  17 
val dummy = assert (term_vars rhs subset term_vars lhs 
454
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

18 
andalso 
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

19 
term_frees rhs subset term_frees lhs 
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

20 
andalso 
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

21 
term_tvars rhs subset term_tvars lhs 
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

22 
andalso 
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

23 
term_tfrees rhs subset term_tfrees lhs) 
0  24 
("Extra variables on RHS in definition of " ^ name) 
454
0d19ab250cc9
removed flatten_term and replaced add_axioms by add_axioms_i
clasohm
parents:
444
diff
changeset

25 
in (name ^ "_def", Logic.mk_equals (lhs, rhs)) end; 
0  26 

516  27 
fun get_def thy s = get_axiom thy (s^"_def"); 
28 

0  29 
fun lookup_const sign a = Symtab.lookup(#const_tab (Sign.rep_sg sign), a); 
30 

31 
(*export to Pure/library? *) 

32 
fun assert_all pred l msg_fn = 

33 
let fun asl [] = () 

34 
 asl (x::xs) = if pred x then asl xs 

35 
else error (msg_fn x) 

36 
in asl l end; 

37 

38 

39 
(** Abstract syntax definitions for FOL and ZF **) 

40 

41 
val iT = Type("i",[]) 

42 
and oT = Type("o",[]); 

43 

44 
fun ap t u = t$u; 

45 
fun app t (u1,u2) = t $ u1 $ u2; 

46 

47 
(*Given u expecting arguments of types [T1,...,Tn], create term of 

48 
type T1*...*Tn => i using split*) 

49 
fun ap_split split u [ ] = Abs("null", iT, u) 

50 
 ap_split split u [_] = u 

51 
 ap_split split u [_,_] = split $ u 

52 
 ap_split split u (T::Ts) = 

53 
split $ (Abs("v", T, ap_split split (u $ Bound(length Ts  2)) Ts)); 

54 

55 
val conj = Const("op &", [oT,oT]>oT) 

56 
and disj = Const("op ", [oT,oT]>oT) 

57 
and imp = Const("op >", [oT,oT]>oT); 

58 

59 
val eq_const = Const("op =", [iT,iT]>oT); 

60 

61 
val mem_const = Const("op :", [iT,iT]>oT); 

62 

63 
val exists_const = Const("Ex", [iT>oT]>oT); 

64 
fun mk_exists (Free(x,T),P) = exists_const $ (absfree (x,T,P)); 

65 

66 
val all_const = Const("All", [iT>oT]>oT); 

67 
fun mk_all (Free(x,T),P) = all_const $ (absfree (x,T,P)); 

68 

69 
(*Creates All(%v.v:A > P(v)) rather than Ball(A,P) *) 

70 
fun mk_all_imp (A,P) = 

71 
all_const $ Abs("v", iT, imp $ (mem_const $ Bound 0 $ A) $ (P $ Bound 0)); 

72 

73 
val Part_const = Const("Part", [iT,iT>iT]>iT); 

74 

75 
val Collect_const = Const("Collect", [iT,iT>oT]>iT); 

76 
fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); 

77 

78 
val Trueprop = Const("Trueprop",oT>propT); 

79 
fun mk_tprop P = Trueprop $ P; 

80 

81 
(*Prove a goal stated as a term, with exception handling*) 

82 
fun prove_term sign defs (P,tacsf) = 

231  83 
let val ct = cterm_of sign P 
0  84 
in prove_goalw_cterm defs ct tacsf 
85 
handle e => (writeln ("Exception in proof of\n" ^ 

231  86 
string_of_cterm ct); 
0  87 
raise e) 
88 
end; 

89 

90 
(*Read an assumption in the given theory*) 

231  91 
fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT)); 
0  92 

516  93 
fun readtm sign T a = 
94 
read_cterm sign (a,T) > term_of 

95 
handle ERROR => error ("The error above occurred for " ^ a); 

96 

97 
(*Skipping initial blanks, find the first identifier*) 

98 
fun scan_to_id s = 

99 
s > explode > take_prefix is_blank > #2 > Lexicon.scan_id > #1 

100 
handle LEXICAL_ERROR => error ("Expected to find an identifier in " ^ s); 

101 

102 
fun is_backslash c = c = "\\"; 

103 

104 
(*Apply string escapes to a quoted string; see Def of Standard ML, page 3 

105 
Does not handle the \ddd form; no error checking*) 

106 
fun escape [] = [] 

107 
 escape cs = (case take_prefix (not o is_backslash) cs of 

108 
(front, []) => front 

109 
 (front, _::"n"::rest) => front @ ("\n" :: escape rest) 

110 
 (front, _::"t"::rest) => front @ ("\t" :: escape rest) 

111 
 (front, _::"^"::c::rest) => front @ (chr(ord(c)64) :: escape rest) 

112 
 (front, _::"\""::rest) => front @ ("\"" :: escape rest) 

113 
 (front, _::"\\"::rest) => front @ ("\\" :: escape rest) 

114 
 (front, b::c::rest) => 

115 
if is_blank c (*remove any further blanks and the following \ *) 

116 
then front @ escape (tl (snd (take_prefix is_blank rest))) 

117 
else error ("Unrecognized string escape: " ^ implode(b::c::rest))); 

118 

119 
(*Remove the first and last charaters  presumed to be quotes*) 

120 
val trim = implode o escape o rev o tl o rev o tl o explode; 

121 

122 
(*simple errorchecking in the premises of an inductive definition*) 

123 
fun chk_prem rec_hd (Const("op &",_) $ _ $ _) = 

124 
error"Premises may not be conjuctive" 

125 
 chk_prem rec_hd (Const("op :",_) $ t $ X) = 

126 
deny (Logic.occs(rec_hd,t)) "Recursion term on left of member symbol" 

127 
 chk_prem rec_hd t = 

128 
deny (Logic.occs(rec_hd,t)) "Recursion term in side formula"; 

129 

130 

131 
(*Inverse of varifyT. Move to Pure/type.ML?*) 

132 
fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts) 

133 
 unvarifyT (TVar ((a, 0), S)) = TFree (a, S) 

134 
 unvarifyT T = T; 

135 

136 
(*Inverse of varify. Move to Pure/logic.ML?*) 

137 
fun unvarify (Const(a,T)) = Const(a, unvarifyT T) 

138 
 unvarify (Var((a,0), T)) = Free(a, unvarifyT T) 

139 
 unvarify (Var(ixn,T)) = Var(ixn, unvarifyT T) (*nonzero index!*) 

140 
 unvarify (Abs (a,T,body)) = Abs (a, unvarifyT T, unvarify body) 

141 
 unvarify (f$t) = unvarify f $ unvarify t 

142 
 unvarify t = t; 

143 

144 

0  145 
(*Make distinct individual variables a1, a2, a3, ..., an. *) 
146 
fun mk_frees a [] = [] 

147 
 mk_frees a (T::Ts) = Free(a,T) :: mk_frees (bump_string a) Ts; 

148 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

149 
(*Return the conclusion of a rule, of the form t:X*) 
0  150 
fun rule_concl rl = 
435  151 
let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = 
152 
Logic.strip_imp_concl rl 

153 
in (t,X) end; 

154 

155 
(*As above, but return error message if bad*) 

156 
fun rule_concl_msg sign rl = rule_concl rl 

157 
handle Bind => error ("Illformed conclusion of introduction rule: " ^ 

158 
Sign.string_of_term sign rl); 

0  159 

160 
(*For deriving cases rules. CollectD2 discards the domain, which is redundant; 

161 
read_instantiate replaces a propositional variable by a formula variable*) 

162 
val equals_CollectD = 

163 
read_instantiate [("W","?Q")] 

164 
(make_elim (equalityD1 RS subsetD RS CollectD2)); 

165 

166 

167 
(*From HOL/ex/meson.ML: raises exception if no rules apply  unlike RL*) 

168 
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) 

169 
 tryres (th, []) = raise THM("tryres", 0, [th]); 

170 

171 
fun gen_make_elim elim_rls rl = 

172 
standard (tryres (rl, elim_rls @ [revcut_rl])); 

173 

516  174 
(** For datatype definitions **) 
175 

176 
fun dest_mem (Const("op :",_) $ x $ A) = (x,A) 

177 
 dest_mem _ = error "Constructor specifications must have the form x:A"; 

178 

179 
(*read a constructor specification*) 

180 
fun read_construct sign (id, sprems, syn) = 

181 
let val prems = map (readtm sign oT) sprems 

182 
val args = map (#1 o dest_mem) prems 

183 
val T = (map (#2 o dest_Free) args) > iT 

184 
handle TERM _ => error 

185 
"Bad variable in constructor specification" 

186 
val name = const_name id syn (*handle infix constructors*) 

187 
in ((id,T,syn), name, args, prems) end; 

188 

189 
val read_constructs = map o map o read_construct; 

0  190 

516  191 
(*convert constructor specifications into introduction rules*) 
192 
fun mk_intr_tms (rec_tm, constructs) = 

193 
let fun mk_intr ((id,T,syn), name, args, prems) = 

194 
Logic.list_implies 

195 
(map mk_tprop prems, 

196 
mk_tprop (mem_const $ list_comb(Const(name,T), args) $ rec_tm)) 

197 
in map mk_intr constructs end; 

198 

199 
val mk_all_intr_tms = flat o map mk_intr_tms o op ~~; 

0  200 

516  201 
val Un = Const("op Un", [iT,iT]>iT) 
202 
and empty = Const("0", iT) 

203 
and univ = Const("univ", iT>iT) 

204 
and quniv = Const("quniv", iT>iT); 

0  205 

516  206 
(*Make a datatype's domain: form the union of its set parameters*) 
207 
fun union_params rec_tm = 

208 
let val (_,args) = strip_comb rec_tm 

209 
in case (filter (fn arg => type_of arg = iT) args) of 

210 
[] => empty 

211 
 iargs => fold_bal (app Un) iargs 

212 
end; 

213 

214 
fun data_domain rec_tms = 

215 
replicate (length rec_tms) (univ $ union_params (hd rec_tms)); 

216 

217 
fun Codata_domain rec_tms = 

218 
replicate (length rec_tms) (quniv $ union_params (hd rec_tms)); 

0  219 

220 
(*Could go to FOL, but it's hardly general*) 

516  221 
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <> c=b" 
222 
(fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]); 

0  223 

224 
val def_trans = prove_goal IFOL.thy "[ f==g; g(a)=b ] ==> f(a)=b" 

225 
(fn [rew,prem] => [ rewtac rew, rtac prem 1 ]); 

226 

55  227 
(*Delete needless equality assumptions*) 
228 
val refl_thin = prove_goal IFOL.thy "!!P. [ a=a; P ] ==> P" 

229 
(fn _ => [assume_tac 1]); 

0  230 

516  231 
end; 
232 