author  wenzelm 
Thu, 10 May 2007 00:39:51 +0200  
changeset 22905  dab6a898b47c 
child 22926  fb6917e426da 
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 

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

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

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

16 
val option_conv: conv > cterm > thm option 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

17 
val AND: conv * conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

18 
val OR: conv * conv > conv 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

25 

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

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

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

28 

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

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

30 

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

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

32 

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

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

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

35 

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

36 
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

37 

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

38 
fun option_conv conv ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

41 
 SOME eq => if is_refl eq then NONE else SOME eq); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

42 

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

43 
fun (conv1 AND conv2) ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

45 
val eq1 = conv1 ct; 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

46 
val eq2 = conv2 (Thm.rhs_of eq1); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

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

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

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

52 

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

53 
fun (conv1 OR conv2) ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

54 
(case try conv1 ct of SOME eq => eq  NONE => conv2 ct); 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

55 

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

56 

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

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

58 

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

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

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

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

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

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

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

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

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

67 
let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

68 
Thm.combination (Thm.reflexive A) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

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

72 

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

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

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

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

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

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

78 
 SOME (A, B) => Drule.imp_cong_rule (reflexive A) (concl_conv (n  1) cv B)); 
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 
(*rewrite the A's in A1 ==> ... ==> An ==> B*) 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

81 
fun prems_conv 0 _ = reflexive 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

84 
fun conv i ct = 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

85 
if i = n + 1 then reflexive ct 
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

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

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

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

89 
 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

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

91 

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

92 
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

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

94 

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

95 
end; 