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