author  chaieb 
Sat, 19 May 2007 18:19:45 +0200  
changeset 23034  b3a6815754d6 
parent 22937  08cf9aaf3aa1 
child 23169  37091da05d8e 
permissions  rwrr 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/conv.ML 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

3 
Author: Amine Chaieb and Makarius 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

4 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

5 
Conversions: primitive equality reasoning. 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

6 
*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

7 

22937  8 
infix 1 then_conv; 
9 
infix 0 else_conv; 

23034  10 
infix aconvc; 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

11 
signature CONV = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

12 
sig 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

13 
type conv = cterm > thm 
23034  14 
val aconvc : cterm * cterm > bool 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

15 
val no_conv: conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

16 
val all_conv: conv 
22937  17 
val then_conv: conv * conv > conv 
18 
val else_conv: conv * conv > conv 

22926  19 
val first_conv: conv list > conv 
20 
val every_conv: conv list > conv 

22937  21 
val try_conv: conv > conv 
22 
val repeat_conv: conv > conv 

22926  23 
val cache_conv: conv > conv 
24 
val abs_conv: conv > conv 

25 
val combination_conv: conv > conv > conv 

26 
val comb_conv: conv > conv 

27 
val arg_conv: conv > conv 

28 
val fun_conv: conv > conv 

29 
val arg1_conv: conv > conv 

30 
val fun2_conv: conv > conv 

23034  31 
val binop_conv: conv > conv 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

32 
val forall_conv: int > conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

33 
val concl_conv: int > conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

34 
val prems_conv: int > (int > conv) > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

35 
val goals_conv: (int > bool) > conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

36 
val fconv_rule: conv > thm > thm 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

37 
end; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

38 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

39 
structure Conv: CONV = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

40 
struct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

41 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

42 
(* conversionals *) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

43 

22926  44 
type conv = cterm > thm; 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

45 

23034  46 
fun s aconvc t = term_of s aconv term_of t; 
47 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

48 
fun no_conv _ = raise CTERM ("no conversion", []); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

49 
val all_conv = Thm.reflexive; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

50 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

51 
val is_refl = op aconv o Logic.dest_equals o Thm.prop_of; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

52 

22937  53 
fun (cv1 then_conv cv2) ct = 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

54 
let 
22926  55 
val eq1 = cv1 ct; 
56 
val eq2 = cv2 (Thm.rhs_of eq1); 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

57 
in 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

58 
if is_refl eq1 then eq2 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

59 
else if is_refl eq2 then eq1 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

60 
else Thm.transitive eq1 eq2 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

61 
end; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

62 

22937  63 
fun (cv1 else_conv cv2) ct = 
22926  64 
(case try cv1 ct of SOME eq => eq  NONE => cv2 ct); 
65 

22937  66 
fun first_conv cvs = fold_rev (curry op else_conv) cvs no_conv; 
67 
fun every_conv cvs = fold_rev (curry op then_conv) cvs all_conv; 

22926  68 

22937  69 
fun try_conv cv = cv else_conv all_conv; 
70 
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; 

22926  71 

72 
fun cache_conv cv = 

73 
let 

74 
val cache = ref Termtab.empty; 

75 
fun conv ct = 

76 
(case Termtab.lookup (! cache) (term_of ct) of 

77 
SOME th => th 

78 
 NONE => 

79 
let val th = cv ct 

80 
in change cache (Termtab.update (term_of ct, th)); th end); 

81 
in conv end; 

82 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

83 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

84 

22926  85 
(** Pure conversions **) 
86 

87 
(* lambda terms *) 

88 

89 
fun abs_conv cv ct = 

90 
(case term_of ct of 

91 
Abs (x, _, _) => 

92 
let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct 

93 
in Thm.abstract_rule x v (cv ct') end 

94 
 _ => raise CTERM ("abs_conv", [ct])); 

95 

96 
fun combination_conv cv1 cv2 ct = 

97 
let val (ct1, ct2) = Thm.dest_comb ct 

98 
in Thm.combination (cv1 ct1) (cv2 ct2) end; 

99 

100 
fun comb_conv cv = combination_conv cv cv; 

101 
fun arg_conv cv = combination_conv all_conv cv; 

102 
fun fun_conv cv = combination_conv cv all_conv; 

103 

104 
val arg1_conv = fun_conv o arg_conv; 

105 
val fun2_conv = fun_conv o fun_conv; 

106 

23034  107 
fun binop_conv cv = combination_conv (arg_conv cv) cv; 
22926  108 

109 
(* logic *) 

22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

110 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

111 
(*rewrite B in !!x1 ... xn. B*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

112 
fun forall_conv 0 cv ct = cv ct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

113 
 forall_conv n cv ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

114 
(case try Thm.dest_comb ct of 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

115 
NONE => cv ct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

116 
 SOME (A, B) => 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

117 
(case (term_of A, term_of B) of 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

118 
(Const ("all", _), Abs (x, _, _)) => 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

119 
let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in 
22926  120 
Thm.combination (all_conv A) 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

121 
(Thm.abstract_rule x v (forall_conv (n  1) cv B')) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

122 
end 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

123 
 _ => cv ct)); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

124 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

125 
(*rewrite B in A1 ==> ... ==> An ==> B*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

126 
fun concl_conv 0 cv ct = cv ct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

127 
 concl_conv n cv ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

128 
(case try Thm.dest_implies ct of 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

129 
NONE => cv ct 
22926  130 
 SOME (A, B) => Drule.imp_cong_rule (all_conv A) (concl_conv (n  1) cv B)); 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

131 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

132 
(*rewrite the A's in A1 ==> ... ==> An ==> B*) 
22926  133 
fun prems_conv 0 _ = all_conv 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

134 
 prems_conv n cv = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

135 
let 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

136 
fun conv i ct = 
22926  137 
if i = n + 1 then all_conv ct 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

138 
else 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

139 
(case try Thm.dest_implies ct of 
22926  140 
NONE => all_conv ct 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

141 
 SOME (A, B) => Drule.imp_cong_rule (cv i A) (conv (i + 1) B)); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

142 
in conv 1 end; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

143 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

144 
fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

145 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

146 

dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

147 
end; 