author  wenzelm 
Thu, 16 Jul 2009 20:32:40 +0200  
changeset 32019  827a8ebb3b2c 
parent 31977  e03059ae2d82 
child 32024  a5e7c8e60c85 
permissions  rwrr 
11519  1 
(* Title: Pure/proofterm.ML 
11540  2 
Author: Stefan Berghofer, TU Muenchen 
11519  3 

11540  4 
LF style proof terms. 
11519  5 
*) 
6 

11615  7 
infix 8 % %% %>; 
11519  8 

9 
signature BASIC_PROOFTERM = 

10 
sig 

11543
d61b913431c5
renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents:
11540
diff
changeset

11 
val proofs: int ref 
11519  12 

13 
datatype proof = 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

14 
MinProof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

15 
 PBound of int 
11519  16 
 Abst of string * typ option * proof 
17 
 AbsP of string * term option * proof 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

18 
 op % of proof * term option 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

19 
 op %% of proof * proof 
11519  20 
 Hyp of term 
21 
 PAxm of string * term * typ list option 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

22 
 OfClass of typ * class 
11519  23 
 Oracle of string * term * typ list option 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

24 
 Promise of serial * term * typ list 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

25 
 PThm of serial * ((string * term * typ list option) * proof_body future) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

26 
and proof_body = PBody of 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

27 
{oracles: (string * term) OrdList.T, 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

28 
thms: (serial * (string * term * proof_body future)) OrdList.T, 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

29 
proof: proof} 
11519  30 

11615  31 
val %> : proof * term > proof 
11519  32 
end; 
33 

34 
signature PROOFTERM = 

35 
sig 

36 
include BASIC_PROOFTERM 

37 

28815  38 
type oracle = string * term 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

39 
type pthm = serial * (string * term * proof_body future) 
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

40 
val join_body: proof_body future > 
28815  41 
{oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof} 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

42 
val join_proof: proof_body future > proof 
28815  43 
val proof_of: proof_body > proof 
30711  44 
val fold_proof_atoms: bool > (proof > 'a > 'a) > proof list > 'a > 'a 
28815  45 
val fold_body_thms: (string * term * proof_body > 'a > 'a) > proof_body list > 'a > 'a 
30712  46 
val status_of: proof_body list > {failed: bool, oracle: bool, unfinished: bool} 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

47 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

48 
val oracle_ord: oracle * oracle > order 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

49 
val thm_ord: pthm * pthm > order 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

50 
val merge_oracles: oracle OrdList.T > oracle OrdList.T > oracle OrdList.T 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

51 
val merge_thms: pthm OrdList.T > pthm OrdList.T > pthm OrdList.T 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

52 
val all_oracles_of: proof_body > oracle OrdList.T 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

53 
val approximate_proof_body: proof > proof_body 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

54 

11519  55 
(** primitive operations **) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

56 
val proof_combt: proof * term list > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

57 
val proof_combt': proof * term option list > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

58 
val proof_combP: proof * proof list > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

59 
val strip_combt: proof > proof * term option list 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

60 
val strip_combP: proof > proof * proof list 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

61 
val strip_thm: proof_body > proof_body 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

62 
val map_proof_terms_option: (term > term option) > (typ > typ option) > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

63 
val map_proof_terms: (term > term) > (typ > typ) > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

64 
val fold_proof_terms: (term > 'a > 'a) > (typ > 'a > 'a) > proof > 'a > 'a 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

65 
val maxidx_proof: proof > int > int 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

66 
val size_of_proof: proof > int 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

67 
val change_type: typ list option > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

68 
val prf_abstract_over: term > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

69 
val prf_incr_bv: int > int > int > int > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

70 
val incr_pboundvars: int > int > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

71 
val prf_loose_bvar1: proof > int > bool 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

72 
val prf_loose_Pbvar1: proof > int > bool 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

73 
val prf_add_loose_bnos: int > int > proof > int list * int list > int list * int list 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

74 
val norm_proof: Envir.env > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

75 
val norm_proof': Envir.env > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

76 
val prf_subst_bounds: term list > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

77 
val prf_subst_pbounds: proof list > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

78 
val freeze_thaw_prf: proof > proof * (proof > proof) 
11519  79 

80 
(** proof terms for specific inference rules **) 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

81 
val implies_intr_proof: term > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

82 
val forall_intr_proof: term > string > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

83 
val varify_proof: term > (string * sort) list > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

84 
val freezeT: term > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

85 
val rotate_proof: term list > term > int > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

86 
val permute_prems_prf: term list > int > int > proof > proof 
19908  87 
val generalize: string list * string list > int > proof > proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

88 
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list 
16880  89 
> proof > proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

90 
val lift_proof: term > int > term > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

91 
val assumption_proof: term list > term > int > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

92 
val bicompose_proof: bool > term list > term list > term list > term option > 
23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

93 
int > int > proof > proof > proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

94 
val equality_axms: (string * term) list 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

95 
val reflexive_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

96 
val symmetric_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

97 
val transitive_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

98 
val equal_intr_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

99 
val equal_elim_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

100 
val abstract_rule_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

101 
val combination_axm: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

102 
val reflexive: proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

103 
val symmetric: proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

104 
val transitive: term > typ > proof > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

105 
val abstract_rule: term > string > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

106 
val combination: term > term > term > term > typ > proof > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

107 
val equal_intr: term > term > proof > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

108 
val equal_elim: term > term > proof > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

109 
val axm_proof: string > term > proof 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

110 
val oracle_proof: string > term > oracle * proof 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

111 
val promise_proof: theory > serial > term > proof 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

112 
val fulfill_proof: theory > (serial * proof_body) list > proof_body > proof_body 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

113 
val thm_proof: theory > string > term list > term > 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

114 
(serial * proof_body future) list > proof_body > pthm * proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

115 
val get_name: term list > term > proof > string 
11519  116 

117 
(** rewriting on proof terms **) 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

118 
val add_prf_rrule: proof * proof > theory > theory 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

119 
val add_prf_rproc: (typ list > proof > proof option) > theory > theory 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

120 
val rewrite_proof: theory > (proof * proof) list * 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

121 
(typ list > proof > proof option) list > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

122 
val rewrite_proof_notypes: (proof * proof) list * 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

123 
(typ list > proof > proof option) list > proof > proof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

124 
val rew_proof: theory > proof > proof 
11519  125 
end 
126 

127 
structure Proofterm : PROOFTERM = 

128 
struct 

129 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

130 
(***** datatype proof *****) 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

131 

11519  132 
datatype proof = 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

133 
MinProof 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

134 
 PBound of int 
11519  135 
 Abst of string * typ option * proof 
136 
 AbsP of string * term option * proof 

12497  137 
 op % of proof * term option 
138 
 op %% of proof * proof 

11519  139 
 Hyp of term 
140 
 PAxm of string * term * typ list option 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

141 
 OfClass of typ * class 
11519  142 
 Oracle of string * term * typ list option 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

143 
 Promise of serial * term * typ list 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

144 
 PThm of serial * ((string * term * typ list option) * proof_body future) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

145 
and proof_body = PBody of 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

146 
{oracles: (string * term) OrdList.T, 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

147 
thms: (serial * (string * term * proof_body future)) OrdList.T, 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

148 
proof: proof}; 
11519  149 

28815  150 
type oracle = string * term; 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

151 
type pthm = serial * (string * term * proof_body future); 
28815  152 

29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

153 
val join_body = Future.join #> (fn PBody args => args); 
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

154 
val join_proof = #proof o join_body; 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

155 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

156 
fun proof_of (PBody {proof, ...}) = proof; 
17017  157 

158 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

159 
(***** proof atoms *****) 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

160 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

161 
fun fold_proof_atoms all f = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

162 
let 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

163 
fun app (Abst (_, _, prf)) = app prf 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

164 
 app (AbsP (_, _, prf)) = app prf 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

165 
 app (prf % _) = app prf 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

166 
 app (prf1 %% prf2) = app prf1 #> app prf2 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

167 
 app (prf as PThm (i, (_, body))) = (fn (x, seen) => 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

168 
if Inttab.defined seen i then (x, seen) 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

169 
else 
28815  170 
let val (x', seen') = 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

171 
(if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen) 
28815  172 
in (f prf x', seen') end) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

173 
 app prf = (fn (x, seen) => (f prf x, seen)); 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

174 
in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; 
19357
dade85a75c9f
Added alternative version of thms_of_proof that does not recursively
berghofe
parents:
19304
diff
changeset

175 

30711  176 
fun fold_body_thms f = 
177 
let 

178 
fun app (PBody {thms, ...}) = thms > fold (fn (i, (name, prop, body)) => fn (x, seen) => 

179 
if Inttab.defined seen i then (x, seen) 

180 
else 

181 
let 

182 
val body' = Future.join body; 

183 
val (x', seen') = app body' (x, Inttab.update (i, ()) seen); 

184 
in (f (name, prop, body') x', seen') end); 

185 
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; 

186 

30712  187 
fun status_of bodies = 
30711  188 
let 
189 
fun status (PBody {oracles, thms, ...}) x = 

190 
let 

191 
val ((oracle, unfinished, failed), seen) = 

192 
(thms, x) > fold (fn (i, (_, _, body)) => fn (st, seen) => 

193 
if Inttab.defined seen i then (st, seen) 

194 
else 

195 
let val seen' = Inttab.update (i, ()) seen in 

196 
(case Future.peek body of 

197 
SOME (Exn.Result body') => status body' (st, seen') 

198 
 SOME (Exn.Exn _) => 

199 
let val (oracle, unfinished, _) = st 

200 
in ((oracle, unfinished, true), seen') end 

201 
 NONE => 

202 
let val (oracle, _, failed) = st 

203 
in ((oracle, true, failed), seen') end) 

204 
end); 

205 
in ((oracle orelse not (null oracles), unfinished, failed), seen) end; 

30712  206 
val (oracle, unfinished, failed) = #1 (fold status bodies ((false, false, false), Inttab.empty)); 
30711  207 
in {oracle = oracle, unfinished = unfinished, failed = failed} end; 
208 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

209 

28815  210 
(* proof body *) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

211 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

212 
val oracle_ord = prod_ord fast_string_ord TermOrd.fast_term_ord; 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

213 
fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i); 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

214 

30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

215 
val merge_oracles = OrdList.union oracle_ord; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

216 
val merge_thms = OrdList.union thm_ord; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

217 

2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

218 
val all_oracles_of = 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

219 
let 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

220 
fun collect (PBody {oracles, thms, ...}) = thms > fold (fn (i, (_, _, body)) => fn (x, seen) => 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

221 
if Inttab.defined seen i then (x, seen) 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

222 
else 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

223 
let 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

224 
val body' = Future.join body; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

225 
val (x', seen') = collect body' (x, Inttab.update (i, ()) seen); 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

226 
in (merge_oracles oracles x', seen') end); 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

227 
in fn body => #1 (collect body ([], Inttab.empty)) end; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

228 

2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

229 
fun approximate_proof_body prf = 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

230 
let 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

231 
val (oracles, thms) = fold_proof_atoms false 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

232 
(fn Oracle (s, prop, _) => apfst (cons (s, prop)) 
28815  233 
 PThm (i, ((name, prop, _), body)) => apsnd (cons (i, (name, prop, body))) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

234 
 _ => I) [prf] ([], []); 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

235 
in 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

236 
PBody 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

237 
{oracles = OrdList.make oracle_ord oracles, 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

238 
thms = OrdList.make thm_ord thms, 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

239 
proof = prf} 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

240 
end; 
11519  241 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

242 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

243 
(***** proof objects with different levels of detail *****) 
11519  244 

15531  245 
fun (prf %> t) = prf % SOME t; 
11519  246 

15570  247 
val proof_combt = Library.foldl (op %>); 
248 
val proof_combt' = Library.foldl (op %); 

249 
val proof_combP = Library.foldl (op %%); 

11519  250 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

251 
fun strip_combt prf = 
11615  252 
let fun stripc (prf % t, ts) = stripc (prf, t::ts) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

253 
 stripc x = x 
11519  254 
in stripc (prf, []) end; 
255 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

256 
fun strip_combP prf = 
11615  257 
let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) 
11519  258 
 stripc x = x 
259 
in stripc (prf, []) end; 

260 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

261 
fun strip_thm (body as PBody {proof, ...}) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

262 
(case strip_combt (fst (strip_combP proof)) of 
29635
31d14e9fa0da
proof_body: turned lazy into future  ensures that body is fulfilled eventually, without explicit force;
wenzelm
parents:
29270
diff
changeset

263 
(PThm (_, (_, body')), _) => Future.join body' 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

264 
 _ => body); 
11519  265 

23178  266 
val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf)); 
15531  267 
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf; 
11519  268 

32019  269 
fun apsome f NONE = raise Same.SAME 
270 
 apsome f (SOME x) = (case f x of NONE => raise Same.SAME  some => some); 

20000  271 

32019  272 
fun apsome' f NONE = raise Same.SAME 
15531  273 
 apsome' f (SOME x) = SOME (f x); 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

274 

20000  275 
fun map_proof_terms_option f g = 
276 
let 

277 
fun map_typs (T :: Ts) = 

278 
(case g T of 

279 
NONE => T :: map_typs Ts 

32019  280 
 SOME T' => T' :: (map_typs Ts handle Same.SAME => Ts)) 
281 
 map_typs [] = raise Same.SAME; 

20000  282 

283 
fun mapp (Abst (s, T, prf)) = (Abst (s, apsome g T, mapph prf) 

32019  284 
handle Same.SAME => Abst (s, T, mapp prf)) 
20000  285 
 mapp (AbsP (s, t, prf)) = (AbsP (s, apsome f t, mapph prf) 
32019  286 
handle Same.SAME => AbsP (s, t, mapp prf)) 
287 
 mapp (prf % t) = (mapp prf % (apsome f t handle Same.SAME => t) 

288 
handle Same.SAME => prf % apsome f t) 

20000  289 
 mapp (prf1 %% prf2) = (mapp prf1 %% mapph prf2 
32019  290 
handle Same.SAME => prf1 %% mapp prf2) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

291 
 mapp (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (map_typs Ts)) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

292 
 mapp (OfClass (T, c)) = OfClass (apsome g (SOME T) > the, c) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

293 
 mapp (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (map_typs Ts)) 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

294 
 mapp (Promise (i, prop, Ts)) = Promise (i, prop, map_typs Ts) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

295 
 mapp (PThm (i, ((a, prop, SOME Ts), body))) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

296 
PThm (i, ((a, prop, SOME (map_typs Ts)), body)) 
32019  297 
 mapp _ = raise Same.SAME 
298 
and mapph prf = (mapp prf handle Same.SAME => prf) 

20000  299 

300 
in mapph end; 

301 

22662  302 
fun same eq f x = 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

303 
let val x' = f x 
32019  304 
in if eq (x, x') then raise Same.SAME else x' end; 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

305 

592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

306 
fun map_proof_terms f g = 
20000  307 
map_proof_terms_option 
32019  308 
(fn t => SOME (same (op =) f t) handle Same.SAME => NONE) 
309 
(fn T => SOME (same (op =) g T) handle Same.SAME => NONE); 

11519  310 

20147  311 
fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf 
312 
 fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf 

313 
 fold_proof_terms f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f g prf 

314 
 fold_proof_terms f g (AbsP (_, NONE, prf)) = fold_proof_terms f g prf 

315 
 fold_proof_terms f g (prf % SOME t) = fold_proof_terms f g prf #> f t 

316 
 fold_proof_terms f g (prf % NONE) = fold_proof_terms f g prf 

317 
 fold_proof_terms f g (prf1 %% prf2) = 

318 
fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 

20159  319 
 fold_proof_terms _ g (PAxm (_, _, SOME Ts)) = fold g Ts 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

320 
 fold_proof_terms _ g (OfClass (T, _)) = g T 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

321 
 fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

322 
 fold_proof_terms _ g (Promise (_, _, Ts)) = fold g Ts 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

323 
 fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts 
20147  324 
 fold_proof_terms _ _ _ = I; 
11519  325 

20300  326 
fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf; 
12868  327 

13744  328 
fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf 
13749  329 
 size_of_proof (AbsP (_, t, prf)) = 1 + size_of_proof prf 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

330 
 size_of_proof (prf % _) = 1 + size_of_proof prf 
13744  331 
 size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 
332 
 size_of_proof _ = 1; 

333 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

334 
fun change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

335 
 change_type (SOME [T]) (OfClass (_, c)) = OfClass (T, c) 
12907
27e6d344d724
New function change_type for changing type assignments of theorems,
berghofe
parents:
12890
diff
changeset

336 
 change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

337 
 change_type opTs (Promise _) = error "change_type: unexpected promise" 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

338 
 change_type opTs (PThm (i, ((name, prop, _), body))) = PThm (i, ((name, prop, opTs), body)) 
12907
27e6d344d724
New function change_type for changing type assignments of theorems,
berghofe
parents:
12890
diff
changeset

339 
 change_type _ prf = prf; 
27e6d344d724
New function change_type for changing type assignments of theorems,
berghofe
parents:
12890
diff
changeset

340 

11519  341 

342 
(***** utilities *****) 

343 

344 
fun strip_abs (_::Ts) (Abs (_, _, t)) = strip_abs Ts t 

345 
 strip_abs _ t = t; 

346 

15570  347 
fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts); 
11519  348 

349 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

350 
(*Abstraction of a proof term over its occurrences of v, 
11519  351 
which must contain no loose bound variables. 
352 
The resulting proof term is ready to become the body of an Abst.*) 

353 

354 
fun prf_abstract_over v = 

355 
let 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

356 
fun abst' lev u = if v aconv u then Bound lev else 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

357 
(case u of 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

358 
Abs (a, T, t) => Abs (a, T, abst' (lev + 1) t) 
32019  359 
 f $ t => (abst' lev f $ absth' lev t handle Same.SAME => f $ abst' lev t) 
360 
 _ => raise Same.SAME) 

361 
and absth' lev t = (abst' lev t handle Same.SAME => t); 

11519  362 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

363 
fun abst lev (AbsP (a, t, prf)) = 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

364 
(AbsP (a, apsome' (abst' lev) t, absth lev prf) 
32019  365 
handle Same.SAME => AbsP (a, t, abst lev prf)) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

366 
 abst lev (Abst (a, T, prf)) = Abst (a, T, abst (lev + 1) prf) 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

367 
 abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 
32019  368 
handle Same.SAME => prf1 %% abst lev prf2) 
15570  369 
 abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t 
32019  370 
handle Same.SAME => prf % apsome' (abst' lev) t) 
371 
 abst _ _ = raise Same.SAME 

372 
and absth lev prf = (abst lev prf handle Same.SAME => prf) 

11519  373 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

374 
in absth 0 end; 
11519  375 

376 

377 
(*increments a proof term's nonlocal bound variables 

378 
required when moving a proof term within abstractions 

379 
inc is increment for bound variables 

380 
lev is level at which a bound variable is considered 'loose'*) 

381 

382 
fun incr_bv' inct tlev t = incr_bv (inct, tlev, t); 

383 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

384 
fun prf_incr_bv' incP inct Plev tlev (PBound i) = 
32019  385 
if i >= Plev then PBound (i+incP) else raise Same.SAME 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

386 
 prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) = 
22662  387 
(AbsP (a, apsome' (same (op =) (incr_bv' inct tlev)) t, 
32019  388 
prf_incr_bv incP inct (Plev+1) tlev body) handle Same.SAME => 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

389 
AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body)) 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

390 
 prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) = 
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

391 
Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

392 
 prf_incr_bv' incP inct Plev tlev (prf %% prf') = 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

393 
(prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf' 
32019  394 
handle Same.SAME => prf %% prf_incr_bv' incP inct Plev tlev prf') 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

395 
 prf_incr_bv' incP inct Plev tlev (prf % t) = 
15570  396 
(prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t 
32019  397 
handle Same.SAME => prf % apsome' (same (op =) (incr_bv' inct tlev)) t) 
398 
 prf_incr_bv' _ _ _ _ _ = raise Same.SAME 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

399 
and prf_incr_bv incP inct Plev tlev prf = 
32019  400 
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); 
11519  401 

402 
fun incr_pboundvars 0 0 prf = prf 

403 
 incr_pboundvars incP inct prf = prf_incr_bv incP inct 0 0 prf; 

404 

405 

11615  406 
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k 
15531  407 
 prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) 
408 
 prf_loose_bvar1 (_ % NONE) _ = true 

409 
 prf_loose_bvar1 (AbsP (_, SOME t, prf)) k = loose_bvar1 (t, k) orelse prf_loose_bvar1 prf k 

410 
 prf_loose_bvar1 (AbsP (_, NONE, _)) k = true 

11519  411 
 prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) 
412 
 prf_loose_bvar1 _ _ = false; 

413 

414 
fun prf_loose_Pbvar1 (PBound i) k = i = k 

11615  415 
 prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k 
416 
 prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k 

11519  417 
 prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) 
418 
 prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k 

419 
 prf_loose_Pbvar1 _ _ = false; 

420 

12279  421 
fun prf_add_loose_bnos plev tlev (PBound i) (is, js) = 
17492  422 
if i < plev then (is, js) else (insert (op =) (iplev) is, js) 
12279  423 
 prf_add_loose_bnos plev tlev (prf1 %% prf2) p = 
424 
prf_add_loose_bnos plev tlev prf2 

425 
(prf_add_loose_bnos plev tlev prf1 p) 

426 
 prf_add_loose_bnos plev tlev (prf % opt) (is, js) = 

427 
prf_add_loose_bnos plev tlev prf (case opt of 

17492  428 
NONE => (is, insert (op =) ~1 js) 
15531  429 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  430 
 prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = 
431 
prf_add_loose_bnos (plev+1) tlev prf (case opt of 

17492  432 
NONE => (is, insert (op =) ~1 js) 
15531  433 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  434 
 prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = 
435 
prf_add_loose_bnos plev (tlev+1) prf p 

436 
 prf_add_loose_bnos _ _ _ _ = ([], []); 

437 

11519  438 

439 
(**** substitutions ****) 

440 

31977  441 
fun del_conflicting_tvars envT T = Term_Subst.instantiateT 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19357
diff
changeset

442 
(map_filter (fn ixnS as (_, S) => 
26328  443 
(Type.lookup envT ixnS; NONE) handle TYPE _ => 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

444 
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

445 

31977  446 
fun del_conflicting_vars env t = Term_Subst.instantiate 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19357
diff
changeset

447 
(map_filter (fn ixnS as (_, S) => 
32019  448 
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ => 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

449 
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t), 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19357
diff
changeset

450 
map_filter (fn Var (ixnT as (_, T)) => 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

451 
(Envir.lookup (env, ixnT); NONE) handle TYPE _ => 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
29261
diff
changeset

452 
SOME (ixnT, Free ("dummy", T))) (OldTerm.term_vars t)) t; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

453 

11519  454 
fun norm_proof env = 
455 
let 

32019  456 
val envT = Envir.type_env env; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

457 
fun msg s = warning ("type conflict in norm_proof:\n" ^ s); 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

458 
fun htype f t = f env t handle TYPE (s, _, _) => 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

459 
(msg s; f env (del_conflicting_vars env t)); 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

460 
fun htypeT f T = f envT T handle TYPE (s, _, _) => 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

461 
(msg s; f envT (del_conflicting_tvars envT T)); 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

462 
fun htypeTs f Ts = f envT Ts handle TYPE (s, _, _) => 
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

463 
(msg s; f envT (map (del_conflicting_tvars envT) Ts)); 
32019  464 
fun norm (Abst (s, T, prf)) = 
465 
(Abst (s, apsome' (htypeT Envir.norm_type_same) T, Same.commit norm prf) 

466 
handle Same.SAME => Abst (s, T, norm prf)) 

467 
 norm (AbsP (s, t, prf)) = 

468 
(AbsP (s, apsome' (htype Envir.norm_term_same) t, Same.commit norm prf) 

469 
handle Same.SAME => AbsP (s, t, norm prf)) 

470 
 norm (prf % t) = 

471 
(norm prf % Option.map (htype Envir.norm_term) t 

472 
handle Same.SAME => prf % apsome' (htype Envir.norm_term_same) t) 

473 
 norm (prf1 %% prf2) = 

474 
(norm prf1 %% Same.commit norm prf2 

475 
handle Same.SAME => prf1 %% norm prf2) 

476 
 norm (PAxm (s, prop, Ts)) = 

477 
PAxm (s, prop, apsome' (htypeTs Envir.norm_types_same) Ts) 

478 
 norm (OfClass (T, c)) = 

479 
OfClass (htypeT Envir.norm_type_same T, c) 

480 
 norm (Oracle (s, prop, Ts)) = 

481 
Oracle (s, prop, apsome' (htypeTs Envir.norm_types_same) Ts) 

482 
 norm (Promise (i, prop, Ts)) = 

483 
Promise (i, prop, htypeTs Envir.norm_types_same Ts) 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

484 
 norm (PThm (i, ((s, t, Ts), body))) = 
32019  485 
PThm (i, ((s, t, apsome' (htypeTs Envir.norm_types_same) Ts), body)) 
486 
 norm _ = raise Same.SAME; 

487 
in Same.commit norm end; 

11519  488 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

489 

11519  490 
(***** Remove some types in proof term (to save space) *****) 
491 

492 
fun remove_types (Abs (s, _, t)) = Abs (s, dummyT, remove_types t) 

493 
 remove_types (t $ u) = remove_types t $ remove_types u 

494 
 remove_types (Const (s, _)) = Const (s, dummyT) 

495 
 remove_types t = t; 

496 

497 
fun remove_types_env (Envir.Envir {iTs, asol, maxidx}) = 

15797  498 
Envir.Envir {iTs = iTs, asol = Vartab.map (apsnd remove_types) asol, 
499 
maxidx = maxidx}; 

11519  500 

501 
fun norm_proof' env prf = norm_proof (remove_types_env env) prf; 

502 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

503 

11519  504 
(**** substitution of bound variables ****) 
505 

506 
fun prf_subst_bounds args prf = 

507 
let 

508 
val n = length args; 

509 
fun subst' lev (Bound i) = 

32019  510 
(if i<lev then raise Same.SAME (*var is locally bound*) 
30146  511 
else incr_boundvars lev (nth args (ilev)) 
512 
handle Subscript => Bound (in)) (*loose: change it*) 

11519  513 
 subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) 
514 
 subst' lev (f $ t) = (subst' lev f $ substh' lev t 

32019  515 
handle Same.SAME => f $ subst' lev t) 
516 
 subst' _ _ = raise Same.SAME 

517 
and substh' lev t = (subst' lev t handle Same.SAME => t); 

11519  518 

519 
fun subst lev (AbsP (a, t, body)) = (AbsP (a, apsome' (subst' lev) t, substh lev body) 

32019  520 
handle Same.SAME => AbsP (a, t, subst lev body)) 
11519  521 
 subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) 
11615  522 
 subst lev (prf %% prf') = (subst lev prf %% substh lev prf' 
32019  523 
handle Same.SAME => prf %% subst lev prf') 
15570  524 
 subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t 
32019  525 
handle Same.SAME => prf % apsome' (subst' lev) t) 
526 
 subst _ _ = raise Same.SAME 

527 
and substh lev prf = (subst lev prf handle Same.SAME => prf) 

11519  528 
in case args of [] => prf  _ => substh 0 prf end; 
529 

530 
fun prf_subst_pbounds args prf = 

531 
let 

532 
val n = length args; 

533 
fun subst (PBound i) Plev tlev = 

32019  534 
(if i < Plev then raise Same.SAME (*var is locally bound*) 
30146  535 
else incr_pboundvars Plev tlev (nth args (iPlev)) 
11519  536 
handle Subscript => PBound (in) (*loose: change it*)) 
537 
 subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) 

538 
 subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) 

11615  539 
 subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev 
32019  540 
handle Same.SAME => prf %% subst prf' Plev tlev) 
11615  541 
 subst (prf % t) Plev tlev = subst prf Plev tlev % t 
32019  542 
 subst prf _ _ = raise Same.SAME 
543 
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) 

11519  544 
in case args of [] => prf  _ => substh prf 0 0 end; 
545 

546 

547 
(**** Freezing and thawing of variables in proof terms ****) 

548 

549 
fun frzT names = 

17325  550 
map_type_tvar (fn (ixn, xs) => TFree ((the o AList.lookup (op =) names) ixn, xs)); 
11519  551 

552 
fun thawT names = 

17325  553 
map_type_tfree (fn (s, xs) => case AList.lookup (op =) names s of 
15531  554 
NONE => TFree (s, xs) 
555 
 SOME ixn => TVar (ixn, xs)); 

11519  556 

557 
fun freeze names names' (t $ u) = 

558 
freeze names names' t $ freeze names names' u 

559 
 freeze names names' (Abs (s, T, t)) = 

560 
Abs (s, frzT names' T, freeze names names' t) 

561 
 freeze names names' (Const (s, T)) = Const (s, frzT names' T) 

562 
 freeze names names' (Free (s, T)) = Free (s, frzT names' T) 

563 
 freeze names names' (Var (ixn, T)) = 

17325  564 
Free ((the o AList.lookup (op =) names) ixn, frzT names' T) 
11519  565 
 freeze names names' t = t; 
566 

567 
fun thaw names names' (t $ u) = 

568 
thaw names names' t $ thaw names names' u 

569 
 thaw names names' (Abs (s, T, t)) = 

570 
Abs (s, thawT names' T, thaw names names' t) 

571 
 thaw names names' (Const (s, T)) = Const (s, thawT names' T) 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

572 
 thaw names names' (Free (s, T)) = 
11519  573 
let val T' = thawT names' T 
17325  574 
in case AList.lookup (op =) names s of 
15531  575 
NONE => Free (s, T') 
576 
 SOME ixn => Var (ixn, T') 

11519  577 
end 
578 
 thaw names names' (Var (ixn, T)) = Var (ixn, thawT names' T) 

579 
 thaw names names' t = t; 

580 

581 
fun freeze_thaw_prf prf = 

582 
let 

583 
val (fs, Tfs, vs, Tvs) = fold_proof_terms 

20147  584 
(fn t => fn (fs, Tfs, vs, Tvs) => 
29261  585 
(Term.add_free_names t fs, Term.add_tfree_names t Tfs, 
586 
Term.add_var_names t vs, Term.add_tvar_names t Tvs)) 

20147  587 
(fn T => fn (fs, Tfs, vs, Tvs) => 
29261  588 
(fs, Term.add_tfree_namesT T Tfs, 
589 
vs, Term.add_tvar_namesT T Tvs)) 

20147  590 
prf ([], [], [], []); 
29261  591 
val names = vs ~~ Name.variant_list fs (map fst vs); 
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20000
diff
changeset

592 
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); 
11519  593 
val rnames = map swap names; 
594 
val rnames' = map swap names'; 

595 
in 

596 
(map_proof_terms (freeze names names') (frzT names') prf, 

597 
map_proof_terms (thaw rnames rnames') (thawT rnames')) 

598 
end; 

599 

600 

601 
(***** implication introduction *****) 

602 

603 
fun implies_intr_proof h prf = 

604 
let 

32019  605 
fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME 
11519  606 
 abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) 
607 
 abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i+1) prf) 

11615  608 
 abshyp i (prf % t) = abshyp i prf % t 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

609 
 abshyp i (prf1 %% prf2) = (abshyp i prf1 %% abshyph i prf2 
32019  610 
handle Same.SAME => prf1 %% abshyp i prf2) 
611 
 abshyp _ _ = raise Same.SAME 

612 
and abshyph i prf = (abshyp i prf handle Same.SAME => prf) 

11519  613 
in 
15531  614 
AbsP ("H", NONE (*h*), abshyph 0 prf) 
11519  615 
end; 
616 

617 

618 
(***** forall introduction *****) 

619 

15531  620 
fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf); 
11519  621 

622 

623 
(***** varify *****) 

624 

625 
fun varify_proof t fixed prf = 

626 
let 

19304  627 
val fs = Term.fold_types (Term.fold_atyps 
628 
(fn TFree v => if member (op =) fixed v then I else insert (op =) v  _ => I)) t []; 

29261  629 
val used = Name.context 
630 
> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a  _ => I)) t; 

631 
val fmap = fs ~~ (#1 (Name.variants (map fst fs) used)); 

11519  632 
fun thaw (f as (a, S)) = 
17314  633 
(case AList.lookup (op =) fmap f of 
15531  634 
NONE => TFree f 
635 
 SOME b => TVar ((b, 0), S)); 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

636 
in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; 
11519  637 

638 

639 
local 

640 

641 
fun new_name (ix, (pairs,used)) = 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
20000
diff
changeset

642 
let val v = Name.variant used (string_of_indexname ix) 
11519  643 
in ((ix, v) :: pairs, v :: used) end; 
644 

17325  645 
fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of 
15531  646 
NONE => TVar (ix, sort) 
647 
 SOME name => TFree (name, sort)); 

11519  648 

649 
in 

650 

651 
fun freezeT t prf = 

652 
let 

29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

653 
val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, []) 
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

654 
and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, [])); 
23178  655 
val (alist, _) = List.foldr new_name ([], used) tvars; 
11519  656 
in 
657 
(case alist of 

658 
[] => prf (*nothing to do!*) 

659 
 _ => 

660 
let val frzT = map_type_tvar (freeze_one alist) 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20509
diff
changeset

661 
in map_proof_terms (map_types frzT) frzT prf end) 
11519  662 
end; 
663 

664 
end; 

665 

666 

667 
(***** rotate assumptions *****) 

668 

669 
fun rotate_proof Bs Bi m prf = 

670 
let 

671 
val params = Term.strip_all_vars Bi; 

672 
val asms = Logic.strip_imp_prems (Term.strip_all_body Bi); 

673 
val i = length asms; 

674 
val j = length Bs; 

675 
in 

676 
mk_AbsP (j+1, proof_combP (prf, map PBound 

23178  677 
(j downto 1) @ [mk_Abst params (mk_AbsP (i, 
11519  678 
proof_combP (proof_combt (PBound i, map Bound ((length params  1) downto 0)), 
23178  679 
map PBound (((im1) downto 0) @ ((i1) downto (im))))))])) 
11519  680 
end; 
681 

682 

683 
(***** permute premises *****) 

684 

685 
fun permute_prems_prf prems j k prf = 

686 
let val n = length prems 

687 
in mk_AbsP (n, proof_combP (prf, 

688 
map PBound ((n1 downto nj) @ (k1 downto 0) @ (nj1 downto k)))) 

689 
end; 

690 

691 

19908  692 
(***** generalization *****) 
693 

20000  694 
fun generalize (tfrees, frees) idx = 
695 
map_proof_terms_option 

31977  696 
(Term_Subst.generalize_option (tfrees, frees) idx) 
697 
(Term_Subst.generalizeT_option tfrees idx); 

19908  698 

699 

11519  700 
(***** instantiation *****) 
701 

20000  702 
fun instantiate (instT, inst) = 
703 
map_proof_terms_option 

31977  704 
(Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst)) 
705 
(Term_Subst.instantiateT_option instT); 

11519  706 

707 

708 
(***** lifting *****) 

709 

710 
fun lift_proof Bi inc prop prf = 

711 
let 

712 
fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t)); 

713 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

714 
fun lift' Us Ts (Abst (s, T, prf)) = 
22662  715 
(Abst (s, apsome' (same (op =) (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf) 
32019  716 
handle Same.SAME => Abst (s, T, lift' Us (dummyT::Ts) prf)) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

717 
 lift' Us Ts (AbsP (s, t, prf)) = 
22662  718 
(AbsP (s, apsome' (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) 
32019  719 
handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) 
15570  720 
 lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t 
32019  721 
handle Same.SAME => prf % apsome' (same (op =) (lift'' Us Ts)) t) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

722 
 lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2 
32019  723 
handle Same.SAME => prf1 %% lift' Us Ts prf2) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

724 
 lift' _ _ (PAxm (s, prop, Ts)) = 
22662  725 
PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

726 
 lift' _ _ (OfClass (T, c)) = 
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

727 
OfClass (same (op =) (Logic.incr_tvar inc) T, c) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

728 
 lift' _ _ (Oracle (s, prop, Ts)) = 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

729 
Oracle (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts) 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

730 
 lift' _ _ (Promise (i, prop, Ts)) = 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

731 
Promise (i, prop, same (op =) (map (Logic.incr_tvar inc)) Ts) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

732 
 lift' _ _ (PThm (i, ((s, prop, Ts), body))) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

733 
PThm (i, ((s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts), body)) 
32019  734 
 lift' _ _ _ = raise Same.SAME 
735 
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf); 

11519  736 

18030  737 
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); 
11519  738 
val k = length ps; 
739 

23178  740 
fun mk_app b (i, j, prf) = 
11615  741 
if b then (i1, j, prf %% PBound i) else (i, j1, prf %> Bound j); 
11519  742 

743 
fun lift Us bs i j (Const ("==>", _) $ A $ B) = 

20147  744 
AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

745 
 lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
20147  746 
Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

747 
 lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf, 
23178  748 
map (fn k => (#3 (fold_rev mk_app bs (i1, j1, PBound k)))) 
11519  749 
(i + k  1 downto i)); 
750 
in 

751 
mk_AbsP (k, lift [] [] 0 0 Bi) 

752 
end; 

753 

754 

755 
(***** proof by assumption *****) 

756 

23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

757 
fun mk_asm_prf t i m = 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

758 
let 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

759 
fun imp_prf _ i 0 = PBound i 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

760 
 imp_prf (Const ("==>", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m1)) 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

761 
 imp_prf _ i _ = PBound i; 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

762 
fun all_prf (Const ("all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

763 
 all_prf t = imp_prf t (~i) m 
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

764 
in all_prf t end; 
11519  765 

766 
fun assumption_proof Bs Bi n prf = 

767 
mk_AbsP (length Bs, proof_combP (prf, 

23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

768 
map PBound (length Bs  1 downto 0) @ [mk_asm_prf Bi n ~1])); 
11519  769 

770 

771 
(***** Composition of object rule with proof state *****) 

772 

773 
fun flatten_params_proof i j n (Const ("==>", _) $ A $ B, k) = 

15531  774 
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) 
11519  775 
 flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) = 
15531  776 
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) 
11519  777 
 flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), 
19304  778 
map Bound (j1 downto 0)), map PBound (remove (op =) (in) (i1 downto 0))); 
11519  779 

23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

780 
fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf = 
11519  781 
let 
782 
val la = length newAs; 

783 
val lb = length Bs; 

784 
in 

785 
mk_AbsP (lb+la, proof_combP (sprf, 

11615  786 
map PBound (lb + la  1 downto la)) %% 
23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

787 
proof_combP (rprf, (if n>0 then [mk_asm_prf (the A) n m] else []) @ 
18485  788 
map (if flatten then flatten_params_proof 0 0 n else PBound o snd) 
789 
(oldAs ~~ (la  1 downto 0)))) 

11519  790 
end; 
791 

792 

793 
(***** axioms for equality *****) 

794 

14854  795 
val aT = TFree ("'a", []); 
796 
val bT = TFree ("'b", []); 

11519  797 
val x = Free ("x", aT); 
798 
val y = Free ("y", aT); 

799 
val z = Free ("z", aT); 

800 
val A = Free ("A", propT); 

801 
val B = Free ("B", propT); 

802 
val f = Free ("f", aT > bT); 

803 
val g = Free ("g", aT > bT); 

804 

805 
local open Logic in 

806 

807 
val equality_axms = 

808 
[("reflexive", mk_equals (x, x)), 

809 
("symmetric", mk_implies (mk_equals (x, y), mk_equals (y, x))), 

810 
("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))), 

811 
("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))), 

812 
("equal_elim", list_implies ([mk_equals (A, B), A], B)), 

27330  813 
("abstract_rule", mk_implies 
814 
(all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))), 

815 
("combination", list_implies 

816 
([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))]; 

11519  817 

818 
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, 

819 
equal_elim_axm, abstract_rule_axm, combination_axm] = 

26424  820 
map (fn (s, t) => PAxm ("Pure." ^ s, varify t, NONE)) equality_axms; 
11519  821 

822 
end; 

823 

15531  824 
val reflexive = reflexive_axm % NONE; 
11519  825 

26424  826 
fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf 
15531  827 
 symmetric prf = symmetric_axm % NONE % NONE %% prf; 
11519  828 

26424  829 
fun transitive _ _ (PAxm ("Pure.reflexive", _, _) % _) prf2 = prf2 
830 
 transitive _ _ prf1 (PAxm ("Pure.reflexive", _, _) % _) = prf1 

11519  831 
 transitive u (Type ("prop", [])) prf1 prf2 = 
15531  832 
transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 
11519  833 
 transitive u T prf1 prf2 = 
15531  834 
transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; 
11519  835 

836 
fun abstract_rule x a prf = 

15531  837 
abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; 
11519  838 

26424  839 
fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) = 
19502  840 
is_some f orelse check_comb prf 
26424  841 
 check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = 
11519  842 
check_comb prf1 andalso check_comb prf2 
26424  843 
 check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf 
11519  844 
 check_comb _ = false; 
845 

846 
fun combination f g t u (Type (_, [T, U])) prf1 prf2 = 

847 
let 

848 
val f = Envir.beta_norm f; 

849 
val g = Envir.beta_norm g; 

850 
val prf = if check_comb prf1 then 

15531  851 
combination_axm % NONE % NONE 
11519  852 
else (case prf1 of 
26424  853 
PAxm ("Pure.reflexive", _, _) % _ => 
15531  854 
combination_axm %> remove_types f % NONE 
11615  855 
 _ => combination_axm %> remove_types f %> remove_types g) 
11519  856 
in 
857 
(case T of 

11615  858 
Type ("fun", _) => prf % 
11519  859 
(case head_of f of 
15531  860 
Abs _ => SOME (remove_types t) 
861 
 Var _ => SOME (remove_types t) 

862 
 _ => NONE) % 

11519  863 
(case head_of g of 
15531  864 
Abs _ => SOME (remove_types u) 
865 
 Var _ => SOME (remove_types u) 

866 
 _ => NONE) %% prf1 %% prf2 

867 
 _ => prf % NONE % NONE %% prf1 %% prf2) 

11519  868 
end; 
869 

870 
fun equal_intr A B prf1 prf2 = 

11615  871 
equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  872 

873 
fun equal_elim A B prf1 prf2 = 

11615  874 
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  875 

876 

877 
(***** axioms and theorems *****) 

878 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

879 
val proofs = ref 2; 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

880 

28812
413695e07bd4
Frees in PThms are now quantified in the order of their appearance in the
berghofe
parents:
28803
diff
changeset

881 
fun vars_of t = map Var (rev (Term.add_vars t [])); 
413695e07bd4
Frees in PThms are now quantified in the order of their appearance in the
berghofe
parents:
28803
diff
changeset

882 
fun frees_of t = map Free (rev (Term.add_frees t [])); 
11519  883 

884 
fun test_args _ [] = true 

885 
 test_args is (Bound i :: ts) = 

17492  886 
not (member (op =) is i) andalso test_args (i :: is) ts 
11519  887 
 test_args _ _ = false; 
888 

889 
fun is_fun (Type ("fun", _)) = true 

890 
 is_fun (TVar _) = true 

891 
 is_fun _ = false; 

892 

893 
fun add_funvars Ts (vs, t) = 

894 
if is_fun (fastype_of1 (Ts, t)) then 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19357
diff
changeset

895 
vs union map_filter (fn Var (ixn, T) => 
15531  896 
if is_fun T then SOME ixn else NONE  _ => NONE) (vars_of t) 
11519  897 
else vs; 
898 

899 
fun add_npvars q p Ts (vs, Const ("==>", _) $ t $ u) = 

900 
add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) 

901 
 add_npvars q p Ts (vs, Const ("all", Type (_, [Type (_, [T, _]), _])) $ t) = 

902 
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) 

12041  903 
 add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) 
904 
 add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) 

905 
and add_npvars' Ts (vs, t) = (case strip_comb t of 

11519  906 
(Var (ixn, _), ts) => if test_args [] ts then vs 
17314  907 
else Library.foldl (add_npvars' Ts) 
908 
(AList.update (op =) (ixn, 

909 
Library.foldl (add_funvars Ts) ((these ooo AList.lookup) (op =) vs ixn, ts)) vs, ts) 

15570  910 
 (Abs (_, T, u), ts) => Library.foldl (add_npvars' (T::Ts)) (vs, u :: ts) 
911 
 (_, ts) => Library.foldl (add_npvars' Ts) (vs, ts)); 

11519  912 

913 
fun prop_vars (Const ("==>", _) $ P $ Q) = prop_vars P union prop_vars Q 

914 
 prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t 

915 
 prop_vars t = (case strip_comb t of 

916 
(Var (ixn, _), _) => [ixn]  _ => []); 

917 

918 
fun is_proj t = 

919 
let 

920 
fun is_p i t = (case strip_comb t of 

921 
(Bound j, []) => false 

922 
 (Bound j, ts) => j >= i orelse exists (is_p i) ts 

923 
 (Abs (_, _, u), _) => is_p (i+1) u 

924 
 (_, ts) => exists (is_p i) ts) 

925 
in (case strip_abs_body t of 

926 
Bound _ => true 

927 
 t' => is_p 0 t') 

928 
end; 

929 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

930 
fun needed_vars prop = 
20853  931 
Library.foldl (op union) 
932 
([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union 

11519  933 
prop_vars prop; 
934 

935 
fun gen_axm_proof c name prop = 

936 
let 

937 
val nvs = needed_vars prop; 

938 
val args = map (fn (v as Var (ixn, _)) => 

17492  939 
if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ 
28812
413695e07bd4
Frees in PThms are now quantified in the order of their appearance in the
berghofe
parents:
28803
diff
changeset

940 
map SOME (frees_of prop); 
11519  941 
in 
15531  942 
proof_combt' (c (name, prop, NONE), args) 
11519  943 
end; 
944 

945 
val axm_proof = gen_axm_proof PAxm; 

17017  946 

947 
val dummy = Const (Term.dummy_patternN, dummyT); 

948 

949 
fun oracle_proof name prop = 

30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

950 
if ! proofs = 0 then ((name, dummy), Oracle (name, dummy, NONE)) 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

951 
else ((name, prop), gen_axm_proof Oracle name prop); 
11519  952 

17492  953 
fun shrink_proof thy = 
954 
let 

955 
fun shrink ls lev (prf as Abst (a, T, body)) = 

956 
let val (b, is, ch, body') = shrink ls (lev+1) body 

26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

957 
in (b, is, ch, if ch then Abst (a, T, body') else prf) end 
17492  958 
 shrink ls lev (prf as AbsP (a, t, body)) = 
959 
let val (b, is, ch, body') = shrink (lev::ls) lev body 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19357
diff
changeset

960 
in (b orelse member (op =) is 0, map_filter (fn 0 => NONE  i => SOME (i1)) is, 
26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

961 
ch, if ch then AbsP (a, t, body') else prf) 
17492  962 
end 
963 
 shrink ls lev prf = 

964 
let val (is, ch, _, prf') = shrink' ls lev [] [] prf 

965 
in (false, is, ch, prf') end 

966 
and shrink' ls lev ts prfs (prf as prf1 %% prf2) = 

967 
let 

968 
val p as (_, is', ch', prf') = shrink ls lev prf2; 

969 
val (is, ch, ts', prf'') = shrink' ls lev ts (p::prfs) prf1 

970 
in (is union is', ch orelse ch', ts', 

971 
if ch orelse ch' then prf'' %% prf' else prf) 

972 
end 

973 
 shrink' ls lev ts prfs (prf as prf1 % t) = 

974 
let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1 

975 
in (is, ch orelse ch', ts', 

26631
d6b6c74a8bcf
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26424
diff
changeset

976 
if ch orelse ch' then prf' % t' else prf) end 
17492  977 
 shrink' ls lev ts prfs (prf as PBound i) = 
30146  978 
(if exists (fn SOME (Bound j) => levj <= nth ls i  _ => true) ts 
18928
042608ffa2ec
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
haftmann
parents:
18485
diff
changeset

979 
orelse has_duplicates (op =) 
042608ffa2ec
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
haftmann
parents:
18485
diff
changeset

980 
(Library.foldl (fn (js, SOME (Bound j)) => j :: js  (js, _) => js) ([], ts)) 
17492  981 
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) 
31903  982 
 shrink' ls lev ts prfs (prf as Hyp _) = ([], false, map (pair false) ts, prf) 
983 
 shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf) 

31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

984 
 shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf) 
17492  985 
 shrink' ls lev ts prfs prf = 
986 
let 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

987 
val prop = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

988 
(case prf of 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

989 
PAxm (_, prop, _) => prop 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

990 
 Oracle (_, prop, _) => prop 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

991 
 Promise (_, prop, _) => prop 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

992 
 PThm (_, ((_, prop, _), _)) => prop 
28319
13cb2108c2b9
added Promise constructor, which is similar to Oracle but may be replaced later;
wenzelm
parents:
27330
diff
changeset

993 
 _ => error "shrink: proof not in normal form"); 
17492  994 
val vs = vars_of prop; 
19012  995 
val (ts', ts'') = chop (length vs) ts; 
17492  996 
val insts = Library.take (length ts', map (fst o dest_Var) vs) ~~ ts'; 
997 
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => 

998 
insert (op =) ixn (case AList.lookup (op =) insts ixn of 

999 
SOME (SOME t) => if is_proj t then ixns union ixns' else ixns' 

1000 
 _ => ixns union ixns')) 

1001 
(needed prop ts'' prfs, add_npvars false true [] ([], prop)); 

1002 
val insts' = map 

1003 
(fn (ixn, x as SOME _) => if member (op =) nvs ixn then (false, x) else (true, NONE) 

1004 
 (_, x) => (false, x)) insts 

1005 
in ([], false, insts' @ map (pair false) ts'', prf) end 

1006 
and needed (Const ("==>", _) $ t $ u) ts ((b, _, _, _)::prfs) = 

1007 
(if b then map (fst o dest_Var) (vars_of t) else []) union needed u ts prfs 

1008 
 needed (Var (ixn, _)) (_::_) _ = [ixn] 

1009 
 needed _ _ _ = []; 

1010 
in shrink end; 

11519  1011 

1012 

1013 
(**** Simple first order matching functions for terms and proofs ****) 

1014 

1015 
exception PMatch; 

1016 

1017 
(** see pattern.ML **) 

1018 

15570  1019 
fun flt (i: int) = List.filter (fn n => n < i); 
12279  1020 

1021 
fun fomatch Ts tymatch j = 

11519  1022 
let 
1023 
fun mtch (instsp as (tyinsts, insts)) = fn 

1024 
(Var (ixn, T), t) => 

12279  1025 
if j>0 andalso not (null (flt j (loose_bnos t))) 
1026 
then raise PMatch 

1027 
else (tymatch (tyinsts, fn () => (T, fastype_of1 (Ts, t))), 

1028 
(ixn, t) :: insts) 

11519  1029 
 (Free (a, T), Free (b, U)) => 
20147  1030 
if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch 
11519  1031 
 (Const (a, T), Const (b, U)) => 
20147  1032 
if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch 
11519  1033 
 (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) 
12279  1034 
 (Bound i, Bound j) => if i=j then instsp else raise PMatch 
11519  1035 
 _ => raise PMatch 
1036 
in mtch end; 

1037 

12279  1038 
fun match_proof Ts tymatch = 
11519  1039 
let 
15531  1040 
fun optmatch _ inst (NONE, _) = inst 
1041 
 optmatch _ _ (SOME _, NONE) = raise PMatch 

1042 
 optmatch mtch inst (SOME x, SOME y) = mtch inst (x, y) 

12279  1043 

1044 
fun matcht Ts j (pinst, tinst) (t, u) = 

1045 
(pinst, fomatch Ts tymatch j tinst (t, Envir.beta_norm u)); 

1046 
fun matchT (pinst, (tyinsts, insts)) p = 

1047 
(pinst, (tymatch (tyinsts, K p), insts)); 

15570  1048 
fun matchTs inst (Ts, Us) = Library.foldl (uncurry matchT) (inst, Ts ~~ Us); 
12279  1049 

1050 
fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) = 

1051 
if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst) 

1052 
else (case apfst (flt i) (apsnd (flt j) 

1053 
(prf_add_loose_bnos 0 0 prf ([], []))) of 

1054 
([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) 

1055 
 ([], _) => if j = 0 then 

1056 
((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst) 

1057 
else raise PMatch 

1058 
 _ => raise PMatch) 

1059 
 mtch Ts i j inst (prf1 % opt1, prf2 % opt2) = 

1060 
optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2) 

1061 
 mtch Ts i j inst (prf1 %% prf2, prf1' %% prf2') = 

1062 
mtch Ts i j (mtch Ts i j inst (prf1, prf1')) (prf2, prf2') 

1063 
 mtch Ts i j inst (Abst (_, opT, prf1), Abst (_, opU, prf2)) = 

18485  1064 
mtch (the_default dummyT opU :: Ts) i (j+1) 
12279  1065 
(optmatch matchT inst (opT, opU)) (prf1, prf2) 
1066 
 mtch Ts i j inst (prf1, Abst (_, opU, prf2)) = 

18485  1067 
mtch (the_default dummyT opU :: Ts) i (j+1) inst 
12279  1068 
(incr_pboundvars 0 1 prf1 %> Bound 0, prf2) 
1069 
 mtch Ts i j inst (AbsP (_, opt, prf1), AbsP (_, opu, prf2)) = 

1070 
mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2) 

1071 
 mtch Ts i j inst (prf1, AbsP (_, _, prf2)) = 

1072 
mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2) 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1073 
 mtch Ts i j inst (PAxm (s1, _, opTs), PAxm (s2, _, opUs)) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1074 
if s1 = s2 then optmatch matchTs inst (opTs, opUs) 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1075 
else raise PMatch 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

1076 
 mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) = 
31903  1077 
if c1 = c2 then matchT inst (T1, T2) 
1078 
else raise PMatch 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1079 
 mtch Ts i j inst (PThm (_, ((name1, prop1, opTs), _)), PThm (_, ((name2, prop2, opUs), _))) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1080 
if name1 = name2 andalso prop1 = prop2 then 
12279  1081 
optmatch matchTs inst (opTs, opUs) 
11519  1082 
else raise PMatch 
12279  1083 
 mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch 
1084 
 mtch _ _ _ _ _ = raise PMatch 

1085 
in mtch Ts 0 0 end; 

11519  1086 

1087 
fun prf_subst (pinst, (tyinsts, insts)) = 

1088 
let 

15797  1089 
val substT = Envir.typ_subst_TVars tyinsts; 
11519  1090 

17325  1091 
fun subst' lev (t as Var (ixn, _)) = (case AList.lookup (op =) insts ixn of 
15531  1092 
NONE => t 
1093 
 SOME u => incr_boundvars lev u) 

11519  1094 
 subst' lev (Const (s, T)) = Const (s, substT T) 
1095 
 subst' lev (Free (s, T)) = Free (s, substT T) 

1096 
 subst' lev (Abs (a, T, body)) = Abs (a, substT T, subst' (lev+1) body) 

1097 
 subst' lev (f $ t) = subst' lev f $ subst' lev t 

1098 
 subst' _ t = t; 

1099 

1100 
fun subst plev tlev (AbsP (a, t, body)) = 

15570  1101 
AbsP (a, Option.map (subst' tlev) t, subst (plev+1) tlev body) 
11519  1102 
 subst plev tlev (Abst (a, T, body)) = 
15570  1103 
Abst (a, Option.map substT T, subst plev (tlev+1) body) 
11615  1104 
 subst plev tlev (prf %% prf') = subst plev tlev prf %% subst plev tlev prf' 
15570  1105 
 subst plev tlev (prf % t) = subst plev tlev prf % Option.map (subst' tlev) t 
17325  1106 
 subst plev tlev (prf as Hyp (Var (ixn, _))) = (case AList.lookup (op =) pinst ixn of 
15531  1107 
NONE => prf 
1108 
 SOME prf' => incr_pboundvars plev tlev prf') 

28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1109 
 subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Option.map (map substT) Ts) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

1110 
 subst _ _ (OfClass (T, c)) = OfClass (substT T, c) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1111 
 subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Option.map (map substT) Ts) 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1112 
 subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, (map substT) Ts) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1113 
 subst _ _ (PThm (i, ((id, prop, Ts), body))) = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1114 
PThm (i, ((id, prop, Option.map (map substT) Ts), body)) 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1115 
 subst _ _ t = t; 
11519  1116 
in subst 0 0 end; 
1117 

21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

1118 
(*A fast unification filter: true unless the two terms cannot be unified. 
12871
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1119 
Terms must be NORMAL. Treats all Vars as distinct. *) 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1120 
fun could_unify prf1 prf2 = 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1121 
let 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1122 
fun matchrands (prf1 %% prf2) (prf1' %% prf2') = 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1123 
could_unify prf2 prf2' andalso matchrands prf1 prf1' 
15531  1124 
 matchrands (prf % SOME t) (prf' % SOME t') = 
12871
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1125 
Term.could_unify (t, t') andalso matchrands prf prf' 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1126 
 matchrands (prf % _) (prf' % _) = matchrands prf prf' 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1127 
 matchrands _ _ = true 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1128 

21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1129 
fun head_of (prf %% _) = head_of prf 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1130 
 head_of (prf % _) = head_of prf 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1131 
 head_of prf = prf 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1132 

21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1133 
in case (head_of prf1, head_of prf2) of 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1134 
(_, Hyp (Var _)) => true 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1135 
 (Hyp (Var _), _) => true 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1136 
 (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

1137 
 (OfClass (_, c), OfClass (_, d)) => c = d andalso matchrands prf1 prf2 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1138 
 (PThm (_, ((a, propa, _), _)), PThm (_, ((b, propb, _), _))) => 
12871
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1139 
a = b andalso propa = propb andalso matchrands prf1 prf2 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1140 
 (PBound i, PBound j) => i = j andalso matchrands prf1 prf2 
12871
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1141 
 (AbsP _, _) => true (*because of possible eta equality*) 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1142 
 (Abst _, _) => true 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1143 
 (_, AbsP _) => true 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1144 
 (_, Abst _) => true 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1145 
 _ => false 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1146 
end; 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

1147 

28329
e6a5fa9f1e41
added conditional add_oracles, keep oracles_of_proof private;
wenzelm
parents:
28319
diff
changeset

1148 

11519  1149 
(**** rewriting on proof terms ****) 
1150 

13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1151 
val skel0 = PBound 0; 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1152 

12279  1153 
fun rewrite_prf tymatch (rules, procs) prf = 
11519  1154 
let 
15531  1155 
fun rew _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, skel0) 
1156 
 rew _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, skel0) 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1157 
 rew Ts prf = (case get_first (fn r => r Ts prf) procs of 
15531  1158 
SOME prf' => SOME (prf', skel0) 
1159 
 NONE => get_first (fn (prf1, prf2) => SOME (prf_subst 

13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1160 
(match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1161 
handle PMatch => NONE) (filter (could_unify prf o fst) rules)); 
11519  1162 

11615  1163 
fun rew0 Ts (prf as AbsP (_, _, prf' %% PBound 0)) = 
11519  1164 
if prf_loose_Pbvar1 prf' 0 then rew Ts prf 
1165 
else 

1166 
let val prf'' = incr_pboundvars (~1) 0 prf' 

19502  1167 
in SOME (the_default (prf'', skel0) (rew Ts prf'')) end 
15531  1168 
 rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) = 
11519  1169 
if prf_loose_bvar1 prf' 0 then rew Ts prf 
1170 
else 

1171 
let val prf'' = incr_pboundvars 0 (~1) prf' 

19502  1172 
in SOME (the_default (prf'', skel0) (rew Ts prf'')) end 
11519  1173 
 rew0 Ts prf = rew Ts prf; 
1174 

15531  1175 
fun rew1 _ (Hyp (Var _)) _ = NONE 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1176 
 rew1 Ts skel prf = (case rew2 Ts skel prf of 
15531  1177 
SOME prf1 => (case rew0 Ts prf1 of 
19502  1178 
SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2)) 
15531  1179 
 NONE => SOME prf1) 
1180 
 NONE => (case rew0 Ts prf of 

19502  1181 
SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1)) 
15531  1182 
 NONE => NONE)) 
11519  1183 

15531  1184 
and rew2 Ts skel (prf % SOME t) = (case prf of 
11519  1185 
Abst (_, _, body) => 
1186 
let val prf' = prf_subst_bounds [t] body 

19502  1187 
in SOME (the_default prf' (rew2 Ts skel0 prf')) end 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1188 
 _ => (case rew1 Ts (case skel of skel' % _ => skel'  _ => skel0) prf of 
15531  1189 
SOME prf' => SOME (prf' % SOME t) 
1190 
 NONE => NONE)) 

15570  1191 
 rew2 Ts skel (prf % NONE) = Option.map (fn prf' => prf' % NONE) 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1192 
(rew1 Ts (case skel of skel' % _ => skel'  _ => skel0) prf) 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1193 
 rew2 Ts skel (prf1 %% prf2) = (case prf1 of 
11519  1194 
AbsP (_, _, body) => 
1195 
let val prf' = prf_subst_pbounds [prf2] body 

19502  1196 
in SOME (the_default prf' (rew2 Ts skel0 prf')) end 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1197 
 _ => 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1198 
let val (skel1, skel2) = (case skel of 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1199 
skel1 %% skel2 => (skel1, skel2) 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1200 
 _ => (skel0, skel0)) 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1201 
in case rew1 Ts skel1 prf1 of 
15531  1202 
SOME prf1' => (case rew1 Ts skel2 prf2 of 
1203 
SOME prf2' => SOME (prf1' %% prf2') 

1204 
 NONE => SOME (prf1' %% prf2)) 

1205 
 NONE => (case rew1 Ts skel2 prf2 of 

1206 
SOME prf2' => SOME (prf1 %% prf2') 

1207 
 NONE => NONE) 

13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1208 
end) 
19502  1209 
 rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1210 
(case skel of Abst (_, _, skel') => skel'  _ => skel0) prf of 
15531  1211 
SOME prf' => SOME (Abst (s, T, prf')) 
1212 
 NONE => NONE) 

13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1213 
 rew2 Ts skel (AbsP (s, t, prf)) = (case rew1 Ts 
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1214 
(case skel of AbsP (_, _, skel') => skel'  _ => skel0) prf of 
15531  1215 
SOME prf' => SOME (AbsP (s, t, prf')) 
1216 
 NONE => NONE) 

1217 
 rew2 _ _ _ = NONE 

11519  1218 

19502  1219 
in the_default prf (rew1 [] skel0 prf) end; 
11519  1220 

17203  1221 
fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) => 
1222 
Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch); 

11519  1223 

11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

1224 
fun rewrite_proof_notypes rews = rewrite_prf fst rews; 
11615  1225 

16940  1226 

11519  1227 
(**** theory data ****) 
1228 

16458  1229 
structure ProofData = TheoryDataFun 
22846  1230 
( 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1231 
type T = (stamp * (proof * proof)) list * (stamp * (typ list > proof > proof option)) list; 
11519  1232 

12233  1233 
val empty = ([], []); 
1234 
val copy = I; 

16458  1235 
val extend = I; 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1236 
fun merge _ ((rules1, procs1), (rules2, procs2)) : T = 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1237 
(AList.merge (op =) (K true) (rules1, rules2), 
22662  1238 
AList.merge (op =) (K true) (procs1, procs2)); 
22846  1239 
); 
11519  1240 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1241 
fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end; 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1242 
fun rew_proof thy = rewrite_prf fst (get_data thy); 
23780
a0e7305dd0cb
Added function rew_proof (for prenormalizing proofs).
berghofe
parents:
23296
diff
changeset

1243 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1244 
fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r)); 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1245 
fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p)); 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1246 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1247 

28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1248 
(***** promises *****) 
11519  1249 

28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1250 
fun promise_proof thy i prop = 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1251 
let 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1252 
val _ = prop > Term.exists_subterm (fn t => 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1253 
(Term.is_Free t orelse Term.is_Var t) andalso 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1254 
error ("promise_proof: illegal variable " ^ Syntax.string_of_term_global thy t)); 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1255 
val _ = prop > Term.exists_type (Term.exists_subtype 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1256 
(fn TFree (a, _) => error ("promise_proof: illegal type variable " ^ quote a) 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1257 
 _ => false)); 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1258 
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end; 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1259 

c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1260 
fun fulfill_proof _ [] body0 = body0 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1261 
 fulfill_proof thy ps body0 = 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1262 
let 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1263 
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0; 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1264 
val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1265 
val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0; 
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1266 
val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty; 
28875
c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1267 

c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1268 
fun fill (Promise (i, prop, Ts)) = 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1269 
(case Inttab.lookup proofs i of 
28875
c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1270 
NONE => NONE 
30716
2ee706293eb5
removed misleading make_proof_body, make_oracles, make_thms, which essentially assume a *full* proof;
wenzelm
parents:
30712
diff
changeset

1271 
 SOME prf => SOME (instantiate (Term.add_tvars prop [] ~~ Ts, []) prf)) 
28875
c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1272 
 fill _ = NONE; 
c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1273 
val (rules, procs) = get_data thy; 
c1c0e23ed063
eliminated finish_proof, keep pre/post normalization of results separate;
wenzelm
parents:
28846
diff
changeset

1274 
val proof = rewrite_prf fst (rules, K fill :: procs) proof0; 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1275 
in PBody {oracles = oracles, thms = thms, proof = proof} end; 
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1276 

29642  1277 
fun fulfill_proof_future _ [] body = Future.value body 
1278 
 fulfill_proof_future thy promises body = 

1279 
Future.fork_deps (map snd promises) (fn () => 

1280 
fulfill_proof thy (map (apsnd Future.join) promises) body); 

1281 

28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1282 

c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

1283 
(***** theorems *****) 
11519  1284 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1285 
fun thm_proof thy name hyps prop promises body = 
11519  1286 
let 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1287 
val PBody {oracles = oracles0, thms = thms0, proof = prf} = body; 
12923  1288 
val prop = Logic.list_implies (hyps, prop); 
11519  1289 
val nvs = needed_vars prop; 
1290 
val args = map (fn (v as Var (ixn, _)) => 

17492  1291 
if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @ 
28812
413695e07bd4
Frees in PThms are now quantified in the order of their appearance in the
berghofe
parents:
28803
diff
changeset

1292 
map SOME (frees_of prop); 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1293 

d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1294 
val proof0 = 
28876  1295 
if ! proofs = 2 then 
1296 
#4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf))) 

1297 
else MinProof; 

29642  1298 
val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0}; 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1299 

29642  1300 
fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0); 
28815  1301 
val (i, name, prop, body') = 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1302 
(case strip_combt (fst (strip_combP prf)) of 
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1303 
(PThm (i, ((old_name, prop', NONE), body')), args') => 
28815  1304 
if (old_name = "" orelse old_name = name) andalso prop = prop' andalso args = args' 
1305 
then (i, name, prop, body') 

28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

1306 
else new_prf () 
28815  1307 
 _ => new_prf ()); 
1308 
val head = PThm (i, ((name, prop, NONE), body')); 

11519  1309 
in 
28815  1310 
((i, (name, prop, body')), proof_combP (proof_combt' (head, args), map Hyp hyps)) 
11519  1311 
end; 