author  paulson 
Fri, 03 Jan 1997 10:45:31 +0100  
changeset 2467  357adb429fda 
parent 2112  3902e9af752f 
child 3191  14bd6e5985f1 
permissions  rwrr 
2112  1 
structure Tfl 
2 
:sig 

3 
structure Prim : TFL_sig 

4 

5 
val tgoalw : theory > thm list > thm > thm list 

6 
val tgoal: theory > thm > thm list 

7 

8 
val WF_TAC : thm list > tactic 

9 

10 
val simplifier : thm > thm 

11 
val std_postprocessor : theory 

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

13 
> {induction:thm, rules:thm, nested_tcs:thm list} 

14 

15 
val rfunction : theory 

16 
> (thm list > thm > thm) 

17 
> term > term 

18 
> {induction:thm, rules:thm, 

19 
tcs:term list, theory:theory} 

20 

21 
val Rfunction : theory > term > term 

22 
> {induction:thm, rules:thm, 

23 
theory:theory, tcs:term list} 

24 

25 
val function : theory > term > {theory:theory, eq_ind : thm} 

26 
val lazyR_def : theory > term > {theory:theory, eqns : thm} 

27 

28 
val tflcongs : theory > thm list 

29 

30 
end = 

31 
struct 

32 
structure Prim = Prim 

33 

34 
fun tgoalw thy defs thm = 

35 
let val L = Prim.termination_goals thm 

36 
open USyntax 

37 
val g = cterm_of (sign_of thy) (mk_prop(list_mk_conj L)) 

38 
in goalw_cterm defs g 

39 
end; 

40 

41 
val tgoal = Utils.C tgoalw []; 

42 

43 
fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) 

44 
val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, 

45 
wf_pred_nat, wf_pred_list, wf_trancl]; 

46 

47 
val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def, 

48 
fst_conv,snd_conv, 

49 
mem_Collect_eq,lessI]) 1 

50 
THEN TRY(fast_tac set_cs 1); 

51 

52 
val simpls = [less_eq RS eq_reflection, 

53 
lex_prod_def, measure_def, inv_image_def, 

54 
fst_conv RS eq_reflection, snd_conv RS eq_reflection, 

55 
mem_Collect_eq RS eq_reflection(*, length_Cons RS eq_reflection*)]; 

56 

57 
val std_postprocessor = Prim.postprocess{WFtac = WFtac, 

58 
terminator = terminator, 

59 
simplifier = Prim.Rules.simpl_conv simpls}; 

60 

61 
val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ 

62 
[pred_nat_def,pred_list_def]); 

63 
fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); 

64 

65 

66 
local structure S = Prim.USyntax 

67 
in 

68 
fun func_of_cond_eqn tm = 

69 
#1(S.strip_comb(#lhs(S.dest_eq(#2(S.strip_forall(#2(S.strip_imp tm))))))) 

70 
end; 

71 

72 

73 
val concl = #2 o Prim.Rules.dest_thm; 

74 

75 
(* 

76 
* Defining a function with an associated termination relation. Lots of 

77 
* postprocessing takes place. 

78 
**) 

79 
local 

80 
structure S = Prim.USyntax 

81 
structure R = Prim.Rules 

82 
structure U = Utils 

83 

84 
val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl 

85 

86 
fun id_thm th = 

87 
let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th)))) 

88 
in S.aconv lhs rhs 

89 
end handle _ => false 

90 

91 
fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]); 

92 
val P_imp_P_iff_True = prover "P > (P= True)" RS mp; 

93 
val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection; 

94 
fun mk_meta_eq r = case concl_of r of 

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

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

97 
 _ => r RS P_imp_P_eq_True 

98 
fun rewrite L = rewrite_rule (map mk_meta_eq (Utils.filter(not o id_thm) L)) 

99 

100 
fun join_assums th = 

101 
let val {sign,...} = rep_thm th 

102 
val tych = cterm_of sign 

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

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

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

106 
val cntxt = U.union S.aconv cntxtl cntxtr 

107 
in 

108 
R.GEN_ALL 

109 
(R.DISCH_ALL 

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

111 
end 

112 
val gen_all = S.gen_all 

113 
in 

114 
fun rfunction theory reducer R eqs = 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

115 
let val _ = prs "Making definition.. " 
2112  116 
val {rules,theory, full_pats_TCs, 
117 
TCs,...} = Prim.gen_wfrec_definition theory {R=R,eqs=eqs} 

118 
val f = func_of_cond_eqn(concl(R.CONJUNCT1 rules handle _ => rules)) 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

119 
val _ = prs "Definition made.\n" 
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

120 
val _ = prs "Proving induction theorem.. " 
2112  121 
val ind = Prim.mk_induction theory f R full_pats_TCs 
2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

122 
val _ = prs "Proved induction theorem.\n" 
2112  123 
val pp = std_postprocessor theory 
2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

124 
val _ = prs "Postprocessing.. " 
2112  125 
val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs} 
126 
val normal_tcs = Prim.termination_goals rules 

127 
in 

128 
case nested_tcs 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

129 
of [] => (prs "Postprocessing done.\n"; 
2112  130 
{theory=theory, induction=induction, rules=rules,tcs=normal_tcs}) 
2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

131 
 L => let val _ = prs "Simplifying nested TCs.. " 
2112  132 
val (solved,simplified,stubborn) = 
133 
U.itlist (fn th => fn (So,Si,St) => 

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

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

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

137 
val simplified' = map join_assums simplified 

138 
val induction' = reducer (solved@simplified') induction 

139 
val rules' = reducer (solved@simplified') rules 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

140 
val _ = prs "Postprocessing done.\n" 
2112  141 
in 
142 
{induction = induction', 

143 
rules = rules', 

144 
tcs = normal_tcs @ 

145 
map (gen_all o S.rhs o #2 o S.strip_forall o concl) 

146 
(simplified@stubborn), 

147 
theory = theory} 

148 
end 

149 
end 

150 
handle (e as Utils.ERR _) => Utils.Raise e 

151 
 e => print_exn e 

152 

153 

154 
fun Rfunction thry = 

155 
rfunction thry 

156 
(fn thl => rewrite (map standard thl @ #simps(rep_ss HOL_ss))); 

157 

158 

159 
end; 

160 

161 

162 
local structure R = Prim.Rules 

163 
in 

164 
fun function theory eqs = 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

165 
let val _ = prs "Making definition.. " 
2112  166 
val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs 
167 
val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) 

2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

168 
val _ = prs "Definition made.\n" 
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

169 
val _ = prs "Proving induction theorem.. " 
2112  170 
val induction = Prim.mk_induction theory f R full_pats_TCs 
2467
357adb429fda
Conversion to Basis Library (using prs instead of output)
paulson
parents:
2112
diff
changeset

171 
val _ = prs "Induction theorem proved.\n" 
2112  172 
in {theory = theory, 
173 
eq_ind = standard (induction RS (rules RS conjI))} 

174 
end 

175 
handle (e as Utils.ERR _) => Utils.Raise e 

176 
 e => print_exn e 

177 
end; 

178 

179 

180 
fun lazyR_def theory eqs = 

181 
let val {rules,theory, ...} = Prim.lazyR_def theory eqs 

182 
in {eqns=rules, theory=theory} 

183 
end 

184 
handle (e as Utils.ERR _) => Utils.Raise e 

185 
 e => print_exn e; 

186 

187 

188 
val () = Prim.Context.write[Thms.LET_CONG, Thms.COND_CONG]; 

189 

190 
end; 