src/Provers/typedsimp.ML
 author skalberg Thu Mar 03 12:43:01 2005 +0100 (2005-03-03) changeset 15570 8d8c70b41bab parent 0 a5a9c433f639 child 15574 b1d1b5bfc464 permissions -rw-r--r--
Move towards standard functions.
 clasohm@0 ` 1` ```(* Title: typedsimp ``` clasohm@0 ` 2` ``` ID: \$Id\$ ``` clasohm@0 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` clasohm@0 ` 4` ``` Copyright 1993 University of Cambridge ``` clasohm@0 ` 5` clasohm@0 ` 6` ```Functor for constructing simplifiers. Suitable for Constructive Type ``` clasohm@0 ` 7` ```Theory with its typed reflexivity axiom a:A ==> a=a:A. For most logics try ``` clasohm@0 ` 8` ```simp.ML. ``` clasohm@0 ` 9` ```*) ``` clasohm@0 ` 10` clasohm@0 ` 11` ```signature TSIMP_DATA = ``` clasohm@0 ` 12` ``` sig ``` clasohm@0 ` 13` ``` val refl: thm (*Reflexive law*) ``` clasohm@0 ` 14` ``` val sym: thm (*Symmetric law*) ``` clasohm@0 ` 15` ``` val trans: thm (*Transitive law*) ``` clasohm@0 ` 16` ``` val refl_red: thm (* reduce(a,a) *) ``` clasohm@0 ` 17` ``` val trans_red: thm (* [|a=b; reduce(b,c) |] ==> a=c *) ``` clasohm@0 ` 18` ``` val red_if_equal: thm (* a=b ==> reduce(a,b) *) ``` clasohm@0 ` 19` ``` (*Built-in rewrite rules*) ``` clasohm@0 ` 20` ``` val default_rls: thm list ``` clasohm@0 ` 21` ``` (*Type checking or similar -- solution of routine conditions*) ``` clasohm@0 ` 22` ``` val routine_tac: thm list -> int -> tactic ``` clasohm@0 ` 23` ``` end; ``` clasohm@0 ` 24` clasohm@0 ` 25` ```signature TSIMP = ``` clasohm@0 ` 26` ``` sig ``` clasohm@0 ` 27` ``` val asm_res_tac: thm list -> int -> tactic ``` clasohm@0 ` 28` ``` val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic ``` clasohm@0 ` 29` ``` val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic ``` clasohm@0 ` 30` ``` val norm_tac: (thm list * thm list) -> tactic ``` clasohm@0 ` 31` ``` val process_rules: thm list -> thm list * thm list ``` clasohm@0 ` 32` ``` val rewrite_res_tac: int -> tactic ``` clasohm@0 ` 33` ``` val split_eqn: thm ``` clasohm@0 ` 34` ``` val step_tac: (thm list * thm list) -> int -> tactic ``` clasohm@0 ` 35` ``` val subconv_res_tac: thm list -> int -> tactic ``` clasohm@0 ` 36` ``` end; ``` clasohm@0 ` 37` clasohm@0 ` 38` clasohm@0 ` 39` ```functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = ``` clasohm@0 ` 40` ```struct ``` clasohm@0 ` 41` ```local open TSimp_data ``` clasohm@0 ` 42` ```in ``` clasohm@0 ` 43` clasohm@0 ` 44` ```(*For simplifying both sides of an equation: ``` clasohm@0 ` 45` ``` [| a=c; b=c |] ==> b=a ``` clasohm@0 ` 46` ``` Can use resolve_tac [split_eqn] to prepare an equation for simplification. *) ``` clasohm@0 ` 47` ```val split_eqn = standard (sym RSN (2,trans) RS sym); ``` clasohm@0 ` 48` clasohm@0 ` 49` clasohm@0 ` 50` ```(* [| a=b; b=c |] ==> reduce(a,c) *) ``` clasohm@0 ` 51` ```val red_trans = standard (trans RS red_if_equal); ``` clasohm@0 ` 52` clasohm@0 ` 53` ```(*For REWRITE rule: Make a reduction rule for simplification, e.g. ``` clasohm@0 ` 54` ``` [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *) ``` clasohm@0 ` 55` ```fun simp_rule rl = rl RS trans; ``` clasohm@0 ` 56` clasohm@0 ` 57` ```(*For REWRITE rule: Make rule for resimplifying if possible, e.g. ``` clasohm@0 ` 58` ``` [| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c) *) ``` clasohm@0 ` 59` ```fun resimp_rule rl = rl RS red_trans; ``` clasohm@0 ` 60` clasohm@0 ` 61` ```(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b) ``` clasohm@0 ` 62` ``` Make rule for simplifying subterms, e.g. ``` clasohm@0 ` 63` ``` [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N *) ``` clasohm@0 ` 64` ```fun subconv_rule rl = rl RS trans_red; ``` clasohm@0 ` 65` clasohm@0 ` 66` ```(*If the rule proves an equality then add both forms to simp_rls ``` clasohm@0 ` 67` ``` else add the rule to other_rls*) ``` clasohm@0 ` 68` ```fun add_rule (rl, (simp_rls, other_rls)) = ``` clasohm@0 ` 69` ``` (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls) ``` clasohm@0 ` 70` ``` handle THM _ => (simp_rls, rl :: other_rls); ``` clasohm@0 ` 71` clasohm@0 ` 72` ```(*Given the list rls, return the pair (simp_rls, other_rls).*) ``` skalberg@15570 ` 73` ```fun process_rules rls = Library.foldr add_rule (rls, ([],[])); ``` clasohm@0 ` 74` clasohm@0 ` 75` ```(*Given list of rewrite rules, return list of both forms, reject others*) ``` clasohm@0 ` 76` ```fun process_rewrites rls = ``` clasohm@0 ` 77` ``` case process_rules rls of ``` clasohm@0 ` 78` ``` (simp_rls,[]) => simp_rls ``` clasohm@0 ` 79` ``` | (_,others) => raise THM ``` clasohm@0 ` 80` ``` ("process_rewrites: Ill-formed rewrite", 0, others); ``` clasohm@0 ` 81` clasohm@0 ` 82` ```(*Process the default rewrite rules*) ``` clasohm@0 ` 83` ```val simp_rls = process_rewrites default_rls; ``` clasohm@0 ` 84` clasohm@0 ` 85` ```(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac ``` clasohm@0 ` 86` ``` will fail! The filter will pass all the rules, and the bound permits ``` clasohm@0 ` 87` ``` no ambiguity.*) ``` clasohm@0 ` 88` clasohm@0 ` 89` ```(*Resolution with rewrite/sub rules. Builds the tree for filt_resolve_tac.*) ``` clasohm@0 ` 90` ```val rewrite_res_tac = filt_resolve_tac simp_rls 2; ``` clasohm@0 ` 91` clasohm@0 ` 92` ```(*The congruence rules for simplifying subterms. If subgoal is too flexible ``` clasohm@0 ` 93` ``` then only refl,refl_red will be used (if even them!). *) ``` clasohm@0 ` 94` ```fun subconv_res_tac congr_rls = ``` clasohm@0 ` 95` ``` filt_resolve_tac (map subconv_rule congr_rls) 2 ``` clasohm@0 ` 96` ``` ORELSE' filt_resolve_tac [refl,refl_red] 1; ``` clasohm@0 ` 97` clasohm@0 ` 98` ```(*Resolve with asms, whether rewrites or not*) ``` clasohm@0 ` 99` ```fun asm_res_tac asms = ``` clasohm@0 ` 100` ``` let val (xsimp_rls,xother_rls) = process_rules asms ``` clasohm@0 ` 101` ``` in routine_tac xother_rls ORELSE' ``` clasohm@0 ` 102` ``` filt_resolve_tac xsimp_rls 2 ``` clasohm@0 ` 103` ``` end; ``` clasohm@0 ` 104` clasohm@0 ` 105` ```(*Single step for simple rewriting*) ``` clasohm@0 ` 106` ```fun step_tac (congr_rls,asms) = ``` clasohm@0 ` 107` ``` asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' ``` clasohm@0 ` 108` ``` subconv_res_tac congr_rls; ``` clasohm@0 ` 109` clasohm@0 ` 110` ```(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) ``` clasohm@0 ` 111` ```fun cond_step_tac (prove_cond_tac, congr_rls, asms) = ``` clasohm@0 ` 112` ``` asm_res_tac asms ORELSE' rewrite_res_tac ORELSE' ``` clasohm@0 ` 113` ``` (resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE' ``` clasohm@0 ` 114` ``` subconv_res_tac congr_rls; ``` clasohm@0 ` 115` clasohm@0 ` 116` ```(*Unconditional normalization tactic*) ``` clasohm@0 ` 117` ```fun norm_tac arg = REPEAT_FIRST (step_tac arg) THEN ``` clasohm@0 ` 118` ``` TRYALL (resolve_tac [red_if_equal]); ``` clasohm@0 ` 119` clasohm@0 ` 120` ```(*Conditional normalization tactic*) ``` clasohm@0 ` 121` ```fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg) THEN ``` clasohm@0 ` 122` ``` TRYALL (resolve_tac [red_if_equal]); ``` clasohm@0 ` 123` clasohm@0 ` 124` ```end; ``` clasohm@0 ` 125` ```end; ``` clasohm@0 ` 126` clasohm@0 ` 127`