author  wenzelm 
Sat, 20 Dec 2014 22:23:37 +0100  
changeset 59164  ff40c53d1af9 
parent 58963  26bf09b95dda 
child 59498  50b60f501b05 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

1 
(* Title: Provers/typedsimp.ML 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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 = 

59164  11 
sig 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

12 
val refl: thm (*Reflexive law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

13 
val sym: thm (*Symmetric law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

14 
val trans: thm (*Transitive law*) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

15 
val refl_red: thm (* reduce(a,a) *) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

16 
val trans_red: thm (* [a=b; reduce(b,c) ] ==> a=c *) 
0  17 
val red_if_equal: thm (* a=b ==> reduce(a,b) *) 
18 
(*Builtin rewrite rules*) 

19 
val default_rls: thm list 

20 
(*Type checking or similar  solution of routine conditions*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

21 
val routine_tac: Proof.context > thm list > int > tactic 
59164  22 
end; 
0  23 

24 
signature TSIMP = 

59164  25 
sig 
26 
val asm_res_tac: Proof.context > thm list > int > tactic 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

27 
val cond_norm_tac: Proof.context > ((int>tactic) * thm list * thm list) > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

28 
val cond_step_tac: Proof.context > ((int>tactic) * thm list * thm list) > int > tactic 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

29 
val norm_tac: Proof.context > (thm list * thm list) > tactic 
0  30 
val process_rules: thm list > thm list * thm list 
59164  31 
val rewrite_res_tac: Proof.context > int > tactic 
0  32 
val split_eqn: thm 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

33 
val step_tac: Proof.context > (thm list * thm list) > int > tactic 
59164  34 
val subconv_res_tac: Proof.context > thm list > int > tactic 
35 
end; 

0  36 

59164  37 
functor TSimpFun (TSimp_data: TSIMP_DATA) : TSIMP = 
0  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. *) 

45659
09539cdffcd7
avoid stepping outside of context  plain zero_var_indexes should be sufficient;
wenzelm
parents:
35021
diff
changeset

45 
val split_eqn = Drule.zero_var_indexes (sym RSN (2,trans) RS sym); 
0  46 

47 

48 
(* [ a=b; b=c ] ==> reduce(a,c) *) 

45659
09539cdffcd7
avoid stepping outside of context  plain zero_var_indexes should be sufficient;
wenzelm
parents:
35021
diff
changeset

49 
val red_trans = Drule.zero_var_indexes (trans RS red_if_equal); 
0  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*) 

33339  66 
fun add_rule rl (simp_rls, other_rls) = 
0  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).*) 

33339  71 
fun process_rules rls = fold_rev add_rule rls ([], []); 
0  72 

73 
(*Given list of rewrite rules, return list of both forms, reject others*) 

59164  74 
fun process_rewrites rls = 
0  75 
case process_rules rls of 
76 
(simp_rls,[]) => simp_rls 

59164  77 
 (_,others) => raise THM 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32957
diff
changeset

78 
("process_rewrites: Illformed rewrite", 0, others); 
0  79 

80 
(*Process the default rewrite rules*) 

81 
val simp_rls = process_rewrites default_rls; 

59164  82 
val simp_net = Tactic.build_net simp_rls; 
0  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.*) 

59164  89 
fun rewrite_res_tac ctxt = filt_resolve_from_net_tac ctxt 2 simp_net; 
0  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!). *) 

59164  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]); 

0  96 

97 
(*Resolve with asms, whether rewrites or not*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

98 
fun asm_res_tac ctxt asms = 
59164  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) 

0  102 
end; 
103 

104 
(*Single step for simple rewriting*) 

59164  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; 

0  108 

109 
(*Single step for conditional rewriting: prove_cond_tac handles new subgoals.*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

110 
fun cond_step_tac ctxt (prove_cond_tac, congr_rls, asms) = 
59164  111 
asm_res_tac ctxt asms ORELSE' rewrite_res_tac ctxt ORELSE' 
112 
(resolve_tac [trans, red_trans] THEN' prove_cond_tac) ORELSE' 

113 
subconv_res_tac ctxt congr_rls; 

0  114 

115 
(*Unconditional normalization tactic*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

116 
fun norm_tac ctxt arg = REPEAT_FIRST (step_tac ctxt arg) THEN 
0  117 
TRYALL (resolve_tac [red_if_equal]); 
118 

119 
(*Conditional normalization tactic*) 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
45659
diff
changeset

120 
fun cond_norm_tac ctxt arg = REPEAT_FIRST (cond_step_tac ctxt arg) THEN 
0  121 
TRYALL (resolve_tac [red_if_equal]); 
122 

123 
end; 

124 
end; 

125 