1(* Title: Provers/typedsimp.ML 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1993 University of Cambridge 4 5Functor for constructing simplifiers. Suitable for Constructive Type 6Theory with its typed reflexivity axiom a:A ==> a=a:A. For most logics try 7simp.ML. 8*) 9 10signature TSIMP_DATA = 11sig 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 (*Built-in rewrite rules*) 19 val default_rls: thm list 20 (*Type checking or similar -- solution of routine conditions*) 21 val routine_tac: Proof.context -> thm list -> int -> tactic 22end; 23 24signature TSIMP = 25sig 26 val asm_res_tac: Proof.context -> thm list -> int -> tactic 27 val cond_norm_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> tactic 28 val cond_step_tac: Proof.context -> ((int->tactic) * thm list * thm list) -> int -> tactic 29 val norm_tac: Proof.context -> (thm list * thm list) -> tactic 30 val process_rules: thm list -> thm list * thm list 31 val rewrite_res_tac: Proof.context -> int -> tactic 32 val split_eqn: thm 33 val step_tac: Proof.context -> (thm list * thm list) -> int -> tactic 34 val subconv_res_tac: Proof.context -> thm list -> int -> tactic 35end; 36 37functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 38struct 39local open TSimp_data 40in 41 42(*For simplifying both sides of an equation: 43 [| a=c; b=c |] ==> b=a 44 Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) 45val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym); 46 47 48(* [| a=b; b=c |] ==> reduce(a,c) *) 49val red_trans = Drule.zero_var_indexes (trans RS red_if_equal); 50 51(*For REWRITE rule: Make a reduction rule for simplification, e.g. 52 [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *) 53fun simp_rule rl = rl RS trans; 54 55(*For REWRITE rule: Make rule for resimplifying if possible, e.g. 56 [| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c) *) 57fun resimp_rule rl = rl RS red_trans; 58 59(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b) 60 Make rule for simplifying subterms, e.g. 61 [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N *) 62fun subconv_rule rl = rl RS trans_red; 63 64(*If the rule proves an equality then add both forms to simp_rls 65 else add the rule to other_rls*) 66fun add_rule rl (simp_rls, other_rls) = 67 (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls) 68 handle THM _ => (simp_rls, rl :: other_rls); 69 70(*Given the list rls, return the pair (simp_rls, other_rls).*) 71fun process_rules rls = fold_rev add_rule rls ([], []); 72 73(*Given list of rewrite rules, return list of both forms, reject others*) 74fun process_rewrites rls = 75 case process_rules rls of 76 (simp_rls,[]) => simp_rls 77 | (_,others) => raise THM 78 ("process_rewrites: Ill-formed rewrite", 0, others); 79 80(*Process the default rewrite rules*) 81val simp_rls = process_rewrites default_rls; 82val simp_net = Tactic.build_net simp_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.*) 89fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net; 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!). *) 93fun subconv_res_tac ctxt congr_rls = 94 filt_resolve_from_net_tac ctxt 2 (Tactic.build_net (map subconv_rule congr_rls)) 95 ORELSE' filt_resolve_from_net_tac ctxt 1 (Tactic.build_net [refl, refl_red]); 96 97(*Resolve with asms, whether rewrites or not*) 98fun asm_res_tac ctxt asms = 99 let val (xsimp_rls, xother_rls) = process_rules asms 100 in routine_tac ctxt xother_rls ORELSE' 101 filt_resolve_from_net_tac ctxt 2 (Tactic.build_net xsimp_rls) 102 end; 103 104(*Single step for simple rewriting*) 105fun step_tac ctxt (congr_rls, asms) = 106 asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE' 107 subconv_res_tac ctxt congr_rls; 108 109(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) 110fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) = 111 asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE' 112 (resolve_tac ctxt [trans, red_trans] THEN' prove_cond_tac) ORELSE' 113 subconv_res_tac ctxt congr_rls; 114 115(*Unconditional normalization tactic*) 116fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg) THEN 117 TRYALL (resolve_tac ctxt [red_if_equal]); 118 119(*Conditional normalization tactic*) 120fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg) THEN 121 TRYALL (resolve_tac ctxt [red_if_equal]); 122 123end; 124end; 125 126