author  wenzelm 
Thu, 27 Nov 1997 19:36:08 +0100  
changeset 4313  03353197410c 
parent 4285  05af145a61d4 
child 4440  9ed4098074bc 
permissions  rwrr 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

1 
(* Title: Pure/drule.ML 
0  2 
ID: $Id$ 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

3766  6 
Derived rules and other operations on theorems. 
0  7 
*) 
8 

11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

9 
infix 0 RS RSN RL RLN MRS MRL COMP; 
0  10 

11 
signature DRULE = 

3766  12 
sig 
4285  13 
val dest_implies : cterm > cterm * cterm 
14 
val skip_flexpairs : cterm > cterm 

15 
val strip_imp_prems : cterm > cterm list 

1460  16 
val cprems_of : thm > cterm list 
4285  17 
val read_insts : 
18 
Sign.sg > (indexname > typ option) * (indexname > sort option) 

19 
> (indexname > typ option) * (indexname > sort option) 

20 
> string list > (string*string)list 

21 
> (indexname*ctyp)list * (cterm*cterm)list 

22 
val types_sorts: thm > (indexname> typ option) * (indexname> sort option) 

1460  23 
val forall_intr_list : cterm list > thm > thm 
24 
val forall_intr_frees : thm > thm 

25 
val forall_intr_vars : thm > thm 

26 
val forall_elim_list : cterm list > thm > thm 

27 
val forall_elim_var : int > thm > thm 

28 
val forall_elim_vars : int > thm > thm 

29 
val implies_elim_list : thm > thm list > thm 

30 
val implies_intr_list : cterm list > thm > thm 

4285  31 
val zero_var_indexes : thm > thm 
32 
val standard : thm > thm 

33 
val assume_ax : theory > string > thm 

34 
val RSN : thm * (int * thm) > thm 

35 
val RS : thm * thm > thm 

36 
val RLN : thm list * (int * thm list) > thm list 

37 
val RL : thm list * thm list > thm list 

38 
val MRS : thm list * thm > thm 

1460  39 
val MRL : thm list list * thm list > thm list 
4285  40 
val compose : thm * int * thm > thm list 
41 
val COMP : thm * thm > thm 

0  42 
val read_instantiate_sg: Sign.sg > (string*string)list > thm > thm 
4285  43 
val read_instantiate : (string*string)list > thm > thm 
44 
val cterm_instantiate : (cterm*cterm)list > thm > thm 

45 
val weak_eq_thm : thm * thm > bool 

46 
val eq_thm_sg : thm * thm > bool 

47 
val size_of_thm : thm > int 

1460  48 
val reflexive_thm : thm 
4285  49 
val symmetric_thm : thm 
50 
val transitive_thm : thm 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

51 
val refl_implies : thm 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

52 
val rewrite_rule_aux : (meta_simpset > thm > thm option) > thm list > thm > thm 
3555  53 
val rewrite_thm : bool * bool > (meta_simpset > thm > thm option) 
54 
> meta_simpset > thm > thm 

4285  55 
val rewrite_goals_rule_aux: (meta_simpset > thm > thm option) > thm list > thm > thm 
56 
val rewrite_goal_rule : bool * bool > (meta_simpset > thm > thm option) 

57 
> meta_simpset > int > thm > thm 

58 

59 
val equal_abs_elim : cterm > thm > thm 

60 
val equal_abs_elim_list: cterm list > thm > thm 

61 
val flexpair_abs_elim_list: cterm list > thm > thm 

62 
val asm_rl : thm 

63 
val cut_rl : thm 

64 
val revcut_rl : thm 

65 
val thin_rl : thm 

66 
val triv_forall_equality: thm 

1756  67 
val swap_prems_rl : thm 
4285  68 
val equal_intr_rule : thm 
69 
val instantiate': ctyp option list > cterm option list > thm > thm 

3766  70 
end; 
0  71 

1499  72 
structure Drule : DRULE = 
0  73 
struct 
74 

3991  75 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

76 
(** some cterm>cterm operations: much faster than calling cterm_of! **) 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

77 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

78 
(** SAME NAMES as in structure Logic: use compound identifiers! **) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

79 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

80 
(*dest_implies for cterms. Note T=prop below*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

81 
fun dest_implies ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

82 
case term_of ct of 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

83 
(Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

84 
let val (ct1,ct2) = dest_comb ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

85 
in (#2 (dest_comb ct1), ct2) end 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

86 
 _ => raise TERM ("dest_implies", [term_of ct]) ; 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

87 

e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1596
diff
changeset

88 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

89 
(*Discard flexflex pairs; return a cterm*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

90 
fun skip_flexpairs ct = 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

91 
case term_of ct of 
1460  92 
(Const("==>", _) $ (Const("=?=",_)$_$_) $ _) => 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

93 
skip_flexpairs (#2 (dest_implies ct)) 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

94 
 _ => ct; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

95 

8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

96 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

97 
fun strip_imp_prems ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

98 
let val (cA,cB) = dest_implies ct 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

99 
in cA :: strip_imp_prems cB end 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

100 
handle TERM _ => []; 
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

101 

2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

102 
(* A1==>...An==>B goes to B, where B is not an implication *) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

103 
fun strip_imp_concl ct = 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

104 
case term_of ct of (Const("==>", _) $ _ $ _) => 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

105 
strip_imp_concl (#2 (dest_comb ct)) 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

106 
 _ => ct; 
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

107 

708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

108 
(*The premises of a theorem, as a cterm list*) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

109 
val cprems_of = strip_imp_prems o skip_flexpairs o cprop_of; 
708
8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

110 

8422e50adce0
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp
parents:
668
diff
changeset

111 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

112 
(** reading of instantiations **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

113 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

114 
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

115 
 _ => error("Lexical error in variable name " ^ quote (implode cs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

116 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

117 
fun absent ixn = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

118 
error("No such variable in term: " ^ Syntax.string_of_vname ixn); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

119 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

120 
fun inst_failure ixn = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

121 
error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

122 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

123 
(* this code is a bit of a mess. add_cterm could be simplified greatly if 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

124 
simultaneous instantiations were read or at least type checked 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

125 
simultaneously rather than one after the other. This would make the tricky 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

126 
composition of implicit type instantiations (parameter tye) superfluous. 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

127 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

128 
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

129 
let val {tsig,...} = Sign.rep_sg sign 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

130 
fun split([],tvs,vs) = (tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

131 
 split((sv,st)::l,tvs,vs) = (case explode sv of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

132 
"'"::cs => split(l,(indexname cs,st)::tvs,vs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

133 
 cs => split(l,tvs,(indexname cs,st)::vs)); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

134 
val (tvs,vs) = split(insts,[],[]); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

135 
fun readT((a,i),st) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

136 
let val ixn = ("'" ^ a,i); 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

137 
val S = case rsorts ixn of Some S => S  None => absent ixn; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

138 
val T = Sign.read_typ (sign,sorts) st; 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

139 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

140 
else inst_failure ixn 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

141 
end 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

142 
val tye = map readT tvs; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

143 
fun add_cterm ((cts,tye,used), (ixn,st)) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

144 
let val T = case rtypes ixn of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

145 
Some T => typ_subst_TVars tye T 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

146 
 None => absent ixn; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

147 
val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

148 
val cts' = (ixn,T,ct)::cts 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

149 
fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

150 
val used' = add_term_tvarnames(term_of ct,used); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

151 
in (map inst cts',tye2 @ tye,used') end 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

152 
val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs); 
952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

153 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

154 
map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms) 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

155 
end; 
4281
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

156 
*) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

157 

6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

158 
fun read_insts sign (rtypes,rsorts) (types,sorts) used insts = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

159 
let val {tsig,...} = Sign.rep_sg sign 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

160 
fun split([],tvs,vs) = (tvs,vs) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

161 
 split((sv,st)::l,tvs,vs) = (case explode sv of 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

162 
"'"::cs => split(l,(indexname cs,st)::tvs,vs) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

163 
 cs => split(l,tvs,(indexname cs,st)::vs)); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

164 
val (tvs,vs) = split(insts,[],[]); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

165 
fun readT((a,i),st) = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

166 
let val ixn = ("'" ^ a,i); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

167 
val S = case rsorts ixn of Some S => S  None => absent ixn; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

168 
val T = Sign.read_typ (sign,sorts) st; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

169 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

170 
else inst_failure ixn 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

171 
end 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

172 
val tye = map readT tvs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

173 
fun mkty(ixn,st) = (case rtypes ixn of 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

174 
Some T => (ixn,(st,typ_subst_TVars tye T)) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

175 
 None => absent ixn); 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

176 
val ixnsTs = map mkty vs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

177 
val ixns = map fst ixnsTs 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

178 
and sTs = map snd ixnsTs 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

179 
val (cts,tye2) = read_def_cterms(sign,types,sorts) used false sTs; 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

180 
fun mkcVar(ixn,T) = 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

181 
let val U = typ_subst_TVars tye2 T 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

182 
in cterm_of sign (Var(ixn,U)) end 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

183 
val ixnTs = ListPair.zip(ixns, map snd sTs) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

184 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) (tye2 @ tye), 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

185 
ListPair.zip(map mkcVar ixnTs,cts)) 
6c6073b13600
Added read_def_cterms for simultaneous reading/typing of terms under
nipkow
parents:
4270
diff
changeset

186 
end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

187 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

188 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

189 
(*** Find the type (sort) associated with a (T)Var or (T)Free in a term 
0  190 
Used for establishing default types (of variables) and sorts (of 
191 
type variables) when reading another term. 

192 
Index 1 indicates that a (T)Free rather than a (T)Var is wanted. 

193 
***) 

194 

195 
fun types_sorts thm = 

196 
let val {prop,hyps,...} = rep_thm thm; 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

197 
val big = list_comb(prop,hyps); (* bogus term! *) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

198 
val vars = map dest_Var (term_vars big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

199 
val frees = map dest_Free (term_frees big); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

200 
val tvars = term_tvars big; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

201 
val tfrees = term_tfrees big; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

202 
fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

203 
fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); 
0  204 
in (typ,sort) end; 
205 

206 
(** Standardization of rules **) 

207 

208 
(*Generalization over a list of variables, IGNORING bad ones*) 

209 
fun forall_intr_list [] th = th 

210 
 forall_intr_list (y::ys) th = 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

211 
let val gth = forall_intr_list ys th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

212 
in forall_intr y gth handle THM _ => gth end; 
0  213 

214 
(*Generalization over all suitable Free variables*) 

215 
fun forall_intr_frees th = 

216 
let val {prop,sign,...} = rep_thm th 

217 
in forall_intr_list 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

218 
(map (cterm_of sign) (sort atless (term_frees prop))) 
0  219 
th 
220 
end; 

221 

222 
(*Replace outermost quantified variable by Var of given index. 

223 
Could clash with Vars already present.*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

224 
fun forall_elim_var i th = 
0  225 
let val {prop,sign,...} = rep_thm th 
226 
in case prop of 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

227 
Const("all",_) $ Abs(a,T,_) => 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

228 
forall_elim (cterm_of sign (Var((a,i), T))) th 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

229 
 _ => raise THM("forall_elim_var", i, [th]) 
0  230 
end; 
231 

232 
(*Repeat forall_elim_var until all outer quantifiers are removed*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

233 
fun forall_elim_vars i th = 
0  234 
forall_elim_vars i (forall_elim_var i th) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

235 
handle THM _ => th; 
0  236 

237 
(*Specialization over a list of cterms*) 

238 
fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); 

239 

240 
(* maps [A1,...,An], B to [ A1;...;An ] ==> B *) 

241 
fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); 

242 

243 
(* maps [ A1;...;An ] ==> B and [A1,...,An] to B *) 

244 
fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths); 

245 

246 
(*Reset Var indexes to zero, renaming to preserve distinctness*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

247 
fun zero_var_indexes th = 
0  248 
let val {prop,sign,...} = rep_thm th; 
249 
val vars = term_vars prop 

250 
val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

251 
val inrs = add_term_tvars(prop,[]); 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

252 
val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); 
2266  253 
val tye = ListPair.map (fn ((v,rs),a) => (v, TVar((a,0),rs))) 
254 
(inrs, nms') 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

255 
val ctye = map (fn (v,T) => (v,ctyp_of sign T)) tye; 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

256 
fun varpairs([],[]) = [] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

257 
 varpairs((var as Var(v,T)) :: vars, b::bs) = 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

258 
let val T' = typ_subst_TVars tye T 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

259 
in (cterm_of sign (Var(v,T')), 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

260 
cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

261 
end 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

262 
 varpairs _ = raise TERM("varpairs", []); 
0  263 
in instantiate (ctye, varpairs(vars,rev bs)) th end; 
264 

265 

266 
(*Standard form of objectrule: no hypotheses, Frees, or outer quantifiers; 

267 
all generality expressed by Vars having index 0.*) 

268 
fun standard th = 

1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

269 
let val {maxidx,...} = rep_thm th 
1237  270 
in 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

271 
th > implies_intr_hyps 
1412  272 
> forall_intr_frees > forall_elim_vars (maxidx + 1) 
1439  273 
> Thm.strip_shyps > Thm.implies_intr_shyps 
1412  274 
> zero_var_indexes > Thm.varifyT > Thm.compress 
1218
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

275 
end; 
59ed8ef1a3a1
modified pretty_thm, standard, eq_thm to handle shyps;
wenzelm
parents:
1194
diff
changeset

276 

0  277 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

278 
(*Assume a new formula, read following the same conventions as axioms. 
0  279 
Generalizes over Free variables, 
280 
creates the assumption, and then strips quantifiers. 

281 
Example is [ ALL x:?A. ?P(x) ] ==> [ ?P(?a) ] 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

282 
[ !(A,P,a)[ ALL x:A. P(x) ] ==> [ P(a) ] ] *) 
0  283 
fun assume_ax thy sP = 
284 
let val sign = sign_of thy 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

285 
val prop = Logic.close_form (term_of (read_cterm sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

286 
(sP, propT))) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

287 
in forall_elim_vars 0 (assume (cterm_of sign prop)) end; 
0  288 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

289 
(*Resolution: exactly one resolvent must be produced.*) 
0  290 
fun tha RSN (i,thb) = 
4270  291 
case Seq.chop (2, biresolution false [(false,tha)] i thb) of 
0  292 
([th],_) => th 
293 
 ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) 

294 
 _ => raise THM("RSN: multiple unifiers", i, [tha,thb]); 

295 

296 
(*resolution: P==>Q, Q==>R gives P==>R. *) 

297 
fun tha RS thb = tha RSN (1,thb); 

298 

299 
(*For joining lists of rules*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

300 
fun thas RLN (i,thbs) = 
0  301 
let val resolve = biresolution false (map (pair false) thas) i 
4270  302 
fun resb thb = Seq.list_of (resolve thb) handle THM _ => [] 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2266
diff
changeset

303 
in List.concat (map resb thbs) end; 
0  304 

305 
fun thas RL thbs = thas RLN (1,thbs); 

306 

11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

307 
(*Resolve a list of rules against bottom_rl from right to left; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

308 
makes proof trees*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

309 
fun rls MRS bottom_rl = 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

310 
let fun rs_aux i [] = bottom_rl 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

311 
 rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls) 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

312 
in rs_aux 1 rls end; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

313 

d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

314 
(*As above, but for rule lists*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

315 
fun rlss MRL bottom_rls = 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

316 
let fun rs_aux i [] = bottom_rls 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

317 
 rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss) 
11
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

318 
in rs_aux 1 rlss end; 
d0e17c42dbb4
Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
lcp
parents:
0
diff
changeset

319 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

320 
(*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R 
0  321 
with no lifting or renaming! Q may contain ==> or metaquants 
322 
ALWAYS deletes premise i *) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

323 
fun compose(tha,i,thb) = 
4270  324 
Seq.list_of (bicompose false (false,tha,0) i thb); 
0  325 

326 
(*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) 

327 
fun tha COMP thb = 

328 
case compose(tha,1,thb) of 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

329 
[th] => th 
0  330 
 _ => raise THM("COMP", 1, [tha,thb]); 
331 

332 
(*Instantiate theorem th, reading instantiations under signature sg*) 

333 
fun read_instantiate_sg sg sinsts th = 

334 
let val ts = types_sorts th; 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

335 
val used = add_term_tvarnames(#prop(rep_thm th),[]); 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

336 
in instantiate (read_insts sg ts ts used sinsts) th end; 
0  337 

338 
(*Instantiate theorem th, reading instantiations under theory of th*) 

339 
fun read_instantiate sinsts th = 

340 
read_instantiate_sg (#sign (rep_thm th)) sinsts th; 

341 

342 

343 
(*Lefttoright replacements: tpairs = [...,(vi,ti),...]. 

344 
Instantiates distinct Vars by terms, inferring type instantiations. *) 

345 
local 

1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

346 
fun add_types ((ct,cu), (sign,tye,maxidx)) = 
2152  347 
let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct 
348 
and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu; 

349 
val maxi = Int.max(maxidx, Int.max(maxt, maxu)); 

0  350 
val sign' = Sign.merge(sign, Sign.merge(signt, signu)) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

351 
val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

352 
handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

353 
in (sign', tye', maxi') end; 
0  354 
in 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

355 
fun cterm_instantiate ctpairs0 th = 
1435
aefcd255ed4a
Removed bug in type unification. Negative indexes are not used any longer.
nipkow
parents:
1412
diff
changeset

356 
let val (sign,tye,_) = foldr add_types (ctpairs0, (#sign(rep_thm th),[],0)) 
0  357 
val tsig = #tsig(Sign.rep_sg sign); 
358 
fun instT(ct,cu) = let val inst = subst_TVars tye 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

359 
in (cterm_fun inst ct, cterm_fun inst cu) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

360 
fun ctyp2 (ix,T) = (ix, ctyp_of sign T) 
0  361 
in instantiate (map ctyp2 tye, map instT ctpairs0) th end 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

362 
handle TERM _ => 
0  363 
raise THM("cterm_instantiate: incompatible signatures",0,[th]) 
4057  364 
 TYPE (msg, _, _) => raise THM("cterm_instantiate: " ^ msg, 0, [th]) 
0  365 
end; 
366 

367 

4016  368 
(** theorem equality **) 
0  369 

370 
(*Do the two theorems have the same signature?*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

371 
fun eq_thm_sg (th1,th2) = Sign.eq_sg(#sign(rep_thm th1), #sign(rep_thm th2)); 
0  372 

373 
(*Useful "distance" function for BEST_FIRST*) 

374 
val size_of_thm = size_of_term o #prop o rep_thm; 

375 

376 

1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

377 
(** Mark Staples's weaker version of eq_thm: ignores variable renaming and 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

378 
(some) type variable renaming **) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

379 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

380 
(* Can't use term_vars, because it sorts the resulting list of variable names. 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

381 
We instead need the unique list noramlised by the order of appearance 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

382 
in the term. *) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

383 
fun term_vars' (t as Var(v,T)) = [t] 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

384 
 term_vars' (Abs(_,_,b)) = term_vars' b 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

385 
 term_vars' (f$a) = (term_vars' f) @ (term_vars' a) 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

386 
 term_vars' _ = []; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

387 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

388 
fun forall_intr_vars th = 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

389 
let val {prop,sign,...} = rep_thm th; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

390 
val vars = distinct (term_vars' prop); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

391 
in forall_intr_list (map (cterm_of sign) vars) th end; 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

392 

1237  393 
fun weak_eq_thm (tha,thb) = 
1194
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

394 
eq_thm(forall_intr_vars (freezeT tha), forall_intr_vars (freezeT thb)); 
563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

395 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

396 

563ecd14c1d8
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
lcp
parents:
952
diff
changeset

397 

0  398 
(*** MetaRewriting Rules ***) 
399 

4016  400 
fun store_thm name thm = PureThy.smart_store_thm (name, standard thm); 
401 

0  402 
val reflexive_thm = 
3991  403 
let val cx = cterm_of (sign_of ProtoPure.thy) (Var(("x",0),TVar(("'a",0),logicS))) 
4016  404 
in store_thm "reflexive" (Thm.reflexive cx) end; 
0  405 

406 
val symmetric_thm = 

3991  407 
let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT) 
4016  408 
in store_thm "symmetric" (Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; 
0  409 

410 
val transitive_thm = 

3991  411 
let val xy = read_cterm (sign_of ProtoPure.thy) ("x::'a::logic == y",propT) 
412 
val yz = read_cterm (sign_of ProtoPure.thy) ("y::'a::logic == z",propT) 

0  413 
val xythm = Thm.assume xy and yzthm = Thm.assume yz 
4016  414 
in store_thm "transitive" (Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; 
0  415 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

416 
(** Below, a "conversion" has type cterm > thm **) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

417 

3991  418 
val refl_implies = reflexive (cterm_of (sign_of ProtoPure.thy) implies); 
0  419 

420 
(*In [A1,...,An]==>B, rewrite the selected A's only  for rewrite_goals_tac*) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

421 
(*Do not rewrite flexflex pairs*) 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

422 
fun goals_conv pred cv = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

423 
let fun gconv i ct = 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

424 
let val (A,B) = dest_implies ct 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

425 
val (thA,j) = case term_of A of 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

426 
Const("=?=",_)$_$_ => (reflexive A, i) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

427 
 _ => (if pred i then cv A else reflexive A, i+1) 
2004
3411fe560611
New operations on cterms. Now same names as in Logic
paulson
parents:
1906
diff
changeset

428 
in combination (combination refl_implies thA) (gconv j B) end 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

429 
handle TERM _ => reflexive ct 
0  430 
in gconv 1 end; 
431 

432 
(*Use a conversion to transform a theorem*) 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

433 
fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th; 
0  434 

435 
(*rewriting conversion*) 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

436 
fun rew_conv mode prover mss = rewrite_cterm mode mss prover; 
0  437 

438 
(*Rewrite a theorem*) 

3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

439 
fun rewrite_rule_aux _ [] th = th 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

440 
 rewrite_rule_aux prover thms th = 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

441 
fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th; 
0  442 

3555  443 
fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss); 
444 

0  445 
(*Rewrite the subgoals of a proof state (represented by a theorem) *) 
3575
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

446 
fun rewrite_goals_rule_aux _ [] th = th 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

447 
 rewrite_goals_rule_aux prover thms th = 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

448 
fconv_rule (goals_conv (K true) (rew_conv (true, true) prover 
4e9beacb5339
improved rewrite_thm / rewrite_goals to handle conditional eqns;
wenzelm
parents:
3555
diff
changeset

449 
(Thm.mss_of thms))) th; 
0  450 

451 
(*Rewrite the subgoal of a proof state (represented by a theorem) *) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

452 
fun rewrite_goal_rule mode prover mss i thm = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

453 
if 0 < i andalso i <= nprems_of thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

454 
then fconv_rule (goals_conv (fn j => j=i) (rew_conv mode prover mss)) thm 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
211
diff
changeset

455 
else raise THM("rewrite_goal_rule",i,[thm]); 
0  456 

457 

458 
(** Derived rules mainly for METAHYPS **) 

459 

460 
(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) 

461 
fun equal_abs_elim ca eqth = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

462 
let val {sign=signa, t=a, ...} = rep_cterm ca 
0  463 
and combth = combination eqth (reflexive ca) 
464 
val {sign,prop,...} = rep_thm eqth 

465 
val (abst,absu) = Logic.dest_equals prop 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
214
diff
changeset

466 
val cterm = cterm_of (Sign.merge (sign,signa)) 
0  467 
in transitive (symmetric (beta_conversion (cterm (abst$a)))) 
468 
(transitive combth (beta_conversion (cterm (absu$a)))) 

469 
end 

470 
handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); 

471 

472 
(*Calling equal_abs_elim with multiple terms*) 

473 
fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); 

474 

475 
local 

476 
val alpha = TVar(("'a",0), []) (* type ?'a::{} *) 

477 
fun err th = raise THM("flexpair_inst: ", 0, [th]) 

478 
fun flexpair_inst def th = 

479 
let val {prop = Const _ $ t $ u, sign,...} = rep_thm th 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

480 
val cterm = cterm_of sign 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

481 
fun cvar a = cterm(Var((a,0),alpha)) 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

482 
val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] 
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

483 
def 
0  484 
in equal_elim def' th 
485 
end 

486 
handle THM _ => err th  bind => err th 

487 
in 

3991  488 
val flexpair_intr = flexpair_inst (symmetric ProtoPure.flexpair_def) 
489 
and flexpair_elim = flexpair_inst ProtoPure.flexpair_def 

0  490 
end; 
491 

492 
(*Version for flexflex pairs  this supports lifting.*) 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

493 
fun flexpair_abs_elim_list cts = 
0  494 
flexpair_intr o equal_abs_elim_list cts o flexpair_elim; 
495 

496 

497 
(*** Some useful metatheorems ***) 

498 

499 
(*The rule V/V, obtains assumption solving for eresolve_tac*) 

4016  500 
val asm_rl = 
501 
store_thm "asm_rl" (trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi",propT))); 

0  502 

503 
(*Metalevel cut rule: [ V==>W; V ] ==> W *) 

4016  504 
val cut_rl = 
505 
store_thm "cut_rl" 

506 
(trivial(read_cterm (sign_of ProtoPure.thy) ("PROP ?psi ==> PROP ?theta", propT))); 

0  507 

252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

508 
(*Generalized elim rule for one conclusion; cut_rl with reversed premises: 
0  509 
[ PROP V; PROP V ==> PROP W ] ==> PROP W *) 
510 
val revcut_rl = 

3991  511 
let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) 
512 
and VW = read_cterm (sign_of ProtoPure.thy) ("PROP V ==> PROP W", propT); 

4016  513 
in 
514 
store_thm "revcut_rl" 

515 
(implies_intr V (implies_intr VW (implies_elim (assume VW) (assume V)))) 

0  516 
end; 
517 

668  518 
(*for deleting an unwanted assumption*) 
519 
val thin_rl = 

3991  520 
let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) 
521 
and W = read_cterm (sign_of ProtoPure.thy) ("PROP W", propT); 

4016  522 
in store_thm "thin_rl" (implies_intr V (implies_intr W (assume W))) 
668  523 
end; 
524 

0  525 
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) 
526 
val triv_forall_equality = 

3991  527 
let val V = read_cterm (sign_of ProtoPure.thy) ("PROP V", propT) 
528 
and QV = read_cterm (sign_of ProtoPure.thy) ("!!x::'a. PROP V", propT) 

529 
and x = read_cterm (sign_of ProtoPure.thy) ("x", TFree("'a",logicS)); 

4016  530 
in 
531 
store_thm "triv_forall_equality" 

532 
(equal_intr (implies_intr QV (forall_elim x (assume QV))) 

533 
(implies_intr V (forall_intr x (assume V)))) 

0  534 
end; 
535 

1756  536 
(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==> 
537 
(PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi) 

538 
`thm COMP swap_prems_rl' swaps the first two premises of `thm' 

539 
*) 

540 
val swap_prems_rl = 

3991  541 
let val cmajor = read_cterm (sign_of ProtoPure.thy) 
1756  542 
("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT); 
543 
val major = assume cmajor; 

3991  544 
val cminor1 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiA", propT); 
1756  545 
val minor1 = assume cminor1; 
3991  546 
val cminor2 = read_cterm (sign_of ProtoPure.thy) ("PROP PhiB", propT); 
1756  547 
val minor2 = assume cminor2; 
4016  548 
in store_thm "swap_prems_rl" 
1756  549 
(implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1 
550 
(implies_elim (implies_elim major minor1) minor2)))) 

551 
end; 

552 

3653  553 
(* [ PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi ] 
554 
==> PROP ?phi == PROP ?psi 

555 
Introduction rule for == using ==> not metahyps. 

556 
*) 

557 
val equal_intr_rule = 

3991  558 
let val PQ = read_cterm (sign_of ProtoPure.thy) ("PROP phi ==> PROP psi", propT) 
559 
and QP = read_cterm (sign_of ProtoPure.thy) ("PROP psi ==> PROP phi", propT) 

4016  560 
in 
561 
store_thm "equal_intr_rule" 

562 
(implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP)))) 

3653  563 
end; 
564 

4285  565 

566 

567 
(** instantiate' rule **) 

568 

569 
(* collect vars *) 

570 

571 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs  (vs, _) => vs); 

572 
val add_tvars = foldl_types add_tvarsT; 

573 
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs  (vs, _) => vs); 

574 

575 
fun tvars_of thm = rev (add_tvars ([], #prop (Thm.rep_thm thm))); 

576 
fun vars_of thm = rev (add_vars ([], #prop (Thm.rep_thm thm))); 

577 

578 

579 
(* instantiate by lefttoright occurrence of variables *) 

580 

581 
fun instantiate' cTs cts thm = 

582 
let 

583 
fun err msg = 

584 
raise TYPE ("instantiate': " ^ msg, 

585 
mapfilter (apsome Thm.typ_of) cTs, 

586 
mapfilter (apsome Thm.term_of) cts); 

587 

588 
fun inst_of (v, ct) = 

589 
(Thm.cterm_of (#sign (Thm.rep_cterm ct)) (Var v), ct) 

590 
handle TYPE (msg, _, _) => err msg; 

591 

592 
fun zip_vars _ [] = [] 

593 
 zip_vars (_ :: vs) (None :: opt_ts) = zip_vars vs opt_ts 

594 
 zip_vars (v :: vs) (Some t :: opt_ts) = (v, t) :: zip_vars vs opt_ts 

595 
 zip_vars [] _ = err "more instantiations than variables in thm"; 

596 

597 
(*instantiate types first!*) 

598 
val thm' = 

599 
if forall is_none cTs then thm 

600 
else Thm.instantiate (zip_vars (map fst (tvars_of thm)) cTs, []) thm; 

601 
in 

602 
if forall is_none cts then thm' 

603 
else Thm.instantiate ([], map inst_of (zip_vars (vars_of thm') cts)) thm' 

604 
end; 

605 

606 

0  607 
end; 
252
7532f95d7f44
removed eq_sg, pprint_sg, print_sg (now in sign.ML);
wenzelm
parents:
229
diff
changeset

608 

1499  609 
open Drule; 