author  paulson 
Fri, 03 Nov 2000 10:23:24 +0100  
changeset 10368  f7e8abd8ea15 
parent 10015  8c16ec5ba62b 
permissions  rwrr 
9866  1 
(* Title: TFL/post.sml 
3302  2 
ID: $Id$ 
3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

9866  6 
Second part of main module (postprocessing of TFL definitions). 
3302  7 
*) 
8 

9866  9 
signature TFL = 
10 
sig 

11 
val trace: bool ref 

12 
val quiet_mode: bool ref 

13 
val message: string > unit 

14 
val tgoalw: theory > thm list > thm list > thm list 

15 
val tgoal: theory > thm list > thm list 

16 
val std_postprocessor: claset > simpset > thm list > theory > 

17 
{induction: thm, rules: thm, TCs: term list list} > 

18 
{induction: thm, rules: thm, nested_tcs: thm list} 

19 
val define_i: theory > claset > simpset > thm list > thm list > xstring > 

20 
term > term list > theory * {rules: (thm * int) list, induct: thm, tcs: term list} 

21 
val define: theory > claset > simpset > thm list > thm list > xstring > 

22 
string > string list > theory * {rules: (thm * int) list, induct: thm, tcs: term list} 

23 
val defer_i: theory > thm list > xstring > term list > theory * thm 

24 
val defer: theory > thm list > xstring > string list > theory * thm 

25 
end; 

3191  26 

27 
structure Tfl: TFL = 

2112  28 
struct 
29 

9866  30 
structure S = USyntax 
8817  31 

32 

9866  33 
(* messages *) 
34 

35 
val trace = Prim.trace 

6524  36 

9866  37 
val quiet_mode = ref false; 
38 
fun message s = if ! quiet_mode then () else writeln s; 

39 

6524  40 

9866  41 
(* misc *) 
42 

43 
fun read_term thy = Sign.simple_read_term (Theory.sign_of thy) HOLogic.termT; 

6498  44 

8817  45 

9866  46 
(* 
47 
* Extract termination goals so that they can be put it into a goalstack, or 

48 
* have a tactic directly applied to them. 

49 
**) 

50 
fun termination_goals rules = 

51 
map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop) 

52 
(foldr (fn (th,A) => union_term (prems_of th, A)) (rules, [])); 

3191  53 

9866  54 
(* 
55 
* Finds the termination conditions in (highly massaged) definition and 

56 
* puts them into a goalstack. 

57 
**) 

58 
fun tgoalw thy defs rules = 

59 
case termination_goals rules of 

60 
[] => error "tgoalw: no termination conditions to prove" 

61 
 L => goalw_cterm defs 

62 
(Thm.cterm_of (Theory.sign_of thy) 

63 
(HOLogic.mk_Trueprop(USyntax.list_mk_conj L))); 

6498  64 

9866  65 
fun tgoal thy = tgoalw thy []; 
6498  66 

9866  67 
(* 
6498  68 
* Three postprocessors are applied to the definition. It 
69 
* attempts to prove wellfoundedness of the given relation, simplifies the 

9866  70 
* nonproved termination conditions, and finally attempts to prove the 
6498  71 
* simplified termination conditions. 
3405  72 
**) 
9866  73 
fun std_postprocessor cs ss wfs = 
74 
Prim.postprocess 

75 
{wf_tac = REPEAT (ares_tac wfs 1), 

76 
terminator = asm_simp_tac ss 1 

77 
THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1), 

78 
simplifier = Rules.simpl_conv ss []}; 

2112  79 

80 

81 

9866  82 
val concl = #2 o Rules.dest_thm; 
2112  83 

3191  84 
(* 
9866  85 
* Postprocess a definition made by "define". This is a separate stage of 
3191  86 
* processing from the definition stage. 
2112  87 
**) 
9866  88 
local 
89 
structure R = Rules 

90 
structure U = Utils 

2112  91 

9866  92 
(* The rest of these local definitions are for the tricky nested case *) 
93 
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl 

2112  94 

9866  95 
fun id_thm th = 
96 
let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) 

97 
in lhs aconv rhs 

10015  98 
end handle _ => false (* FIXME do not handle _ !!! *) 
2112  99 

9866  100 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); 
101 
val P_imp_P_iff_True = prover "P > (P= True)" RS mp; 

102 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

103 
fun mk_meta_eq r = case concl_of r of 

104 
Const("==",_)$_$_ => r 

105 
 _ $(Const("op =",_)$_$_) => r RS eq_reflection 

106 
 _ => r RS P_imp_P_eq_True 

3405  107 

9866  108 
(*Is this the best way to invoke the simplifier??*) 
109 
fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L)) 

2112  110 

9866  111 
fun join_assums th = 
112 
let val {sign,...} = rep_thm th 

113 
val tych = cterm_of sign 

114 
val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th))) 

115 
val cntxtl = (#1 o S.strip_imp) lhs (* cntxtl should = cntxtr *) 

116 
val cntxtr = (#1 o S.strip_imp) rhs (* but union is solider *) 

117 
val cntxt = gen_union (op aconv) (cntxtl, cntxtr) 

118 
in 

119 
R.GEN_ALL 

120 
(R.DISCH_ALL 

121 
(rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th))) 

122 
end 

123 
val gen_all = S.gen_all 

124 
in 

125 
fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} = 

126 
let 

127 
val _ = message "Proving induction theorem ..." 

128 
val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs} 

129 
val _ = message "Postprocessing ..."; 

130 
val {rules, induction, nested_tcs} = 

131 
std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs} 

132 
in 

133 
case nested_tcs 

134 
of [] => {induction=induction, rules=rules,tcs=[]} 

135 
 L => let val dummy = message "Simplifying nested TCs ..." 

136 
val (solved,simplified,stubborn) = 

137 
U.itlist (fn th => fn (So,Si,St) => 

138 
if (id_thm th) then (So, Si, th::St) else 

139 
if (solved th) then (th::So, Si, St) 

140 
else (So, th::Si, St)) nested_tcs ([],[],[]) 

141 
val simplified' = map join_assums simplified 

142 
val rewr = full_simplify (ss addsimps (solved @ simplified')); 

143 
val induction' = rewr induction 

144 
and rules' = rewr rules 

145 
in 

146 
{induction = induction', 

147 
rules = rules', 

148 
tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl) 

149 
(simplified@stubborn)} 

150 
end 

151 
end; 

3191  152 

153 

9866  154 
(*lcp: curry the predicate of the induction rule*) 
155 
fun curry_rule rl = split_rule_var 

156 
(head_of (HOLogic.dest_Trueprop (concl_of rl)), 

157 
rl); 

3191  158 

9866  159 
(*lcp: put a theorem into Isabelle form, using metalevel connectives*) 
160 
val meta_outer = 

161 
curry_rule o standard o 

162 
rule_by_tactic (REPEAT 

163 
(FIRSTGOAL (resolve_tac [allI, impI, conjI] 

164 
ORELSE' etac conjE))); 

2112  165 

9866  166 
(*Strip off the outer !P*) 
167 
val spec'= read_instantiate [("x","P::?'b=>bool")] spec; 

3459
112cbb8301dc
Removal of structure Context and its replacement by a theorem list of
paulson
parents:
3405
diff
changeset

168 

9866  169 
fun simplify_defn thy cs ss congs wfs id pats def0 = 
170 
let val def = freezeT def0 RS meta_eq_to_obj_eq 

171 
val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) 

172 
val {lhs=f,rhs} = S.dest_eq (concl def) 

173 
val (_,[R,_]) = S.strip_comb rhs 

174 
val {induction, rules, tcs} = 

175 
proof_stage cs ss wfs theory 

176 
{f = f, R = R, rules = rules, 

177 
full_pats_TCs = full_pats_TCs, 

178 
TCs = TCs} 

9904  179 
val rules' = map (standard o Rulify.rulify_no_asm) (R.CONJUNCTS rules) 
180 
in {induct = meta_outer (Rulify.rulify_no_asm (induction RS spec')), 

9866  181 
rules = ListPair.zip(rules', rows), 
182 
tcs = (termination_goals rules') @ tcs} 

183 
end 

184 
handle Utils.ERR {mesg,func,module} => 

185 
error (mesg ^ 

186 
"\n (In TFL function " ^ module ^ "." ^ func ^ ")"); 

2112  187 

3191  188 
(* 
9866  189 
* Defining a function with an associated termination relation. 
7262  190 
**) 
9866  191 
fun define_i thy cs ss congs wfs fid R eqs = 
192 
let val {functional,pats} = Prim.mk_functional thy eqs 

193 
val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional 

194 
in (thy, simplify_defn thy cs ss congs wfs fid pats def) end; 

7262  195 

9866  196 
fun define thy cs ss congs wfs fid R seqs = 
197 
define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs) 

198 
handle Utils.ERR {mesg,...} => error mesg; 

7262  199 

200 

201 
(* 

3191  202 
* 
6498  203 
* Definitions with synthesized termination relation 
3191  204 
* 
205 
**) 

6498  206 

9866  207 
local open USyntax 
208 
in 

209 
fun func_of_cond_eqn tm = 

210 
#1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm))))))) 

211 
end; 

6498  212 

9866  213 
fun defer_i thy congs fid eqs = 
214 
let val {rules,R,theory,full_pats_TCs,SV,...} = 

215 
Prim.lazyR_def thy (Sign.base_name fid) congs eqs 

10015  216 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) (* FIXME do not handle _ !!! *) 
9866  217 
val dummy = message "Proving induction theorem ..."; 
218 
val induction = Prim.mk_induction theory 

219 
{fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs} 

220 
in (theory, 

221 
(*return the conjoined induction rule and recursion equations, 

222 
with assumptions remaining to discharge*) 

223 
standard (induction RS (rules RS conjI))) 

224 
end 

6498  225 

9866  226 
fun defer thy congs fid seqs = 
227 
defer_i thy congs fid (map (read_term thy) seqs) 

228 
handle Utils.ERR {mesg,...} => error mesg; 

229 
end; 

6498  230 

2112  231 
end; 