src/Provers/typedsimp.ML
changeset 0 a5a9c433f639
child 15570 8d8c70b41bab
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Provers/typedsimp.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,127 @@
     1.4 +(*  Title: 	typedsimp
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1993  University of Cambridge
     1.8 +
     1.9 +Functor for constructing simplifiers.  Suitable for Constructive Type
    1.10 +Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try
    1.11 +simp.ML.
    1.12 +*)
    1.13 +
    1.14 +signature TSIMP_DATA =
    1.15 +  sig
    1.16 +  val refl: thm		(*Reflexive law*)
    1.17 +  val sym: thm		(*Symmetric law*)
    1.18 +  val trans: thm	(*Transitive law*)
    1.19 +  val refl_red: thm	(* reduce(a,a) *)
    1.20 +  val trans_red: thm	(* [|a=b; reduce(b,c) |] ==> a=c *)
    1.21 +  val red_if_equal: thm (* a=b ==> reduce(a,b) *)
    1.22 +  (*Built-in rewrite rules*)
    1.23 +  val default_rls: thm list
    1.24 +  (*Type checking or similar -- solution of routine conditions*)
    1.25 +  val routine_tac: thm list -> int -> tactic
    1.26 +  end;
    1.27 +
    1.28 +signature TSIMP =
    1.29 +  sig
    1.30 +  val asm_res_tac: thm list -> int -> tactic   
    1.31 +  val cond_norm_tac: ((int->tactic) * thm list * thm list) -> tactic
    1.32 +  val cond_step_tac: ((int->tactic) * thm list * thm list) -> int -> tactic
    1.33 +  val norm_tac: (thm list * thm list) -> tactic
    1.34 +  val process_rules: thm list -> thm list * thm list
    1.35 +  val rewrite_res_tac: int -> tactic   
    1.36 +  val split_eqn: thm
    1.37 +  val step_tac: (thm list * thm list) -> int -> tactic
    1.38 +  val subconv_res_tac: thm list -> int -> tactic   
    1.39 +  end;
    1.40 +
    1.41 +
    1.42 +functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 
    1.43 +struct
    1.44 +local open TSimp_data
    1.45 +in
    1.46 +
    1.47 +(*For simplifying both sides of an equation:
    1.48 +      [| a=c; b=c |] ==> b=a
    1.49 +  Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
    1.50 +val split_eqn = standard (sym RSN (2,trans) RS sym);
    1.51 +
    1.52 +
    1.53 +(*    [| a=b; b=c |] ==> reduce(a,c)  *)
    1.54 +val red_trans = standard (trans RS red_if_equal);
    1.55 +
    1.56 +(*For REWRITE rule: Make a reduction rule for simplification, e.g.
    1.57 +  [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)
    1.58 +fun simp_rule rl = rl RS trans;
    1.59 +
    1.60 +(*For REWRITE rule: Make rule for resimplifying if possible, e.g.
    1.61 +  [| a: C(0); ...; a=c: C(0) |] ==> reduce(rec(0,a,b), c)  *)
    1.62 +fun resimp_rule rl = rl RS red_trans;
    1.63 +
    1.64 +(*For CONGRUENCE rule, like a=b ==> succ(a) = succ(b)
    1.65 +  Make rule for simplifying subterms, e.g.
    1.66 +  [| a=b: N; reduce(succ(b), c) |] ==> succ(a)=c: N   *)
    1.67 +fun subconv_rule rl = rl RS trans_red;
    1.68 +
    1.69 +(*If the rule proves an equality then add both forms to simp_rls
    1.70 +  else add the rule to other_rls*)
    1.71 +fun add_rule (rl, (simp_rls, other_rls)) =
    1.72 +    (simp_rule rl :: resimp_rule rl :: simp_rls, other_rls)
    1.73 +    handle THM _ => (simp_rls, rl :: other_rls);
    1.74 +
    1.75 +(*Given the list rls, return the pair (simp_rls, other_rls).*)
    1.76 +fun process_rules rls = foldr add_rule (rls, ([],[]));
    1.77 +
    1.78 +(*Given list of rewrite rules, return list of both forms, reject others*)
    1.79 +fun process_rewrites rls = 
    1.80 +  case process_rules rls of
    1.81 +      (simp_rls,[])  =>  simp_rls
    1.82 +    | (_,others) => raise THM 
    1.83 +	("process_rewrites: Ill-formed rewrite", 0, others);
    1.84 +
    1.85 +(*Process the default rewrite rules*)
    1.86 +val simp_rls = process_rewrites default_rls;
    1.87 +
    1.88 +(*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac
    1.89 +  will fail!  The filter will pass all the rules, and the bound permits
    1.90 +  no ambiguity.*)
    1.91 +
    1.92 +(*Resolution with rewrite/sub rules.  Builds the tree for filt_resolve_tac.*)
    1.93 +val rewrite_res_tac = filt_resolve_tac simp_rls 2;
    1.94 +
    1.95 +(*The congruence rules for simplifying subterms.  If subgoal is too flexible
    1.96 +    then only refl,refl_red will be used (if even them!). *)
    1.97 +fun subconv_res_tac congr_rls =
    1.98 +  filt_resolve_tac (map subconv_rule congr_rls) 2
    1.99 +  ORELSE'  filt_resolve_tac [refl,refl_red] 1;
   1.100 +
   1.101 +(*Resolve with asms, whether rewrites or not*)
   1.102 +fun asm_res_tac asms =
   1.103 +    let val (xsimp_rls,xother_rls) = process_rules asms
   1.104 +    in 	routine_tac xother_rls  ORELSE'  
   1.105 +	filt_resolve_tac xsimp_rls 2
   1.106 +    end;
   1.107 +
   1.108 +(*Single step for simple rewriting*)
   1.109 +fun step_tac (congr_rls,asms) =
   1.110 +    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   1.111 +    subconv_res_tac congr_rls;
   1.112 +
   1.113 +(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*)
   1.114 +fun cond_step_tac (prove_cond_tac, congr_rls, asms) =
   1.115 +    asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  
   1.116 +    (resolve_tac [trans, red_trans]  THEN'  prove_cond_tac)  ORELSE'  
   1.117 +    subconv_res_tac congr_rls;
   1.118 +
   1.119 +(*Unconditional normalization tactic*)
   1.120 +fun norm_tac arg = REPEAT_FIRST (step_tac arg)  THEN
   1.121 +    TRYALL (resolve_tac [red_if_equal]);
   1.122 +
   1.123 +(*Conditional normalization tactic*)
   1.124 +fun cond_norm_tac arg = REPEAT_FIRST (cond_step_tac arg)  THEN
   1.125 +    TRYALL (resolve_tac [red_if_equal]);
   1.126 +
   1.127 +end;
   1.128 +end;
   1.129 +
   1.130 +