author  wenzelm 
Sat, 20 Aug 2011 18:11:17 +0200  
changeset 44332  e10f6b873f88 
parent 44331  aa9c1e9ef2ce 
child 44333  cc53ce50f738 
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) 
44331  40 
val check_body_thms: proof_body > proof_body future 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

41 
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

42 
val join_proof: proof_body future > proof 
30711  43 
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

44 
val fold_body_thms: (string * term * proof_body > 'a > 'a) > proof_body list > 'a > 'a 
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 

44331  174 
fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms)); 
175 

176 
fun check_body_thms (body as PBody {thms, ...}) = 

177 
(singleton o Future.cond_forks) 

178 
{name = "Proofterm.check_body_thms", group = NONE, 

44332  179 
deps = map (Future.task_of o #3 o #2) thms, pri = 0, interrupts = true} 
44331  180 
(fn () => (join_thms thms; body)); 
44303
4e2abb045eac
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
wenzelm
parents:
44302
diff
changeset

181 

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

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

183 
val join_proof = Future.join #> proof_of; 
17017  184 

185 

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

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

187 

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

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

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

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

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

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

193 
 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

194 
 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

195 
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

196 
else 
28815  197 
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

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

200 
 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

201 
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

202 

30711  203 
fun fold_body_thms f = 
204 
let 

32726  205 
fun app (PBody {thms, ...}) = 
44303
4e2abb045eac
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
wenzelm
parents:
44302
diff
changeset

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

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

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

210 
val body' = Future.join body; 
32726  211 
val (x', seen') = app body' (x, Inttab.update (i, ()) seen); 
44303
4e2abb045eac
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
wenzelm
parents:
44302
diff
changeset

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

30712  215 
fun status_of bodies = 
30711  216 
let 
217 
fun status (PBody {oracles, thms, ...}) x = 

218 
let 

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

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

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

222 
else 

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

224 
(case Future.peek body of 

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

225 
SOME (Exn.Res body') => status body' (st, seen') 
30711  226 
 SOME (Exn.Exn _) => 
227 
let val (oracle, unfinished, _) = st 

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

229 
 NONE => 

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

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

232 
end); 

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

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

30711  236 
in {oracle = oracle, unfinished = unfinished, failed = failed} end; 
237 

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

238 

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

240 

35408  241 
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

242 
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

243 

39687  244 
val merge_oracles = Ord_List.union oracle_ord; 
245 
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

246 

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

247 
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

248 
let 
32057  249 
fun collect (PBody {oracles, thms, ...}) = 
44303
4e2abb045eac
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
wenzelm
parents:
44302
diff
changeset

250 
tap join_thms thms > fold (fn (i, (_, _, body)) => fn (x, seen) => 
32057  251 
if Inttab.defined seen i then (x, seen) 
252 
else 

253 
let 

254 
val body' = Future.join body; 

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

44303
4e2abb045eac
incremental Proofterm.join_body, with join_thms step in fulfill_norm_proof  avoid full graph traversal of former Proofterm.join_bodies;
wenzelm
parents:
44302
diff
changeset

256 
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

257 
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

258 

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

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

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

261 
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

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

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

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

266 
PBody 
39687  267 
{oracles = Ord_List.make oracle_ord oracles, 
268 
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

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

270 
end; 
11519  271 

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

272 

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

273 
(***** proof objects with different levels of detail *****) 
11519  274 

15531  275 
fun (prf %> t) = prf % SOME t; 
11519  276 

15570  277 
val proof_combt = Library.foldl (op %>); 
278 
val proof_combt' = Library.foldl (op %); 

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

11519  280 

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

281 
fun strip_combt prf = 
11615  282 
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

283 
 stripc x = x 
11519  284 
in stripc (prf, []) end; 
285 

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

286 
fun strip_combP prf = 
11615  287 
let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) 
11519  288 
 stripc x = x 
289 
in stripc (prf, []) end; 

290 

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

291 
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

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

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

294 
 _ => body); 
11519  295 

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

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

299 
fun map_proof_same term typ ofclass = 
20000  300 
let 
32024  301 
val typs = Same.map typ; 
20000  302 

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

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

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

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

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

309 
 proof (prf % t) = 

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

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

312 
 proof (prf1 %% prf2) = 

313 
(proof prf1 %% Same.commit proof prf2 

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

315 
 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

316 
 proof (OfClass T_c) = ofclass T_c 
32024  317 
 proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) 
318 
 proof (Promise (i, prop, Ts)) = Promise (i, prop, typs Ts) 

32057  319 
 proof (PThm (i, ((a, prop, SOME Ts), body))) = 
320 
PThm (i, ((a, prop, SOME (typs Ts)), body)) 

32024  321 
 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

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

323 

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

324 
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

325 
fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; 
20000  326 

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

328 
let val x' = f x 
32019  329 
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

330 

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

331 
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

332 
fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); 
11519  333 

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

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

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

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

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

340 
 fold_proof_terms f g (prf1 %% prf2) = 

341 
fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 

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

343 
 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

344 
 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

345 
 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

346 
 fold_proof_terms _ g (PThm (_, ((_, _, SOME Ts), _))) = fold g Ts 
20147  347 
 fold_proof_terms _ _ _ = I; 
11519  348 

20300  349 
fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf; 
12868  350 

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

353 
 size_of_proof (prf % _) = 1 + size_of_proof prf 
13744  354 
 size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 
355 
 size_of_proof _ = 1; 

356 

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

357 
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

358 
 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

359 
 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

360 
 change_type opTs (Promise _) = raise Fail "change_type: unexpected promise" 
32057  361 
 change_type opTs (PThm (i, ((name, prop, _), body))) = 
362 
PThm (i, ((name, prop, opTs), body)) 

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

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

364 

11519  365 

366 
(***** utilities *****) 

367 

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

369 
 strip_abs _ t = t; 

370 

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

373 

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

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

377 

378 
fun prf_abstract_over v = 

379 
let 

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

380 
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

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

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

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

11519  386 

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

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

390 
 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

391 
 abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 
32019  392 
handle Same.SAME => prf1 %% abst lev prf2) 
15570  393 
 abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t 
32024  394 
handle Same.SAME => prf % Same.map_option (abst' lev) t) 
32019  395 
 abst _ _ = raise Same.SAME 
32024  396 
and absth lev prf = (abst lev prf handle Same.SAME => prf); 
11519  397 

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

398 
in absth 0 end; 
11519  399 

400 

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

402 
required when moving a proof term within abstractions 

403 
inc is increment for bound variables 

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

405 

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

407 

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

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

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

413 
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

414 
 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

415 
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

416 
 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

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

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

423 
and prf_incr_bv incP inct Plev tlev prf = 
32019  424 
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); 
11519  425 

426 
fun incr_pboundvars 0 0 prf = prf 

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

428 

429 

11615  430 
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k 
15531  431 
 prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) 
432 
 prf_loose_bvar1 (_ % NONE) _ = true 

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

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

11519  435 
 prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) 
436 
 prf_loose_bvar1 _ _ = false; 

437 

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

11615  439 
 prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k 
440 
 prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k 

11519  441 
 prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) 
442 
 prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k 

443 
 prf_loose_Pbvar1 _ _ = false; 

444 

12279  445 
fun prf_add_loose_bnos plev tlev (PBound i) (is, js) = 
17492  446 
if i < plev then (is, js) else (insert (op =) (iplev) is, js) 
12279  447 
 prf_add_loose_bnos plev tlev (prf1 %% prf2) p = 
448 
prf_add_loose_bnos plev tlev prf2 

449 
(prf_add_loose_bnos plev tlev prf1 p) 

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

451 
prf_add_loose_bnos plev 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 (AbsP (_, opt, prf)) (is, js) = 
455 
prf_add_loose_bnos (plev+1) tlev prf (case opt of 

17492  456 
NONE => (is, insert (op =) ~1 js) 
15531  457 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  458 
 prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = 
459 
prf_add_loose_bnos plev (tlev+1) prf p 

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

461 

11519  462 

463 
(**** substitutions ****) 

464 

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

466 
(map_filter (fn ixnS as (_, S) => 
26328  467 
(Type.lookup envT ixnS; NONE) handle TYPE _ => 
44118
69e29cf993c0
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44116
diff
changeset

468 
SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvarsT T [])) T; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

469 

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

471 
(map_filter (fn ixnS as (_, S) => 
32019  472 
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ => 
44118
69e29cf993c0
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44116
diff
changeset

473 
SOME (ixnS, TFree ("'dummy", S))) (Term.add_tvars t []), 
69e29cf993c0
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44116
diff
changeset

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

475 
(Envir.lookup (env, ixnT); NONE) handle TYPE _ => 
44118
69e29cf993c0
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44116
diff
changeset

476 
SOME (ixnT, Free ("dummy", T))) (Term.add_vars t [])) t; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

477 

11519  478 
fun norm_proof env = 
479 
let 

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

481 
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

482 
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

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

484 
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

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

486 
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

487 
(msg s; f envT (map (del_conflicting_tvars envT) Ts)); 
32024  488 

32019  489 
fun norm (Abst (s, T, prf)) = 
32024  490 
(Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) 
32019  491 
handle Same.SAME => Abst (s, T, norm prf)) 
492 
 norm (AbsP (s, t, prf)) = 

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

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

32024  497 
handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) 
32019  498 
 norm (prf1 %% prf2) = 
499 
(norm prf1 %% Same.commit norm prf2 

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

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

32024  502 
PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
32019  503 
 norm (OfClass (T, c)) = 
504 
OfClass (htypeT Envir.norm_type_same T, c) 

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

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

509 
 norm (PThm (i, ((s, t, Ts), body))) = 
32024  510 
PThm (i, ((s, t, Same.map_option (htypeTs Envir.norm_types_same) Ts), body)) 
32019  511 
 norm _ = raise Same.SAME; 
512 
in Same.commit norm end; 

11519  513 

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

514 

11519  515 
(***** Remove some types in proof term (to save space) *****) 
516 

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

518 
 remove_types (t $ u) = remove_types t $ remove_types u 

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

520 
 remove_types t = t; 

521 

32032  522 
fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = 
39020  523 
Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; 
11519  524 

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

526 

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

527 

11519  528 
(**** substitution of bound variables ****) 
529 

530 
fun prf_subst_bounds args prf = 

531 
let 

532 
val n = length args; 

533 
fun subst' lev (Bound i) = 

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

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

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

11519  542 

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

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

555 
fun prf_subst_pbounds args prf = 

556 
let 

557 
val n = length args; 

558 
fun subst (PBound i) Plev tlev = 

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

11615  564 
 subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev 
32019  565 
handle Same.SAME => prf %% subst prf' Plev tlev) 
11615  566 
 subst (prf % t) Plev tlev = subst prf Plev tlev % t 
32019  567 
 subst prf _ _ = raise Same.SAME 
568 
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) 

11519  569 
in case args of [] => prf  _ => substh prf 0 0 end; 
570 

571 

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

573 

44101  574 
local 
575 

11519  576 
fun frzT names = 
44101  577 
map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); 
11519  578 

579 
fun thawT names = 

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

582 
NONE => TFree (a, S) 

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

11519  584 

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

586 
freeze names names' t $ freeze names names' u 

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

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

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

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

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

44101  592 
Free (the (AList.lookup (op =) names ixn), frzT names' T) 
11519  593 
 freeze names names' t = t; 
594 

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

596 
thaw names names' t $ thaw names names' u 

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

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

599 
 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

600 
 thaw names names' (Free (s, T)) = 
44101  601 
let val T' = thawT names' T in 
602 
(case AList.lookup (op =) names s of 

15531  603 
NONE => Free (s, T') 
44101  604 
 SOME ixn => Var (ixn, T')) 
11519  605 
end 
606 
 thaw names names' (Var (ixn, T)) = Var (ixn, thawT names' T) 

607 
 thaw names names' t = t; 

608 

44101  609 
in 
610 

11519  611 
fun freeze_thaw_prf prf = 
612 
let 

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

20147  614 
(fn t => fn (fs, Tfs, vs, Tvs) => 
29261  615 
(Term.add_free_names t fs, Term.add_tfree_names t Tfs, 
616 
Term.add_var_names t vs, Term.add_tvar_names t Tvs)) 

20147  617 
(fn T => fn (fs, Tfs, vs, Tvs) => 
29261  618 
(fs, Term.add_tfree_namesT T Tfs, 
619 
vs, Term.add_tvar_namesT T Tvs)) 

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

622 
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); 
11519  623 
val rnames = map swap names; 
624 
val rnames' = map swap names'; 

625 
in 

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

627 
map_proof_terms (thaw rnames rnames') (thawT rnames')) 

628 
end; 

629 

44101  630 
end; 
631 

11519  632 

633 
(***** implication introduction *****) 

634 

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

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

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

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

647 
AbsP ("H", f h, abshyph 0 prf) 
11519  648 
end; 
649 

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

650 
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

651 
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

652 

11519  653 

654 
(***** forall introduction *****) 

655 

15531  656 
fun forall_intr_proof x a prf = Abst (a, NONE, prf_abstract_over x prf); 
11519  657 

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

658 
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

659 
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

660 
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

661 

11519  662 

663 
(***** varify *****) 

664 

665 
fun varify_proof t fixed prf = 

666 
let 

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

29261  669 
val used = Name.context 
670 
> 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

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

676 
in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; 
11519  677 

678 

679 
local 

680 

44116
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

681 
fun new_name ix (pairs, used) = 
43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43278
diff
changeset

682 
let val v = singleton (Name.variant_list used) (string_of_indexname ix) 
44116
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

683 
in ((ix, v) :: pairs, v :: used) end; 
11519  684 

44116
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

685 
fun freeze_one alist (ix, sort) = 
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

686 
(case AList.lookup (op =) alist ix of 
15531  687 
NONE => TVar (ix, sort) 
688 
 SOME name => TFree (name, sort)); 

11519  689 

690 
in 

691 

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

692 
fun legacy_freezeT t prf = 
11519  693 
let 
44116
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

694 
val used = Term.add_tfree_names t []; 
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

695 
val (alist, _) = fold_rev new_name (map #1 (Term.add_tvars t [])) ([], used); 
11519  696 
in 
697 
(case alist of 

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

699 
 _ => 

44116
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

700 
let val frzT = map_type_tvar (freeze_one alist) 
c70257b4cb7e
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44113
diff
changeset

701 
in map_proof_terms (map_types frzT) frzT prf end) 
11519  702 
end; 
703 

704 
end; 

705 

706 

707 
(***** rotate assumptions *****) 

708 

709 
fun rotate_proof Bs Bi m prf = 

710 
let 

711 
val params = Term.strip_all_vars Bi; 

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

713 
val i = length asms; 

714 
val j = length Bs; 

715 
in 

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

23178  717 
(j downto 1) @ [mk_Abst params (mk_AbsP (i, 
11519  718 
proof_combP (proof_combt (PBound i, map Bound ((length params  1) downto 0)), 
23178  719 
map PBound (((im1) downto 0) @ ((i1) downto (im))))))])) 
11519  720 
end; 
721 

722 

723 
(***** permute premises *****) 

724 

36742  725 
fun permute_prems_proof prems j k prf = 
11519  726 
let val n = length prems 
727 
in mk_AbsP (n, proof_combP (prf, 

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

729 
end; 

730 

731 

19908  732 
(***** generalization *****) 
733 

20000  734 
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

735 
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

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

737 
(Term_Subst.generalizeT_same tfrees idx)); 
19908  738 

739 

11519  740 
(***** instantiation *****) 
741 

20000  742 
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

743 
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

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

745 
(Term_Subst.instantiateT_same instT)); 
11519  746 

747 

748 
(***** lifting *****) 

749 

750 
fun lift_proof Bi inc prop prf = 

751 
let 

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

11519  754 

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

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

758 
 lift' Us Ts (AbsP (s, t, prf)) = 
32024  759 
(AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) 
32019  760 
handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) 
15570  761 
 lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t 
32024  762 
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

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

765 
 lift' _ _ (PAxm (s, prop, Ts)) = 
32024  766 
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

767 
 lift' _ _ (OfClass (T, c)) = 
32024  768 
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

769 
 lift' _ _ (Oracle (s, prop, Ts)) = 
32024  770 
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

771 
 lift' _ _ (Promise (i, prop, Ts)) = 
32024  772 
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

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

11519  777 

18030  778 
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); 
11519  779 
val k = length ps; 
780 

23178  781 
fun mk_app b (i, j, prf) = 
11615  782 
if b then (i1, j, prf %% PBound i) else (i, j1, prf %> Bound j); 
11519  783 

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

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

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

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

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

793 
end; 

794 

32027  795 
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

796 
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

797 
(Logic.incr_indexes_same ([], i)) (Logic.incr_tvar_same i)); 
32027  798 

11519  799 

800 
(***** proof by assumption *****) 

801 

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

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

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

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

805 
 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

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

807 
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

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

809 
in all_prf t end; 
11519  810 

811 
fun assumption_proof Bs Bi n prf = 

812 
mk_AbsP (length Bs, proof_combP (prf, 

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

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

815 

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

817 

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

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

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

825 
fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf = 
11519  826 
let 
827 
val la = length newAs; 

828 
val lb = length Bs; 

829 
in 

830 
mk_AbsP (lb+la, proof_combP (sprf, 

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

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

11519  835 
end; 
836 

837 

838 
(***** axioms for equality *****) 

839 

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

11519  842 
val x = Free ("x", aT); 
843 
val y = Free ("y", aT); 

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

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

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

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

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

849 

850 
val equality_axms = 

35851  851 
[("reflexive", Logic.mk_equals (x, x)), 
852 
("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), 

853 
("transitive", 

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

855 
("equal_intr", 

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

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

858 
("abstract_rule", 

859 
Logic.mk_implies 

860 
(Logic.all x 

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

862 
("combination", Logic.list_implies 

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

11519  864 

865 
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, 

866 
equal_elim_axm, abstract_rule_axm, combination_axm] = 

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

15531  869 
val reflexive = reflexive_axm % NONE; 
11519  870 

26424  871 
fun symmetric (prf as PAxm ("Pure.reflexive", _, _) % _) = prf 
15531  872 
 symmetric prf = symmetric_axm % NONE % NONE %% prf; 
11519  873 

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

11519  876 
 transitive u (Type ("prop", [])) prf1 prf2 = 
15531  877 
transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 
11519  878 
 transitive u T prf1 prf2 = 
15531  879 
transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; 
11519  880 

881 
fun abstract_rule x a prf = 

15531  882 
abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf; 
11519  883 

26424  884 
fun check_comb (PAxm ("Pure.combination", _, _) % f % g % _ % _ %% prf %% _) = 
19502  885 
is_some f orelse check_comb prf 
26424  886 
 check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = 
11519  887 
check_comb prf1 andalso check_comb prf2 
26424  888 
 check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf 
11519  889 
 check_comb _ = false; 
890 

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

892 
let 

893 
val f = Envir.beta_norm f; 

894 
val g = Envir.beta_norm g; 

44100  895 
val prf = 
896 
if check_comb prf1 then 

15531  897 
combination_axm % NONE % NONE 
44100  898 
else 
899 
(case prf1 of 

26424  900 
PAxm ("Pure.reflexive", _, _) % _ => 
15531  901 
combination_axm %> remove_types f % NONE 
11615  902 
 _ => combination_axm %> remove_types f %> remove_types g) 
11519  903 
in 
904 
(case T of 

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

907 
Abs _ => SOME (remove_types t) 

908 
 Var _ => SOME (remove_types t) 

909 
 _ => NONE) % 

910 
(case head_of g of 

911 
Abs _ => SOME (remove_types u) 

912 
 Var _ => SOME (remove_types u) 

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

15531  914 
 _ => prf % NONE % NONE %% prf1 %% prf2) 
11519  915 
end; 
916 

917 
fun equal_intr A B prf1 prf2 = 

11615  918 
equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  919 

920 
fun equal_elim A B prf1 prf2 = 

11615  921 
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 
11519  922 

923 

36740  924 
(**** 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

925 

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

926 
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

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

928 
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

929 
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

930 
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

931 
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

932 
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

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

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

935 
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

936 
 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

937 
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

938 

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

939 

36740  940 
local 
941 

942 
type axclass_proofs = 

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

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

945 

946 
val axclass_proofs: axclass_proofs Single_Assignment.var = 

947 
Single_Assignment.var "Proofterm.axclass_proofs"; 

948 

949 
fun axclass_proof which thy x = 

950 
(case Single_Assignment.peek axclass_proofs of 

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

952 
 SOME prfs => which prfs thy x); 

953 

954 
in 

955 

956 
val classrel_proof = axclass_proof #classrel_proof; 

957 
val arity_proof = axclass_proof #arity_proof; 

958 

959 
fun install_axclass_proofs prfs = Single_Assignment.assign axclass_proofs prfs; 

960 

961 
end; 

962 

963 

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

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

965 

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

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

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

968 
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

969 
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

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

971 

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

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

973 

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

974 
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

975 
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

976 
{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

977 
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

978 
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

979 
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

980 
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

981 
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

982 
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

983 

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

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

985 

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

986 

11519  987 
(***** axioms and theorems *****) 
988 

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

991 

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

992 
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

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

995 
fun test_args _ [] = true 

996 
 test_args is (Bound i :: ts) = 

17492  997 
not (member (op =) is i) andalso test_args (i :: is) ts 
11519  998 
 test_args _ _ = false; 
999 

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

1001 
 is_fun (TVar _) = true 

1002 
 is_fun _ = false; 

1003 

1004 
fun add_funvars Ts (vs, t) = 

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

33042  1006 
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

1007 
if is_fun T then SOME ixn else NONE  _ => NONE) (vars_of t)) 
11519  1008 
else vs; 
1009 

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

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

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

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

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

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

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

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

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

11519  1023 

33042  1024 
fun prop_vars (Const ("==>", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) 
11519  1025 
 prop_vars (Const ("all", _) $ Abs (_, _, t)) = prop_vars t 
1026 
 prop_vars t = (case strip_comb t of 

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

1028 

1029 
fun is_proj t = 

1030 
let 

1031 
fun is_p i t = (case strip_comb t of 

1032 
(Bound j, []) => false 

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

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

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

1036 
in (case strip_abs_body t of 

1037 
Bound _ => true 

1038 
 t' => is_p 0 t') 

1039 
end; 

1040 

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

1041 
fun needed_vars prop = 
33042  1042 
union (op =) (Library.foldl (uncurry (union (op =))) 
1043 
([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) 

1044 
(prop_vars prop); 

11519  1045 

1046 
fun gen_axm_proof c name prop = 

1047 
let 

1048 
val nvs = needed_vars prop; 

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

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

1051 
map SOME (frees_of prop); 
11519  1052 
in 
15531  1053 
proof_combt' (c (name, prop, NONE), args) 
11519  1054 
end; 
1055 

1056 
val axm_proof = gen_axm_proof PAxm; 

17017  1057 

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

1059 

1060 
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

1061 
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

1062 
else ((name, prop), gen_axm_proof Oracle name prop); 
11519  1063 

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

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

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

1067 

17492  1068 
fun shrink ls lev (prf as Abst (a, T, body)) = 
1069 
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

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

1073 
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

1074 
ch, if ch then AbsP (a, Option.map term t, body') else prf) 
17492  1075 
end 
1076 
 shrink ls lev prf = 

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

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

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

1080 
let 

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

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

33042  1083 
in (union (op =) is is', ch orelse ch', ts', 
17492  1084 
if ch orelse ch' then prf'' %% prf' else prf) 
1085 
end 

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

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

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

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

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

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

1093 
(Library.foldl (fn (js, SOME (Bound j)) => j :: js  (js, _) => js) ([], ts)) 
17492  1094 
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

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

1097 
 shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf) 
17492  1098 
 shrink' ls lev ts prfs prf = 
1099 
let 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1123 
in shrink end; 

11519  1124 

1125 

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

1127 

1128 
exception PMatch; 

1129 

1130 
(** see pattern.ML **) 

1131 

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

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

1134 
fun fomatch Ts tymatch j instsp p = 
11519  1135 
let 
1136 
fun mtch (instsp as (tyinsts, insts)) = fn 

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

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

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

1141 
(ixn, t) :: insts) 

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

1149 
in mtch instsp (pairself Envir.beta_eta_contract p) end; 
11519  1150 

12279  1151 
fun match_proof Ts tymatch = 
11519  1152 
let 
15531  1153 
fun optmatch _ inst (NONE, _) = inst 
1154 
 optmatch _ _ (SOME _, NONE) = raise PMatch 

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

12279  1156 

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

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

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

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

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

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

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

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

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

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

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

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

1170 
else raise PMatch 

1171 
 _ => raise PMatch) 

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

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

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

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

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

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

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

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

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

1185 
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

1186 
 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

1187 
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

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

1189 
 mtch Ts i j inst (OfClass (T1, c1), OfClass (T2, c2)) = 
31903  1190 
if c1 = c2 then matchT inst (T1, T2) 
1191 
else raise PMatch 

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

1192 
 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

1193 
if name1 = name2 andalso prop1 = prop2 then 
12279  1194 
optmatch matchTs inst (opTs, opUs) 
11519  1195 
else raise PMatch 
12279  1196 
 mtch _ _ _ inst (PBound i, PBound j) = if i = j then inst else raise PMatch 
1197 
 mtch _ _ _ _ _ = raise PMatch 

1198 
in mtch Ts 0 0 end; 

11519  1199 

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

1201 
let 

32049  1202 
val substT = Envir.subst_type_same tyinsts; 
1203 
val substTs = Same.map substT; 

11519  1204 

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

1207 
NONE => raise Same.SAME 

15531  1208 
 SOME u => incr_boundvars lev u) 
32049  1209 
 subst' _ (Const (s, T)) = Const (s, substT T) 
1210 
 subst' _ (Free (s, T)) = Free (s, substT T) 

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

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

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

1214 
 subst' lev (f $ t) = 

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

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

1217 
 subst' _ _ = raise Same.SAME; 

11519  1218 

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

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

11519  1222 
 subst plev tlev (Abst (a, T, body)) = 
32049  1223 
(Abst (a, Same.map_option substT T, Same.commit (subst plev (tlev + 1)) body) 
1224 
handle Same.SAME => Abst (a, T, subst plev (tlev + 1) body)) 

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

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

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

1228 
 subst plev tlev (prf % t) = 

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

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

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

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

1233 
NONE => raise Same.SAME 

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

1235 
 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

1236 
 subst _ _ (OfClass (T, c)) = OfClass (substT T, c) 
32049  1237 
 subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts) 
1238 
 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

1239 
 subst _ _ (PThm (i, ((id, prop, Ts), body))) = 
32049  1240 
PThm (i, ((id, prop, Same.map_option substTs Ts), body)) 
1241 
 subst _ _ _ = raise Same.SAME; 

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

11519  1243 

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

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

1245 
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

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

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

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

1249 
could_unify prf2 prf2' andalso matchrands prf1 prf1' 
15531  1250 
 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

1251 
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

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

1253 
 matchrands _ _ = true 
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 
fun head_of (prf %% _) = head_of prf 
21486a0557d1
Added function could_unify to speed up rewriting of proof terms.
berghofe
parents:
12868
diff
changeset

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

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

1258 

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

1259 
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

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

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

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

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

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

1265 
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

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

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

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

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

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

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

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

1273 

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

1274 

11519  1275 
(**** rewriting on proof terms ****) 
1276 

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

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

1278 
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

1279 

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

1282 
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

1283 
 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

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

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

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

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

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

1289 
 some => some); 
11519  1290 

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

1291 
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

1292 
if prf_loose_Pbvar1 prf' 0 then rew Ts hs prf 
11519  1293 
else 
1294 
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

1295 
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

1296 
 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

1297 
if prf_loose_bvar1 prf' 0 then rew Ts hs prf 
11519  1298 
else 
1299 
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

1300 
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

1301 
 rew0 Ts hs prf = rew Ts hs prf; 
11519  < 