src/Provers/typedsimp.ML
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (3 months ago)
changeset 69980 f2e3adfd916f
parent 59498 50b60f501b05
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Provers/typedsimp.ML
     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   (*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
    22 end;
    23 
    24 signature TSIMP =
    25 sig
    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
    35 end;
    36 
    37 functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP =
    38 struct
    39 local open TSimp_data
    40 in
    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. *)
    45 val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym);
    46 
    47 
    48 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
    49 val 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) *)
    53 fun 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)  *)
    57 fun 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   *)
    62 fun 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*)
    66 fun 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).*)
    71 fun process_rules rls = fold_rev add_rule rls ([], []);
    72 
    73 (*Given list of rewrite rules, return list of both forms, reject others*)
    74 fun 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*)
    81 val simp_rls = process_rewrites default_rls;
    82 val 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.*)
    89 fun 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!). *)
    93 fun 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*)
    98 fun 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*)
   105 fun 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.*)
   110 fun 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*)
   116 fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg)  THEN
   117     TRYALL (resolve_tac ctxt [red_if_equal]);
   118 
   119 (*Conditional normalization tactic*)
   120 fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg)  THEN
   121     TRYALL (resolve_tac ctxt [red_if_equal]);
   122 
   123 end;
   124 end;
   125