author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24834  5684cbf8c895 
child 26130  03a7cfed5e9e 
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; 

23169  10 

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

14 
val all_conv: conv 
22937  15 
val then_conv: conv * conv > conv 
16 
val else_conv: conv * conv > conv 

22926  17 
val first_conv: conv list > conv 
18 
val every_conv: conv list > conv 

22937  19 
val try_conv: conv > conv 
20 
val repeat_conv: conv > conv 

24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

21 
val abs_conv: (Proof.context > conv) > Proof.context > conv 
22926  22 
val combination_conv: conv > conv > conv 
23 
val comb_conv: conv > conv 

24 
val arg_conv: conv > conv 

25 
val fun_conv: conv > conv 

26 
val arg1_conv: conv > conv 

27 
val fun2_conv: conv > conv 

23034  28 
val binop_conv: conv > conv 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

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

30 
val concl_conv: int > conv > conv 
23583
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

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

32 
val fconv_rule: conv > thm > thm 
23583
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

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

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

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

40 

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

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

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

43 

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

45 
let 
22926  46 
val eq1 = cv1 ct; 
47 
val eq2 = cv2 (Thm.rhs_of eq1); 

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

48 
in 
23596  49 
if Thm.is_reflexive eq1 then eq2 
50 
else if Thm.is_reflexive eq2 then eq1 

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

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

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

53 

22937  54 
fun (cv1 else_conv cv2) ct = 
23583
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

55 
(cv1 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

56 
handle THM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

57 
 CTERM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

58 
 TERM _ => cv2 ct 
00751df1f98c
else_conv: only handle THM  CTERM  TERM  TYPE;
wenzelm
parents:
23534
diff
changeset

59 
 TYPE _ => cv2 ct); 
22926  60 

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

22926  63 

22937  64 
fun try_conv cv = cv else_conv all_conv; 
65 
fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; 

22926  66 

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

67 

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

68 

22926  69 
(** Pure conversions **) 
70 

71 
(* lambda terms *) 

72 

24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

73 
fun abs_conv cv ctxt ct = 
23587  74 
(case Thm.term_of ct of 
22926  75 
Abs (x, _, _) => 
23596  76 
let 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

77 
val ([u], ctxt') = Variable.variant_fixes ["u"] ctxt; 
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

78 
val (v, ct') = Thm.dest_abs (SOME u) ct; 
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

79 
val eq = (cv ctxt') ct'; 
23596  80 
in if Thm.is_reflexive eq then all_conv ct else Thm.abstract_rule x v eq end 
22926  81 
 _ => raise CTERM ("abs_conv", [ct])); 
82 

83 
fun combination_conv cv1 cv2 ct = 

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

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

86 

87 
fun comb_conv cv = combination_conv cv cv; 

88 
fun arg_conv cv = combination_conv all_conv cv; 

89 
fun fun_conv cv = combination_conv cv all_conv; 

90 

91 
val arg1_conv = fun_conv o arg_conv; 

92 
val fun2_conv = fun_conv o fun_conv; 

93 

23034  94 
fun binop_conv cv = combination_conv (arg_conv cv) cv; 
22926  95 

23169  96 

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

98 

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

99 
(*rewrite B in !!x1 ... xn. B*) 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

100 
fun forall_conv n cv ctxt ct = 
23596  101 
if n <> 0 andalso can Logic.dest_all (Thm.term_of ct) 
24834
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

102 
then arg_conv (abs_conv (forall_conv (n  1) cv) ctxt) ct 
5684cbf8c895
abs_conv/forall_conv: proper context (avoid gensym);
wenzelm
parents:
23656
diff
changeset

103 
else cv ctxt ct; 
22905
dab6a898b47c
Conversions: primitive equality reasoning (from drule.ML);
wenzelm
parents:
diff
changeset

104 

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

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

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

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

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

109 
NONE => cv ct 
22926  110 
 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

111 

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

112 
(*rewrite the A's in A1 ==> ... ==> An ==> B*) 
23596  113 
fun prems_conv 0 _ ct = all_conv ct 
114 
 prems_conv n cv ct = 

115 
(case try Thm.dest_implies ct of 

116 
NONE => all_conv ct 

117 
 SOME (A, B) => Drule.imp_cong_rule (cv A) (prems_conv (n  1) cv B)); 

118 

119 

120 
(* conversions as rules *) 

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

121 

23596  122 
(*forward conversion, cf. FCONV_RULE in LCF*) 
123 
fun fconv_rule cv th = 

124 
let val eq = cv (Thm.cprop_of th) in 

125 
if Thm.is_reflexive eq then th 

126 
else Thm.equal_elim eq th 

127 
end; 

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

128 

23596  129 
(*goal conversion*) 
130 
fun gconv_rule cv i th = 

131 
(case try (Thm.cprem_of th) i of 

132 
SOME ct => 

133 
let val eq = cv ct in 

134 
if Thm.is_reflexive eq then th 

135 
else Drule.with_subgoal i (fconv_rule (arg1_conv (K eq))) th 

136 
end 

137 
 NONE => raise THM ("gconv_rule", i, [th])); 

23411
c524900454f3
Added eta_conv and etaexpansion conversion: waiting for it to be in thm.ML; exported is_refl
chaieb
parents:
23169
diff
changeset

138 

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

139 
end; 