0

1 
(* Title: typedsimp


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1993 University of Cambridge


5 


6 
Functor for constructing simplifiers. Suitable for Constructive Type


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


8 
simp.ML.


9 
*)


10 


11 
signature TSIMP_DATA =


12 
sig


13 
val refl: thm (*Reflexive law*)


14 
val sym: thm (*Symmetric law*)


15 
val trans: thm (*Transitive law*)


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


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


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


19 
(*Builtin rewrite rules*)


20 
val default_rls: thm list


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


22 
val routine_tac: thm list > int > tactic


23 
end;


24 


25 
signature TSIMP =


26 
sig


27 
val asm_res_tac: thm list > int > tactic


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


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


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


31 
val process_rules: thm list > thm list * thm list


32 
val rewrite_res_tac: int > tactic


33 
val split_eqn: thm


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


35 
val subconv_res_tac: thm list > int > tactic


36 
end;


37 


38 


39 
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =


40 
struct


41 
local open TSimp_data


42 
in


43 


44 
(*For simplifying both sides of an equation:


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


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


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


48 


49 


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


51 
val red_trans = standard (trans RS red_if_equal);


52 


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


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


55 
fun simp_rule rl = rl RS trans;


56 


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


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


59 
fun resimp_rule rl = rl RS red_trans;


60 


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


62 
Make rule for simplifying subterms, e.g.


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


64 
fun subconv_rule rl = rl RS trans_red;


65 


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


67 
else add the rule to other_rls*)


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


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


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


71 


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


73 
fun process_rules rls = foldr add_rule (rls, ([],[]));


74 


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


76 
fun process_rewrites rls =


77 
case process_rules rls of


78 
(simp_rls,[]) => simp_rls


79 
 (_,others) => raise THM


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


81 


82 
(*Process the default rewrite rules*)


83 
val simp_rls = process_rewrites default_rls;


84 


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


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


87 
no ambiguity.*)


88 


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


90 
val rewrite_res_tac = filt_resolve_tac simp_rls 2;


91 


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


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


94 
fun subconv_res_tac congr_rls =


95 
filt_resolve_tac (map subconv_rule congr_rls) 2


96 
ORELSE' filt_resolve_tac [refl,refl_red] 1;


97 


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


99 
fun asm_res_tac asms =


100 
let val (xsimp_rls,xother_rls) = process_rules asms


101 
in routine_tac xother_rls ORELSE'


102 
filt_resolve_tac xsimp_rls 2


103 
end;


104 


105 
(*Single step for simple rewriting*)


106 
fun step_tac (congr_rls,asms) =


107 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE'


108 
subconv_res_tac congr_rls;


109 


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


111 
fun cond_step_tac (prove_cond_tac, congr_rls, asms) =


112 
asm_res_tac asms ORELSE' rewrite_res_tac ORELSE'


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


114 
subconv_res_tac congr_rls;


115 


116 
(*Unconditional normalization tactic*)


117 
fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN


118 
TRYALL (resolve_tac [red_if_equal]);


119 


120 
(*Conditional normalization tactic*)


121 
fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN


122 
TRYALL (resolve_tac [red_if_equal]);


123 


124 
end;


125 
end;


126 


127 
