author  wenzelm 
Sun, 15 Apr 2007 14:31:53 +0200  
changeset 22695  17073e9b94f2 
parent 22682  92448396c9d9 
child 22907  dccd0763ae37 
permissions  rwrr 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/more_thm.ML 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

4 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

5 
Further operations on type thm, outside the inference kernel. 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

6 
*) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

7 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

8 
signature THM = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

9 
sig 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

10 
include THM 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

11 
val thm_ord: thm * thm > order 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

12 
val eq_thm: thm * thm > bool 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

13 
val eq_thms: thm list * thm list > bool 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

14 
val eq_thm_thy: thm * thm > bool 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

15 
val eq_thm_prop: thm * thm > bool 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

16 
val equiv_thm: thm * thm > bool 
22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

17 
val plain_prop_of: thm > term 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

18 
val fold_terms: (term > 'a > 'a) > thm > 'a > 'a 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

19 
val axiomK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

20 
val assumptionK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

21 
val definitionK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

22 
val theoremK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

23 
val lemmaK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

24 
val corollaryK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

25 
val internalK: string 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

26 
val rule_attribute: (Context.generic > thm > thm) > attribute 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

27 
val declaration_attribute: (thm > Context.generic > Context.generic) > attribute 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

28 
val theory_attributes: attribute list > theory * thm > theory * thm 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

29 
val proof_attributes: attribute list > Proof.context * thm > Proof.context * thm 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

30 
val no_attributes: 'a > 'a * 'b list 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

31 
val simple_fact: 'a > ('a * 'b list) list 
22682  32 
val read_def_cterms: 
33 
theory * (indexname > typ option) * (indexname > sort option) > 

34 
string list > bool > (string * typ)list 

35 
> cterm list * (indexname * typ)list 

36 
val read_cterm: theory > string * typ > cterm 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

37 
end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

38 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

39 
structure Thm: THM = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

40 
struct 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

41 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

42 
(** basic operations **) 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

43 

22682  44 
(* order: ignores theory context! *) 
45 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

46 
fun thm_ord (th1, th2) = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

47 
let 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

48 
val {shyps = shyps1, hyps = hyps1, tpairs = tpairs1, prop = prop1, ...} = Thm.rep_thm th1; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

49 
val {shyps = shyps2, hyps = hyps2, tpairs = tpairs2, prop = prop2, ...} = Thm.rep_thm th2; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

50 
in 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

51 
(case Term.fast_term_ord (prop1, prop2) of 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

52 
EQUAL => 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

53 
(case list_ord (prod_ord Term.fast_term_ord Term.fast_term_ord) (tpairs1, tpairs2) of 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

54 
EQUAL => 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

55 
(case list_ord Term.fast_term_ord (hyps1, hyps2) of 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

56 
EQUAL => list_ord Term.sort_ord (shyps1, shyps2) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

57 
 ord => ord) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

58 
 ord => ord) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

59 
 ord => ord) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

60 
end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

61 

22682  62 

63 
(* equality *) 

64 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

65 
fun eq_thm ths = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

66 
Context.joinable (pairself Thm.theory_of_thm ths) andalso 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

67 
thm_ord ths = EQUAL; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

68 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

69 
val eq_thms = eq_list eq_thm; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

70 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

71 
val eq_thm_thy = eq_thy o pairself Thm.theory_of_thm; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

72 
val eq_thm_prop = op aconv o pairself Thm.full_prop_of; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

73 

22682  74 

75 
(* pattern equivalence *) 

76 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

77 
fun equiv_thm ths = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

78 
Pattern.equiv (Theory.merge (pairself Thm.theory_of_thm ths)) (pairself Thm.full_prop_of ths); 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

79 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

80 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

81 
(* misc operations *) 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

82 

17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

83 
fun plain_prop_of raw_thm = 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

84 
let 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

85 
val thm = Thm.strip_shyps raw_thm; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

86 
fun err msg = raise THM ("plain_prop_of: " ^ msg, 0, [thm]); 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

87 
val {hyps, prop, tpairs, ...} = Thm.rep_thm thm; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

88 
in 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

89 
if not (null hyps) then 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

90 
err "theorem may not contain hypotheses" 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

91 
else if not (null (Thm.extra_shyps thm)) then 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

92 
err "theorem may not contain sort hypotheses" 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

93 
else if not (null tpairs) then 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

94 
err "theorem may not contain flexflex pairs" 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

95 
else prop 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

96 
end; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

97 

17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

98 
fun fold_terms f th = 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

99 
let val {tpairs, prop, hyps, ...} = Thm.rep_thm th 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

100 
in fold (fn (t, u) => f t #> f u) tpairs #> f prop #> fold f hyps end; 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

101 

17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

102 

22682  103 

104 
(** theorem kinds **) 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

105 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

106 
val axiomK = "axiom"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

107 
val assumptionK = "assumption"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

108 
val definitionK = "definition"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

109 
val theoremK = "theorem"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

110 
val lemmaK = "lemma"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

111 
val corollaryK = "corollary"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

112 
val internalK = "internal"; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

113 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

114 

22682  115 

116 
(** attributes **) 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

117 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

118 
fun rule_attribute f (x, th) = (x, f x th); 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

119 
fun declaration_attribute f (x, th) = (f th x, th); 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

120 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

121 
fun apply_attributes mk dest = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

122 
let 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

123 
fun app [] = I 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

124 
 app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) >> dest > app fs; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

125 
in app end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

126 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

127 
val theory_attributes = apply_attributes Context.Theory Context.the_theory; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

128 
val proof_attributes = apply_attributes Context.Proof Context.the_proof; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

129 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

130 
fun no_attributes x = (x, []); 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

131 
fun simple_fact x = [(x, [])]; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

132 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

133 

22682  134 
(** read/certify terms (obsolete) **) (*exception ERROR*) 
135 

136 
fun read_def_cterms (thy, types, sorts) used freeze sTs = 

137 
let 

138 
val (ts', tye) = Sign.read_def_terms (thy, types, sorts) used freeze sTs; 

139 
val cts = map (Thm.cterm_of thy) ts' 

140 
handle TYPE (msg, _, _) => error msg 

141 
 TERM (msg, _) => error msg; 

142 
in (cts, tye) end; 

143 

144 
fun read_cterm thy sT = 

145 
let val ([ct], _) = read_def_cterms (thy, K NONE, K NONE) [] true [sT] 

146 
in ct end; 

147 

148 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

149 
open Thm; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

150 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

151 
end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

152 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

153 
structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord); 