author  wenzelm 
Tue, 09 Aug 2011 22:30:33 +0200  
changeset 44101  202d2f56560c 
parent 44100  2cf62c4e6c7a 
child 44113  0baa8bbd355a 
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 

32738  11 
val proofs: int Unsynchronized.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 
39687  27 
{oracles: (string * term) Ord_List.T, 
28 
thms: (serial * (string * term * proof_body future)) Ord_List.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) 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

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

41 
val join_proof: proof_body future > proof 
30711  42 
val fold_proof_atoms: bool > (proof > 'a > 'a) > proof list > 'a > 'a 
32810
f3466a5645fa
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc)  the cycle check is implicit in the future computation of join_proofs;
wenzelm
parents:
32785
diff
changeset

43 
val fold_body_thms: (string * term * proof_body > 'a > 'a) > proof_body list > 'a > 'a 
32054  44 
val join_bodies: proof_body list > unit 
30712  45 
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

46 

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

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

48 
val thm_ord: pthm * pthm > order 
39687  49 
val merge_oracles: oracle Ord_List.T > oracle Ord_List.T > oracle Ord_List.T 
50 
val merge_thms: pthm Ord_List.T > pthm Ord_List.T > pthm Ord_List.T 

51 
val all_oracles_of: proof_body > oracle Ord_List.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 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

53 

11519  54 
(** primitive operations **) 
41698  55 
val proofs_enabled: unit > bool 
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 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

62 
val map_proof_same: term Same.operation > typ Same.operation 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

63 
> (typ * class > proof) > proof Same.operation 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

64 
val map_proof_terms_same: term Same.operation > typ Same.operation > proof Same.operation 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

65 
val map_proof_types_same: typ Same.operation > proof Same.operation 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

66 
val map_proof_terms: (term > term) > (typ > typ) > proof > proof 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

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

68 
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

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

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

71 
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

72 
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

73 
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

74 
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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

82 
val freeze_thaw_prf: proof > proof * (proof > proof) 
11519  83 

84 
(** 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

85 
val implies_intr_proof: term > proof > proof 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

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

87 
val forall_intr_proof: term > string > proof > proof 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

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

89 
val varify_proof: term > (string * sort) list > proof > proof 
36619
deadcd0ec431
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
wenzelm
parents:
35851
diff
changeset

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

91 
val rotate_proof: term list > term > int > proof > proof 
36742  92 
val permute_prems_proof: term list > int > int > proof > proof 
19908  93 
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

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

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

98 
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

99 
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

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

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

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

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

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

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

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

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

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

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

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

111 
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

112 
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

113 
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

114 
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

115 
val equal_elim: term > term > proof > proof > proof 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

116 
val strip_shyps_proof: Sorts.algebra > (typ * sort) list > (typ * sort) list > 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

117 
sort list > proof > proof 
36740  118 
val classrel_proof: theory > class * class > proof 
119 
val arity_proof: theory > string * sort list * class > proof 

36741
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

120 
val of_sort_proof: theory > (typ * class > proof) > typ * sort > proof list 
36740  121 
val install_axclass_proofs: 
122 
{classrel_proof: theory > class * class > proof, 

123 
arity_proof: theory > string * sort list * class > proof} > unit 

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

124 
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

125 
val oracle_proof: string > term > oracle * proof 
11519  126 

127 
(** rewriting on proof terms **) 

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

128 
val add_prf_rrule: proof * proof > theory > theory 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

129 
val add_prf_rproc: (typ list > term option list > proof > (proof * proof) option) > theory > theory 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

130 
val no_skel: proof 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

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

132 
val rewrite_proof: theory > (proof * proof) list * 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

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

134 
val rewrite_proof_notypes: (proof * proof) list * 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

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

136 
val rew_proof: theory > proof > proof 
36877
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

137 

7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

138 
val promise_proof: theory > serial > term > proof 
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

139 
val fulfill_norm_proof: theory > (serial * proof_body) list > proof_body > proof_body 
36882
f33760bb8ca0
conditionally unconstrain thm proofs  loosely based on the version by krauss/schropp;
wenzelm
parents:
36880
diff
changeset

140 
val thm_proof: theory > string > sort list > term list > term > 
36877
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

141 
(serial * proof_body future) list > proof_body > pthm * proof 
36883
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

142 
val unconstrain_thm_proof: theory > sort list > term > 
4ed0d72def50
added Proofterm.unconstrain_thm_proof for Thm.unconstrainT  loosely based on the version by krauss/schropp;
wenzelm
parents:
36882
diff
changeset

143 
(serial * proof_body future) list > proof_body > pthm * proof 
37297  144 
val get_name: sort list > term list > term > proof > string 
36877
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

145 
val guess_name: proof > string 
11519  146 
end 
147 

148 
structure Proofterm : PROOFTERM = 

149 
struct 

150 

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

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

152 

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

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

155 
 PBound of int 
11519  156 
 Abst of string * typ option * proof 
157 
 AbsP of string * term option * proof 

12497  158 
 op % of proof * term option 
159 
 op %% of proof * proof 

11519  160 
 Hyp of term 
161 
 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

162 
 OfClass of typ * class 
11519  163 
 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

164 
 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

165 
 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

166 
and proof_body = PBody of 
39687  167 
{oracles: (string * term) Ord_List.T, 
168 
thms: (serial * (string * term * proof_body future)) Ord_List.T, 

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

169 
proof: proof}; 
11519  170 

28815  171 
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

172 
type pthm = serial * (string * term * proof_body future); 
28815  173 

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

174 
fun proof_of (PBody {proof, ...}) = proof; 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

175 
val join_proof = Future.join #> proof_of; 
17017  176 

177 

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

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

179 

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

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

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

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

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

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

185 
 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

186 
 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

187 
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

188 
else 
28815  189 
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

190 
(if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen) 
28815  191 
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

192 
 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

193 
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

194 

30711  195 
fun fold_body_thms f = 
196 
let 

32726  197 
fun app (PBody {thms, ...}) = 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

198 
(Future.join_results (map (#3 o #2) thms); 
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

199 
thms > fold (fn (i, (name, prop, body)) => fn (x, seen) => 
32726  200 
if Inttab.defined seen i then (x, seen) 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

201 
else 
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

202 
let 
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

203 
val body' = Future.join body; 
32726  204 
val (x', seen') = app body' (x, Inttab.update (i, ()) seen); 
32810
f3466a5645fa
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc)  the cycle check is implicit in the future computation of join_proofs;
wenzelm
parents:
32785
diff
changeset

205 
in (f (name, prop, body') x', seen') end)); 
32726  206 
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; 
30711  207 

32054  208 
fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies (); 
209 

30712  210 
fun status_of bodies = 
30711  211 
let 
212 
fun status (PBody {oracles, thms, ...}) x = 

213 
let 

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

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

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

217 
else 

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

219 
(case Future.peek body of 

43761
e72ba84ae58f
tuned signature  corresponding to Scala version;
wenzelm
parents:
43329
diff
changeset

220 
SOME (Exn.Res body') => status body' (st, seen') 
30711  221 
 SOME (Exn.Exn _) => 
222 
let val (oracle, unfinished, _) = st 

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

224 
 NONE => 

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

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

227 
end); 

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

32057  229 
val (oracle, unfinished, failed) = 
230 
#1 (fold status bodies ((false, false, false), Inttab.empty)); 

30711  231 
in {oracle = oracle, unfinished = unfinished, failed = failed} end; 
232 

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

233 

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

235 

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

237 
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

238 

39687  239 
val merge_oracles = Ord_List.union oracle_ord; 
240 
val merge_thms = Ord_List.union thm_ord; 

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

241 

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

242 
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

243 
let 
32057  244 
fun collect (PBody {oracles, thms, ...}) = 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

245 
(Future.join_results (map (#3 o #2) thms); 
32057  246 
thms > fold (fn (i, (_, _, body)) => fn (x, seen) => 
247 
if Inttab.defined seen i then (x, seen) 

248 
else 

249 
let 

250 
val body' = Future.join body; 

251 
val (x', seen') = collect body' (x, Inttab.update (i, ()) seen); 

32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

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

253 
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

254 

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

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

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

257 
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

258 
(fn Oracle (s, prop, _) => apfst (cons (s, prop)) 
28815  259 
 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

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

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

262 
PBody 
39687  263 
{oracles = Ord_List.make oracle_ord oracles, 
264 
thms = Ord_List.make thm_ord thms, 

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

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

266 
end; 
11519  267 

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

268 

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

269 
(***** proof objects with different levels of detail *****) 
11519  270 

15531  271 
fun (prf %> t) = prf % SOME t; 
11519  272 

15570  273 
val proof_combt = Library.foldl (op %>); 
274 
val proof_combt' = Library.foldl (op %); 

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

11519  276 

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

277 
fun strip_combt prf = 
11615  278 
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

279 
 stripc x = x 
11519  280 
in stripc (prf, []) end; 
281 

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

282 
fun strip_combP prf = 
11615  283 
let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) 
11519  284 
 stripc x = x 
285 
in stripc (prf, []) end; 

286 

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

287 
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

288 
(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

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

290 
 _ => body); 
11519  291 

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

36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

295 
fun map_proof_same term typ ofclass = 
20000  296 
let 
32024  297 
val typs = Same.map typ; 
20000  298 

32024  299 
fun proof (Abst (s, T, prf)) = 
300 
(Abst (s, Same.map_option typ T, Same.commit proof prf) 

301 
handle Same.SAME => Abst (s, T, proof prf)) 

302 
 proof (AbsP (s, t, prf)) = 

303 
(AbsP (s, Same.map_option term t, Same.commit proof prf) 

304 
handle Same.SAME => AbsP (s, t, proof prf)) 

305 
 proof (prf % t) = 

306 
(proof prf % Same.commit (Same.map_option term) t 

307 
handle Same.SAME => prf % Same.map_option term t) 

308 
 proof (prf1 %% prf2) = 

309 
(proof prf1 %% Same.commit proof prf2 

310 
handle Same.SAME => prf1 %% proof prf2) 

311 
 proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts)) 

36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

312 
 proof (OfClass T_c) = ofclass T_c 
32024  313 
 proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) 
314 
 proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts) 

32057  315 
 proof (PThm (i, ((a, prop, SOME Ts), body))) = 
316 
PThm (i, ((a, prop, SOME (typs Ts)), body)) 

32024  317 
 proof _ = raise Same.SAME; 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

318 
in proof end; 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

319 

e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

320 
fun map_proof_terms_same term typ = map_proof_same term typ (fn (T, c) => OfClass (typ T, c)); 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

321 
fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; 
20000  322 

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

324 
let val x' = f x 
32019  325 
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

326 

36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

327 
fun map_proof_terms f g = Same.commit (map_proof_terms_same (same (op =) f) (same (op =) g)); 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

328 
fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); 
11519  329 

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

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

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

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

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

336 
 fold_proof_terms f g (prf1 %% prf2) = 

337 
fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 

20159  338 
 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

339 
 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

340 
 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

341 
 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

342 
 fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts 
20147  343 
 fold_proof_terms _ _ _ = I; 
11519  344 

20300  345 
fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf; 
12868  346 

13744  347 
fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf 
13749  348 
 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

349 
 size_of_proof (prf % _) = 1 + size_of_proof prf 
13744  350 
 size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 
351 
 size_of_proof _ = 1; 

352 

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

353 
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

354 
 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

355 
 change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs) 
36879
201a4afd8533
raise Fail uniformly for proofterm errors, which appear to be rather lowlevel;
wenzelm
parents:
36878
diff
changeset

356 
 change_type opTs (Promise _) = raise Fail "change_type: unexpected promise" 
32057  357 
 change_type opTs (PThm (i, ((name, prop, _), body))) = 
358 
PThm (i, ((name, prop, opTs), body)) 

12907
27e6d344d724
New function change_type for changing type assignments of theorems,
berghofe
parents:
12890
diff
changeset

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

360 

11519  361 

362 
(***** utilities *****) 

363 

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

365 
 strip_abs _ t = t; 

366 

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

369 

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

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

373 

374 
fun prf_abstract_over v = 

375 
let 

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

376 
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

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

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

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

11519  382 

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

383 
fun abst lev (AbsP (a, t, prf)) = 
32024  384 
(AbsP (a, Same.map_option (abst' lev) t, absth lev prf) 
32019  385 
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

386 
 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

387 
 abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 
32019  388 
handle Same.SAME => prf1 %% abst lev prf2) 
15570  389 
 abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t 
32024  390 
handle Same.SAME => prf % Same.map_option (abst' lev) t) 
32019  391 
 abst _ _ = raise Same.SAME 
32024  392 
and absth lev prf = (abst lev prf handle Same.SAME => prf); 
11519  393 

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

394 
in absth 0 end; 
11519  395 

396 

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

398 
required when moving a proof term within abstractions 

399 
inc is increment for bound variables 

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

401 

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

403 

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

404 
fun prf_incr_bv' incP inct Plev tlev (PBound i) = 
32019  405 
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

406 
 prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) = 
32024  407 
(AbsP (a, Same.map_option (same (op =) (incr_bv' inct tlev)) t, 
32019  408 
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

409 
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

410 
 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

411 
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

412 
 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

413 
(prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf' 
32019  414 
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

415 
 prf_incr_bv' incP inct Plev tlev (prf % t) = 
15570  416 
(prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t 
32024  417 
handle Same.SAME => prf % Same.map_option (same (op =) (incr_bv' inct tlev)) t) 
32019  418 
 prf_incr_bv' _ _ _ _ _ = raise Same.SAME 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

419 
and prf_incr_bv incP inct Plev tlev prf = 
32019  420 
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); 
11519  421 

422 
fun incr_pboundvars 0 0 prf = prf 

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

424 

425 

11615  426 
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k 
15531  427 
 prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) 
428 
 prf_loose_bvar1 (_ % NONE) _ = true 

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

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

11519  431 
 prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) 
432 
 prf_loose_bvar1 _ _ = false; 

433 

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

11615  435 
 prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k 
436 
 prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k 

11519  437 
 prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) 
438 
 prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k 

439 
 prf_loose_Pbvar1 _ _ = false; 

440 

12279  441 
fun prf_add_loose_bnos plev tlev (PBound i) (is, js) = 
17492  442 
if i < plev then (is, js) else (insert (op =) (iplev) is, js) 
12279  443 
 prf_add_loose_bnos plev tlev (prf1 %% prf2) p = 
444 
prf_add_loose_bnos plev tlev prf2 

445 
(prf_add_loose_bnos plev tlev prf1 p) 

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

447 
prf_add_loose_bnos plev tlev prf (case opt of 

17492  448 
NONE => (is, insert (op =) ~1 js) 
15531  449 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  450 
 prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = 
451 
prf_add_loose_bnos (plev+1) tlev prf (case opt of 

17492  452 
NONE => (is, insert (op =) ~1 js) 
15531  453 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  454 
 prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = 
455 
prf_add_loose_bnos plev (tlev+1) prf p 

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

457 

11519  458 

459 
(**** substitutions ****) 

460 

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

462 
(map_filter (fn ixnS as (_, S) => 
26328  463 
(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

464 
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

465 

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

467 
(map_filter (fn ixnS as (_, S) => 
32019  468 
(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

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

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

471 
(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

472 
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

473 

11519  474 
fun norm_proof env = 
475 
let 

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

477 
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

478 
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

479 
(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

480 
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

481 
(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

482 
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

483 
(msg s; f envT (map (del_conflicting_tvars envT) Ts)); 
32024  484 

32019  485 
fun norm (Abst (s, T, prf)) = 
32024  486 
(Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) 
32019  487 
handle Same.SAME => Abst (s, T, norm prf)) 
488 
 norm (AbsP (s, t, prf)) = 

32024  489 
(AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf) 
32019  490 
handle Same.SAME => AbsP (s, t, norm prf)) 
491 
 norm (prf % t) = 

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

32024  493 
handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) 
32019  494 
 norm (prf1 %% prf2) = 
495 
(norm prf1 %% Same.commit norm prf2 

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

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

32024  498 
PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
32019  499 
 norm (OfClass (T, c)) = 
500 
OfClass (htypeT Envir.norm_type_same T, c) 

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

32024  502 
Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
32019  503 
 norm (Promise (i, prop, Ts)) = 
504 
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

505 
 norm (PThm (i, ((s, t, Ts), body))) = 
32024  506 
PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts), body)) 
32019  507 
 norm _ = raise Same.SAME; 
508 
in Same.commit norm end; 

11519  509 

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

510 

11519  511 
(***** Remove some types in proof term (to save space) *****) 
512 

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

514 
 remove_types (t $ u) = remove_types t $ remove_types u 

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

516 
 remove_types t = t; 

517 

32032  518 
fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = 
39020  519 
Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; 
11519  520 

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

522 

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

523 

11519  524 
(**** substitution of bound variables ****) 
525 

526 
fun prf_subst_bounds args prf = 

527 
let 

528 
val n = length args; 

529 
fun subst' lev (Bound i) = 

32019  530 
(if i<lev then raise Same.SAME (*var is locally bound*) 
30146  531 
else incr_boundvars lev (nth args (ilev)) 
43278  532 
handle General.Subscript => Bound (in)) (*loose: change it*) 
11519  533 
 subst' lev (Abs (a, T, body)) = Abs (a, T, subst' (lev+1) body) 
534 
 subst' lev (f $ t) = (subst' lev f $ substh' lev t 

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

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

11519  538 

32057  539 
fun subst lev (AbsP (a, t, body)) = 
540 
(AbsP (a, Same.map_option (subst' lev) t, substh lev body) 

32019  541 
handle Same.SAME => AbsP (a, t, subst lev body)) 
11519  542 
 subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) 
11615  543 
 subst lev (prf %% prf') = (subst lev prf %% substh lev prf' 
32019  544 
handle Same.SAME => prf %% subst lev prf') 
15570  545 
 subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t 
32024  546 
handle Same.SAME => prf % Same.map_option (subst' lev) t) 
32019  547 
 subst _ _ = raise Same.SAME 
32024  548 
and substh lev prf = (subst lev prf handle Same.SAME => prf); 
11519  549 
in case args of [] => prf  _ => substh 0 prf end; 
550 

551 
fun prf_subst_pbounds args prf = 

552 
let 

553 
val n = length args; 

554 
fun subst (PBound i) Plev tlev = 

32019  555 
(if i < Plev then raise Same.SAME (*var is locally bound*) 
30146  556 
else incr_pboundvars Plev tlev (nth args (iPlev)) 
43278  557 
handle General.Subscript => PBound (in) (*loose: change it*)) 
11519  558 
 subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev) 
559 
 subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1)) 

11615  560 
 subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev 
32019  561 
handle Same.SAME => prf %% subst prf' Plev tlev) 
11615  562 
 subst (prf % t) Plev tlev = subst prf Plev tlev % t 
32019  563 
 subst prf _ _ = raise Same.SAME 
564 
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) 

11519  565 
in case args of [] => prf  _ => substh prf 0 0 end; 
566 

567 

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

569 

44101  570 
local 
571 

11519  572 
fun frzT names = 
44101  573 
map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); 
11519  574 

575 
fun thawT names = 

44101  576 
map_type_tfree (fn (a, S) => 
577 
(case AList.lookup (op =) names a of 

578 
NONE => TFree (a, S) 

579 
 SOME ixn => TVar (ixn, S))); 

11519  580 

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

582 
freeze names names' t $ freeze names names' u 

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

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

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

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

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

44101  588 
Free (the (AList.lookup (op =) names ixn), frzT names' T) 
11519  589 
 freeze names names' t = t; 
590 

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

592 
thaw names names' t $ thaw names names' u 

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

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

595 
 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

596 
 thaw names names' (Free (s, T)) = 
44101  597 
let val T' = thawT names' T in 
598 
(case AList.lookup (op =) names s of 

15531  599 
NONE => Free (s, T') 
44101  600 
 SOME ixn => Var (ixn, T')) 
11519  601 
end 
602 
 thaw names names' (Var (ixn, T)) = Var (ixn, thawT names' T) 

603 
 thaw names names' t = t; 

604 

44101  605 
in 
606 

11519  607 
fun freeze_thaw_prf prf = 
608 
let 

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

20147  610 
(fn t => fn (fs, Tfs, vs, Tvs) => 
29261  611 
(Term.add_free_names t fs, Term.add_tfree_names t Tfs, 
612 
Term.add_var_names t vs, Term.add_tvar_names t Tvs)) 

20147  613 
(fn T => fn (fs, Tfs, vs, Tvs) => 
29261  614 
(fs, Term.add_tfree_namesT T Tfs, 
615 
vs, Term.add_tvar_namesT T Tvs)) 

20147  616 
prf ([], [], [], []); 
29261  617 
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

618 
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); 
11519  619 
val rnames = map swap names; 
620 
val rnames' = map swap names'; 

621 
in 

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

623 
map_proof_terms (thaw rnames rnames') (thawT rnames')) 

624 
end; 

625 

44101  626 
end; 
627 

11519  628 

629 
(***** implication introduction *****) 

630 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

631 
fun gen_implies_intr_proof f h prf = 
11519  632 
let 
32019  633 
fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME 
11519  634 
 abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) 
32024  635 
 abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf) 
11615  636 
 abshyp i (prf % t) = abshyp i prf % t 
32024  637 
 abshyp i (prf1 %% prf2) = 
638 
(abshyp i prf1 %% abshyph i prf2 

639 
handle Same.SAME => prf1 %% abshyp i prf2) 

32019  640 
 abshyp _ _ = raise Same.SAME 
32024  641 
and abshyph i prf = (abshyp i prf handle Same.SAME => prf); 
11519  642 
in 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

643 
AbsP ("H", f h, abshyph 0 prf) 
11519  644 
end; 
645 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

646 
val implies_intr_proof = gen_implies_intr_proof (K NONE); 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

647 
val implies_intr_proof' = gen_implies_intr_proof SOME; 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

648 

11519  649 

650 
(***** forall introduction *****) 

651 

15531  652 
fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf); 
11519  653 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

654 
fun forall_intr_proof' t prf = 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

655 
let val (a, T) = (case t of Var ((a, _), T) => (a, T)  Free p => p) 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

656 
in Abst (a, SOME T, prf_abstract_over t prf) end; 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

657 

11519  658 

659 
(***** varify *****) 

660 

661 
fun varify_proof t fixed prf = 

662 
let 

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

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

43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

667 
val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used); 
11519  668 
fun thaw (f as (a, S)) = 
17314  669 
(case AList.lookup (op =) fmap f of 
15531  670 
NONE => TFree f 
671 
 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

672 
in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; 
11519  673 

674 

675 
local 

676 

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

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43278
diff
changeset

678 
let val v = singleton (Name.variant_list used) (string_of_indexname ix) 
11519  679 
in ((ix, v) :: pairs, v :: used) end; 
680 

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

11519  684 

685 
in 

686 

36619
deadcd0ec431
renamed Proofterm.freezeT to Proofterm.legacy_freezeT (cf. 88756a5a92fc);
wenzelm
parents:
35851
diff
changeset

687 
fun legacy_freezeT t prf = 
11519  688 
let 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

689 
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

690 
and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, [])); 
23178  691 
val (alist, _) = List.foldr new_name ([], used) tvars; 
11519  692 
in 
693 
(case alist of 

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

695 
 _ => 

696 
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

697 
in map_proof_terms (map_types frzT) frzT prf end) 
11519  698 
end; 
699 

700 
end; 

701 

702 

703 
(***** rotate assumptions *****) 

704 

705 
fun rotate_proof Bs Bi m prf = 

706 
let 

707 
val params = Term.strip_all_vars Bi; 

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

709 
val i = length asms; 

710 
val j = length Bs; 

711 
in 

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

23178  713 
(j downto 1) @ [mk_Abst params (mk_AbsP (i, 
11519  714 
proof_combP (proof_combt (PBound i, map Bound ((length params  1) downto 0)), 
23178  715 
map PBound (((im1) downto 0) @ ((i1) downto (im))))))])) 
11519  716 
end; 
717 

718 

719 
(***** permute premises *****) 

720 

36742  721 
fun permute_prems_proof prems j k prf = 
11519  722 
let val n = length prems 
723 
in mk_AbsP (n, proof_combP (prf, 

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

725 
end; 

726 

727 

19908  728 
(***** generalization *****) 
729 

20000  730 
fun generalize (tfrees, frees) idx = 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

731 
Same.commit (map_proof_terms_same 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

732 
(Term_Subst.generalize_same (tfrees, frees) idx) 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

733 
(Term_Subst.generalizeT_same tfrees idx)); 
19908  734 

735 

11519  736 
(***** instantiation *****) 
737 

20000  738 
fun instantiate (instT, inst) = 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

739 
Same.commit (map_proof_terms_same 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

740 
(Term_Subst.instantiate_same (instT, map (apsnd remove_types) inst)) 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

741 
(Term_Subst.instantiateT_same instT)); 
11519  742 

743 

744 
(***** lifting *****) 

745 

746 
fun lift_proof Bi inc prop prf = 

747 
let 

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

11519  750 

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

751 
fun lift' Us Ts (Abst (s, T, prf)) = 
32024  752 
(Abst (s, Same.map_option (Logic.incr_tvar_same inc) T, lifth' Us (dummyT::Ts) prf) 
32019  753 
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

754 
 lift' Us Ts (AbsP (s, t, prf)) = 
32024  755 
(AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) 
32019  756 
handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) 
15570  757 
 lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t 
32024  758 
handle Same.SAME => prf % Same.map_option (same (op =) (lift'' Us Ts)) t) 
11715
592923615f77
Tuned several functions to improve sharing of unchanged subproofs.
berghofe
parents:
11652
diff
changeset

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

761 
 lift' _ _ (PAxm (s, prop, Ts)) = 
32024  762 
PAxm (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) 
31943
5e960a0780a2
renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
wenzelm
parents:
31903
diff
changeset

763 
 lift' _ _ (OfClass (T, c)) = 
32024  764 
OfClass (Logic.incr_tvar_same inc T, c) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

765 
 lift' _ _ (Oracle (s, prop, Ts)) = 
32024  766 
Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) 
28828
c25dd83a6f9f
unified treatment of PAxm/Oracle/Promise in basic proof term operations;
wenzelm
parents:
28815
diff
changeset

767 
 lift' _ _ (Promise (i, prop, Ts)) = 
32024  768 
Promise (i, prop, Same.map (Logic.incr_tvar_same inc) Ts) 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

769 
 lift' _ _ (PThm (i, ((s, prop, Ts), body))) = 
32024  770 
PThm (i, ((s, prop, (Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), body)) 
32019  771 
 lift' _ _ _ = raise Same.SAME 
772 
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf); 

11519  773 

18030  774 
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); 
11519  775 
val k = length ps; 
776 

23178  777 
fun mk_app b (i, j, prf) = 
11615  778 
if b then (i1, j, prf %% PBound i) else (i, j1, prf %> Bound j); 
11519  779 

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

20147  781 
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

782 
 lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
20147  783 
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

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

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

789 
end; 

790 

32027  791 
fun incr_indexes i = 
36620
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

792 
Same.commit (map_proof_terms_same 
e6bb250402b5
simplified/unified fundamental operations on types/terms/proofterms  prefer Same.operation over "option" variant;
wenzelm
parents:
36619
diff
changeset

793 
(Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i)); 
32027  794 

11519  795 

796 
(***** proof by assumption *****) 

797 

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

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

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

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

801 
 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

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

803 
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

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

805 
in all_prf t end; 
11519  806 

807 
fun assumption_proof Bs Bi n prf = 

808 
mk_AbsP (length Bs, proof_combP (prf, 

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

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

811 

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

813 

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

15531  815 
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) 
11519  816 
 flatten_params_proof i j n (Const ("all", _) $ Abs (a, T, t), k) = 
15531  817 
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) 
11519  818 
 flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), 
19304  819 
map Bound (j1 downto 0)), map PBound (remove (op =) (in) (i1 downto 0))); 
11519  820 

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

821 
fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf = 
11519  822 
let 
823 
val la = length newAs; 

824 
val lb = length Bs; 

825 
in 

826 
mk_AbsP (lb+la, proof_combP (sprf, 

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

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

11519  831 
end; 
832 

833 

834 
(***** axioms for equality *****) 

835 

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

11519  838 
val x = Free ("x", aT); 
839 
val y = Free ("y", aT); 

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

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

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

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

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

845 

846 
val equality_axms = 

35851  847 
[("reflexive", Logic.mk_equals (x, x)), 
848 
("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), 

849 
("transitive", 

850 
Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))), 

851 
("equal_intr", 

852 
Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))), 

853 
("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)), 

854 
("abstract_rule", 

855 
Logic.mk_implies 

856 
(Logic.all x 

857 
(Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), 

858 
("combination", Logic.list_implies 

859 
([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))]; 

11519  860 

861 
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, 

862 
equal_elim_axm, abstract_rule_axm, combination_axm] = 

35851  863 
map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms; 
11519  864 

15531  865 
val reflexive = reflexive_axm % NONE; 
11519  866 

26424  867 
fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf 
15531  868 
 symmetric prf = symmetric_axm % NONE % NONE %% prf; 
11519  869 

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

11519  872 
 transitive u (Type ("prop", [])) prf1 prf2 = 
15531  873 
transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 
11519  874 
 transitive u T prf1 prf2 = 
15531  875 
transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; 
11519  876 

877 
fun abstract_rule x a prf = 

15531  878 
abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; 
11519  879 

26424  880 
fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) = 
19502  881 
is_some f orelse check_comb prf 
26424  882 
 check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = 
11519  883 
check_comb prf1 andalso check_comb prf2 
26424  884 
 check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf 
11519  885 
 check_comb _ = false; 
886 

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

888 
let 

889 
val f = Envir.beta_norm f; 

890 
val g = Envir.beta_norm g; 

44100  891 
val prf = 
892 
if check_comb prf1 then 

15531  893 
combination_axm % NONE % NONE 
44100  894 
else 
895 
(case prf1 of 

26424  896 
PAxm ("Pure.reflexive", _, _) % _ => 
15531  897 
combination_axm %> remove_types f % NONE 
11615  898 
 _ => combination_axm %> remove_types f %> remove_types g) 
11519  899 
in 
900 
(case T of 

44100  901 
Type ("fun", _) => prf % 
902 
(case head_of f of 

903 
Abs _ => SOME (remove_types t) 

904 
 Var _ => SOME (remove_types t) 

905 
 _ => NONE) % 

906 
(case head_of g of 

907 
Abs _ => SOME (remove_types u) 

908 
 Var _ => SOME (remove_types u) 

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

15531  910 
 _ => prf % NONE % NONE %% prf1 %% prf2) 
11519  911 
end; 
912 

913 
fun equal_intr A B prf1 prf2 = 

11615  914 
equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  915 

916 
fun equal_elim A B prf1 prf2 = 

11615  917 
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  918 

919 

36740  920 
(**** type classes ****) 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

921 

2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

922 
fun strip_shyps_proof algebra present witnessed extra_sorts prf = 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

923 
let 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

924 
fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; 
36732
9c2ee10809b2
strip_shyps_proof: dummy TFrees are called "'dummy" as in del_conflicting_tvars below;
wenzelm
parents:
36621
diff
changeset

925 
val extra = map (fn S => (TFree ("'dummy", S), S)) extra_sorts; 
36621
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

926 
val replacements = present @ extra @ witnessed; 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

927 
fun replace T = 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

928 
if exists (fn (T', _) => T' = T) present then raise Same.SAME 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

929 
else 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

930 
(case get_first (get (Type.sort_of_atyp T)) replacements of 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

931 
SOME T' => T' 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

932 
 NONE => raise Fail "strip_shyps_proof: bad type variable in proof term"); 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

933 
in Same.commit (map_proof_types_same (Term_Subst.map_atypsT_same replace)) prf end; 
2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

934 

2fd4e2c76636
proof terms for strip_shyps, based on the version by krauss/schropp with some notable differences:
wenzelm
parents:
36620
diff
changeset

935 

36740  936 
local 
937 

938 
type axclass_proofs = 

939 
{classrel_proof: theory > class * class > proof, 

940 
arity_proof: theory > string * sort list * class > proof}; 

941 

942 
val axclass_proofs: axclass_proofs Single_Assignment.var = 

943 
Single_Assignment.var "Proofterm.axclass_proofs"; 

944 

945 
fun axclass_proof which thy x = 

946 
(case Single_Assignment.peek axclass_proofs of 

947 
NONE => raise Fail "Axclass proof operations not installed" 

948 
 SOME prfs => which prfs thy x); 

949 

950 
in 

951 

952 
val classrel_proof = axclass_proof #classrel_proof; 

953 
val arity_proof = axclass_proof #arity_proof; 

954 

955 
fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs; 

956 

957 
end; 

958 

959 

36741
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

960 
local 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

961 

d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

962 
fun canonical_instance typs = 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

963 
let 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

964 
val names = Name.invent Name.context Name.aT (length typs); 
36741
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

965 
val instT = map2 (fn a => fn T => (((a, 0), []), Type.strip_sorts T)) names typs; 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

966 
in instantiate (instT, []) end; 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

967 

d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

968 
in 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

969 

d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

970 
fun of_sort_proof thy hyps = 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

971 
Sorts.of_sort_derivation (Sign.classes_of thy) 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

972 
{class_relation = fn typ => fn (prf, c1) => fn c2 => 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

973 
if c1 = c2 then prf 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

974 
else canonical_instance [typ] (classrel_proof thy (c1, c2)) %% prf, 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

975 
type_constructor = fn (a, typs) => fn dom => fn c => 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

976 
let val Ss = map (map snd) dom and prfs = maps (map fst) dom 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

977 
in proof_combP (canonical_instance typs (arity_proof thy (a, Ss, c)), prfs) end, 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

978 
type_variable = fn typ => map (fn c => (hyps (typ, c), c)) (Type.sort_of_atyp typ)}; 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

979 

d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

980 
end; 
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

981 

d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

982 

11519  983 
(***** axioms and theorems *****) 
984 

32738  985 
val proofs = Unsynchronized.ref 2; 
41698  986 
fun proofs_enabled () = ! proofs >= 2; 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

987 

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

988 
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

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

991 
fun test_args _ [] = true 

992 
 test_args is (Bound i :: ts) = 

17492  993 
not (member (op =) is i) andalso test_args (i :: is) ts 
11519  994 
 test_args _ _ = false; 
995 

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

997 
 is_fun (TVar _) = true 

998 
 is_fun _ = false; 

999 

1000 
fun add_funvars Ts (vs, t) = 

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

33042  1002 
union (op =) vs (map_filter (fn Var (ixn, T) => 
33037
b22e44496dc2
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
haftmann
parents:
32810
diff
changeset

1003 
if is_fun T then SOME ixn else NONE  _ => NONE) (vars_of t)) 
11519  1004 
else vs; 
1005 

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

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

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

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

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

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

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

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

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

11519  1019 

33042  1020 
fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) 
11519  1021 
 prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t 
1022 
 prop_vars t = (case strip_comb t of 

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

1024 

1025 
fun is_proj t = 

1026 
let 

1027 
fun is_p i t = (case strip_comb t of 

1028 
(Bound j, []) => false 

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

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

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

1032 
in (case strip_abs_body t of 

1033 
Bound _ => true 

1034 
 t' => is_p 0 t') 

1035 
end; 

1036 

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

1037 
fun needed_vars prop = 
33042  1038 
union (op =) (Library.foldl (uncurry (union (op =))) 
1039 
([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) 

1040 
(prop_vars prop); 

11519  1041 

1042 
fun gen_axm_proof c name prop = 

1043 
let 

1044 
val nvs = needed_vars prop; 

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

17492  1046 
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

1047 
map SOME (frees_of prop); 
11519  1048 
in 
15531  1049 
proof_combt' (c (name, prop, NONE), args) 
11519  1050 
end; 
1051 

1052 
val axm_proof = gen_axm_proof PAxm; 

17017  1053 

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

1055 

1056 
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

1057 
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

1058 
else ((name, prop), gen_axm_proof Oracle name prop); 
11519  1059 

43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1060 
fun shrink_proof thy = 
17492  1061 
let 
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1062 
val (typ, term) = Term_Sharing.init thy; 
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1063 

17492  1064 
fun shrink ls lev (prf as Abst (a, T, body)) = 
1065 
let val (b, is, ch, body') = shrink ls (lev+1) body 

43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1066 
in (b, is, ch, if ch then Abst (a, Option.map typ T, body') else prf) end 
17492  1067 
 shrink ls lev (prf as AbsP (a, t, body)) = 
1068 
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

1069 
in (b orelse member (op =) is 0, map_filter (fn 0 => NONE  i => SOME (i1)) is, 
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1070 
ch, if ch then AbsP (a, Option.map term t, body') else prf) 
17492  1071 
end 
1072 
 shrink ls lev prf = 

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

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

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

1076 
let 

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

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

33042  1079 
in (union (op =) is is', ch orelse ch', ts', 
17492  1080 
if ch orelse ch' then prf'' %% prf' else prf) 
1081 
end 

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

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

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

43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1085 
if ch orelse ch' then prf' % Option.map term t' else prf) end 
17492  1086 
 shrink' ls lev ts prfs (prf as PBound i) = 
30146  1087 
(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

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

1089 
(Library.foldl (fn (js, SOME (Bound j)) => j :: js  (js, _) => js) ([], ts)) 
17492  1090 
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) 
43795
ca5896a836ba
recovered some runtime sharing from d6b6c74a8bcf, without the global memory bottleneck;
wenzelm
parents:
43761
diff
changeset

1091 
 shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (term t)) 
31903  1092 
 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

1093 
 shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf) 
17492  1094 
 shrink' ls lev ts prfs prf = 
1095 
let 

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

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

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

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

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

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

1101 
 PThm (_, ((_, prop, _), _)) => prop 
36879
201a4afd8533
raise Fail uniformly for proofterm errors, which appear to be rather lowlevel;
wenzelm
parents:
36878
diff
changeset

1102 
 _ => raise Fail "shrink: proof not in normal form"); 
17492  1103 
val vs = vars_of prop; 
19012  1104 
val (ts', ts'') = chop (length vs) ts; 
33957  1105 
val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; 
17492  1106 
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => 
1107 
insert (op =) ixn (case AList.lookup (op =) insts ixn of 

33042  1108 
SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns' 
1109 
 _ => union (op =) ixns ixns')) 

17492  1110 
(needed prop ts'' prfs, add_npvars false true [] ([], prop)); 
1111 
val insts' = map 

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

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

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

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

33042  1116 
union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) 
17492  1117 
 needed (Var (ixn, _)) (_::_) _ = [ixn] 
1118 
 needed _ _ _ = []; 

1119 
in shrink end; 

11519  1120 

1121 

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

1123 

1124 
exception PMatch; 

1125 

1126 
(** see pattern.ML **) 

1127 

33317  1128 
fun flt (i: int) = filter (fn n => n < i); 
12279  1129 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1130 
fun fomatch Ts tymatch j instsp p = 
11519  1131 
let 
1132 
fun mtch (instsp as (tyinsts, insts)) = fn 

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

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

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

1137 
(ixn, t) :: insts) 

11519  1138 
 (Free (a, T), Free (b, U)) => 
20147  1139 
if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch 
11519  1140 
 (Const (a, T), Const (b, U)) => 
20147  1141 
if a=b then (tymatch (tyinsts, K (T, U)), insts) else raise PMatch 
11519  1142 
 (f $ t, g $ u) => mtch (mtch instsp (f, g)) (t, u) 
12279  1143 
 (Bound i, Bound j) => if i=j then instsp else raise PMatch 
11519  1144 
 _ => raise PMatch 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1145 
in mtch instsp (pairself Envir.beta_eta_contract p) end; 
11519  1146 

12279  1147 
fun match_proof Ts tymatch = 
11519  1148 
let 
15531  1149 
fun optmatch _ inst (NONE, _) = inst 
1150 
 optmatch _ _ (SOME _, NONE) = raise PMatch 

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

12279  1152 

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

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

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

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

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

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

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

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

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

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

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

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

1166 
else raise PMatch 

1167 
 _ => raise PMatch) 

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

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

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

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

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

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

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

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

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

1181 
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

1182 
 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

1183 
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

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

1185 
 mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) = 
31903  1186 
if c1 = c2 then matchT inst (T1, T2) 
1187 
else raise PMatch 

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

1188 
 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

1189 
if name1 = name2 andalso prop1 = prop2 then 
12279  1190 
optmatch matchTs inst (opTs, opUs) 
11519  1191 
else raise PMatch 
12279  1192 
 mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch 
1193 
 mtch _ _ _ _ _ = raise PMatch 

1194 
in mtch Ts 0 0 end; 

11519  1195 

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

1197 
let 

32049  1198 
val substT = Envir.subst_type_same tyinsts; 
1199 
val substTs = Same.map substT; 

11519  1200 

32049  1201 
fun subst' lev (Var (xi, _)) = 
1202 
(case AList.lookup (op =) insts xi of 

1203 
NONE => raise Same.SAME 

15531  1204 
 SOME u => incr_boundvars lev u) 
32049  1205 
 subst' _ (Const (s, T)) = Const (s, substT T) 
1206 
 subst' _ (Free (s, T)) = Free (s, substT T) 

1207 
 subst' lev (Abs (a, T, body)) = 

1208 
(Abs (a, substT T, Same.commit (subst' (lev + 1)) body) 

1209 
handle Same.SAME => Abs (a, T, subst' (lev + 1) body)) 

1210 
 subst' lev (f $ t) = 

1211 
(subst' lev f $ Same.commit (subst' lev) t 

1212 
handle Same.SAME => f $ subst' lev t) 

1213 
 subst' _ _ = raise Same.SAME; 

11519  1214 

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

32049  1216 
(AbsP (a, Same.map_option (subst' tlev) t, Same.commit (subst (plev + 1) tlev) body) 
1217 
handle Same.SAME => AbsP (a, t, subst (plev + 1) tlev body)) 

11519  1218 
 subst plev tlev (Abst (a, T, body)) = 
32049  1219 
(Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body) 
1220 
handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body)) 

1221 
 subst plev tlev (prf %% prf') = 

1222 
(subst plev tlev prf %% Same.commit (subst plev tlev) prf' 

1223 
handle Same.SAME => prf %% subst plev tlev prf') 

1224 
 subst plev tlev (prf % t) = 

1225 
(subst plev tlev prf % Same.commit (Same.map_option (subst' tlev)) t 

1226 
handle Same.SAME => prf % Same.map_option (subst' tlev) t) 

1227 
 subst plev tlev (Hyp (Var (xi, _))) = 

1228 
(case AList.lookup (op =) pinst xi of 

1229 
NONE => raise Same.SAME 

1230 
 SOME prf' => incr_pboundvars plev tlev prf') 

1231 
 subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts) 

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

1232 
 subst _ _ (OfClass (T, c)) = OfClass (substT T, c) 
32049  1233 
 subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) 
1234 
 subst _ _ (Promise (i, prop, Ts)) = Promise (i, prop, substTs Ts) 

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

1235 
 subst _ _ (PThm (i, ((id, prop, Ts), body))) = 
32049  1236 
PThm (i, ((id, prop, Same.map_option substTs Ts), body)) 
1237 
 subst _ _ _ = raise Same.SAME; 

1238 
in fn t => subst 0 0 t handle Same.SAME => t end; 

11519  1239 

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

1240 
(*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

1241 
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

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

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

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

1245 
could_unify prf2 prf2' andalso matchrands prf1 prf1' 
15531  1246 
 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

1247 
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

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

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

1250 

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

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

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

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

1254 

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

1255 
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

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

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

1258 
 (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

1259 
 (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

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

1261 
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

1262 
 (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

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

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

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

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

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

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

1269 

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

1270 

11519  1271 
(**** rewriting on proof terms ****) 
1272 

33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1273 
val no_skel = PBound 0; 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1274 
val normal_skel = Hyp (Var ((Name.uu, 0), propT)); 
13102
b6f8aae5f152
Added skeletons to speed up rewriting on proof terms.
berghofe
parents:
12923
diff
changeset

1275 

12279  1276 
fun rewrite_prf tymatch (rules, procs) prf = 
11519  1277 
let 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1278 
fun rew _ _ (Abst (_, _, body) % SOME t) = SOME (prf_subst_bounds [t] body, no_skel) 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1279 
 rew _ _ (AbsP (_, _, body) %% prf) = SOME (prf_subst_pbounds [prf] body, no_skel) 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1280 
 rew Ts hs prf = 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1281 
(case get_first (fn r => r Ts hs prf) procs of 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1282 
NONE => get_first (fn (prf1, prf2) => SOME (prf_subst 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1283 
(match_proof Ts tymatch ([], (Vartab.empty, [])) (prf1, prf)) prf2, prf2) 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1284 
handle PMatch => NONE) (filter (could_unify prf o fst) rules) 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33522
diff
changeset

1285 
 some => some); 
11519  1286 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1287 
fun rew0 Ts hs (prf as AbsP (_, _, prf' %% PBound 0)) = 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1288 
if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf 
11519  1289 
else 
1290 
let val prf'' = incr_pboundvars (~1) 0 prf' 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1291 
in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1292 
 rew0 Ts hs (prf as Abst (_, _, prf' % SOME (Bound 0))) = 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1293 
if prf_loose_bvar1 prf' 0 then rew Ts hs prf 
11519  1294 
else 
1295 
let val prf'' = incr_pboundvars 0 (~1) prf' 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1296 
in SOME (the_default (prf'', no_skel) (rew Ts hs prf'')) end 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1297 
 rew0 Ts hs prf = rew Ts hs prf; 
11519  1298 

37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1299 
fun rew1 _ _ (Hyp (Var _)) _ = NONE 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1300 
 rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1301 
SOME prf1 => (case rew0 Ts hs prf1 of 
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

1302 
SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2)) 
15531
08c8dad8e399
Deleted Library.option type.
ska
