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
```