author  wenzelm 
Thu, 10 May 2007 18:10:32 +0200  
changeset 22926  fb6917e426da 
parent 22905  dab6a898b47c 
child 22937  08cf9aaf3aa1 
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 

22926  8 
infix 1 thenc; 
9 
infix 0 orelsec; 

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

10 

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 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

15 
val all_conv: conv 
22926  16 
val thenc: conv * conv > conv 
17 
val orelsec: conv * conv > conv 

18 
val first_conv: conv list > conv 

19 
val every_conv: conv list > conv 

20 
val tryc: conv > conv 

21 
val repeatc: conv > conv 

22 
val cache_conv: conv > conv 

23 
val abs_conv: conv > conv 

24 
val combination_conv: conv > conv > conv 

25 
val comb_conv: conv > conv 

26 
val arg_conv: conv > conv 

27 
val fun_conv: conv > conv 

28 
val arg1_conv: conv > conv 

29 
val fun2_conv: conv > conv 

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

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

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

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

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

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

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

36 

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

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

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

39 

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

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

41 

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

43 

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

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

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

46 

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

47 
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

48 

22926  49 
fun (cv1 thenc cv2) ct = 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

50 
let 
22926  51 
val eq1 = cv1 ct; 
52 
val eq2 = cv2 (Thm.rhs_of eq1); 

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

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

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

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

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

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

58 

22926  59 
fun (cv1 orelsec cv2) ct = 
60 
(case try cv1 ct of SOME eq => eq  NONE => cv2 ct); 

61 

62 
fun first_conv cvs = fold_rev (curry op orelsec) cvs no_conv; 

63 
fun every_conv cvs = fold_rev (curry op thenc) cvs all_conv; 

64 

65 
fun tryc cv = cv orelsec all_conv; 

66 
fun repeatc cv ct = tryc (cv thenc repeatc cv) ct; 

67 

68 
fun cache_conv cv = 

69 
let 

70 
val cache = ref Termtab.empty; 

71 
fun conv ct = 

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

73 
SOME th => th 

74 
 NONE => 

75 
let val th = cv ct 

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

77 
in conv end; 

78 

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

79 

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

80 

22926  81 
(** Pure conversions **) 
82 

83 
(* lambda terms *) 

84 

85 
fun abs_conv cv ct = 

86 
(case term_of ct of 

87 
Abs (x, _, _) => 

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

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

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

91 

92 
fun combination_conv cv1 cv2 ct = 

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

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

95 

96 
fun comb_conv cv = combination_conv cv cv; 

97 
fun arg_conv cv = combination_conv all_conv cv; 

98 
fun fun_conv cv = combination_conv cv all_conv; 

99 

100 
val arg1_conv = fun_conv o arg_conv; 

101 
val fun2_conv = fun_conv o fun_conv; 

102 

103 

104 
(* logic *) 

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

105 

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

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

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

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

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

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

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

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

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

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

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

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

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

119 

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

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

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

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

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

124 
NONE => cv ct 
22926  125 
 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

126 

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

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

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

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

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

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

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

136 
 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

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

138 

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

139 
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

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

141 

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

142 
end; 