0

1 
(* Title: typedsimp


2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


3 
Copyright 1993 University of Cambridge


4 


5 
Functor for constructing simplifiers. Suitable for Constructive Type


6 
Theory with its typed reflexivity axiom a:A ==> a=a:A. For most logics try


7 
simp.ML.


8 
*)


9 


10 
signature TSIMP_DATA =


11 
sig


12 
val refl: thm (*Reflexive law*)


13 
val sym: thm (*Symmetric law*)


14 
val trans: thm (*Transitive law*)


15 
val refl_red: thm (* reduce(a,a) *)


16 
val trans_red: thm (* [a=b; reduce(b,c) ] ==> a=c *)


17 
val red_if_equal: thm (* a=b ==> reduce(a,b) *)


18 
(*Builtin rewrite rules*)


19 
val default_rls: thm list


20 
(*Type checking or similar  solution of routine conditions*)


21 
val routine_tac: thm list > int > tactic


22 
end;


23 


24 
signature TSIMP =


25 
sig


26 
val asm_res_tac: thm list > int > tactic


27 
val cond_norm_tac: ((int>tactic) * thm list * thm list) > tactic


28 
val cond_step_tac: ((int>tactic) * thm list * thm list) > int > tactic


29 
val norm_tac: (thm list * thm list) > tactic


30 
val process_rules: thm list > thm list * thm list


31 
val rewrite_res_tac: int > tactic


32 
val split_eqn: thm


33 
val step_tac: (thm list * thm list) > int > tactic


34 
val subconv_res_tac: thm list > int > tactic


35 
end;


36 


37 


38 
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =


39 
struct


40 
local open TSimp_data


41 
in


42 


43 
(*For simplifying both sides of an equation:


44 
[ a=c; b=c ] ==> b=a


45 
Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)


46 
val split_eqn = standard (sym RSN (2,trans) RS sym);


47 


48 


49 
(* [ a=b; b=c ] ==> reduce(a,c) *)


50 
val red_trans = standard (trans RS red_if_equal);


51 


52 
(*For REWRITE rule: Make a reduction rule for simplification, e.g.


53 
[ a: C(0); ... ; a=c: C(0) ] ==> rec(0,a,b) = c: C(0) *)


54 
fun simp_rule rl = rl RS trans;


55 


56 
(*For REWRITE rule: Make rule for resimplifying if possible, e.g.


57 
[ a: C(0); ...; a=c: C(0) ] ==> reduce(rec(0,a,b), c) *)


58 
fun resimp_rule rl = rl RS red_trans;


59 


60 
(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b)


61 
Make rule for simplifying subterms, e.g.


62 
[ a=b: N; reduce(succ(b), c) ] ==> succ(a)=c: N *)


63 
fun subconv_rule rl = rl RS trans_red;


64 


65 
(*If the rule proves an equality then add both forms to simp_rls


66 
else add the rule to other_rls*)


67 
fun add_rule (rl, (simp_rls, other_rls)) =


68 
(simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)


69 
handle THM _ => (simp_rls, rl :: other_rls);


70 


71 
(*Given the list rls, return the pair (simp_rls, other_rls).*)

30190

72 
fun process_rules rls = List.foldr add_rule ([],[]) rls;

0

73 


74 
(*Given list of rewrite rules, return list of both forms, reject others*)


75 
fun process_rewrites rls =


76 
case process_rules rls of


77 
(simp_rls,[]) => simp_rls


78 
 (_,others) => raise THM


79 
("process_rewrites: Illformed rewrite", 0, others);


80 


81 
(*Process the default rewrite rules*)


82 
val simp_rls = process_rewrites default_rls;


83 


84 
(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac


85 
will fail! The filter will pass all the rules, and the bound permits


86 
no ambiguity.*)


87 


88 
(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*)


89 
val rewrite_res_tac = filt_resolve_tac simp_rls 2;


90 


91 
(*The congruence rules for simplifying subterms. If subgoal is too flexible


92 
then only refl,refl_red will be used (if even them!). *)


93 
fun subconv_res_tac congr_rls =


94 
filt_resolve_tac (map subconv_rule congr_rls) 2


95 
ORELSE' filt_resolve_tac [refl,refl_red] 1;


96 


97 
(*Resolve with asms, whether rewrites or not*)


98 
fun asm_res_tac asms =


99 
let val (xsimp_rls,xother_rls) = process_rules asms


100 
in routine_tac xother_rls ORELSE'


101 
filt_resolve_tac xsimp_rls 2


102 
end;


103 


104 
(*Single step for simple rewriting*)


105 
fun step_tac (congr_rls,asms) =


106 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE'


107 
subconv_res_tac congr_rls;


108 


109 
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)


110 
fun cond_step_tac (prove_cond_tac, congr_rls, asms) =


111 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE'


112 
(resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE'


113 
subconv_res_tac congr_rls;


114 


115 
(*Unconditional normalization tactic*)


116 
fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN


117 
TRYALL (resolve_tac [red_if_equal]);


118 


119 
(*Conditional normalization tactic*)


120 
fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN


121 
TRYALL (resolve_tac [red_if_equal]);


122 


123 
end;


124 
end;


125 


126 
