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