author  wenzelm 
Wed, 09 Oct 2019 23:00:12 +0200  
changeset 70815  a74ab9230cb3 
parent 70814  a6644dfe8e26 
child 70822  22e2f5acc0b4 
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 

70578  9 
signature PROOFTERM = 
11519  10 
sig 
70493  11 
type thm_header = 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

12 
{serial: serial, pos: Position.T list, theory_name: string, name: string, 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

13 
prop: term, types: typ list option} 
70493  14 
type thm_body 
70587  15 
type thm_node 
11519  16 
datatype proof = 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

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

18 
 PBound of int 
11519  19 
 Abst of string * typ option * proof 
20 
 AbsP of string * term option * proof 

63857  21 
 % of proof * term option 
22 
 %% of proof * proof 

11519  23 
 Hyp of term 
24 
 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

25 
 OfClass of typ * class 
70559  26 
 Oracle of string * term option * typ list option 
70493  27 
 PThm of thm_header * thm_body 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

28 
and proof_body = PBody of 
70559  29 
{oracles: (string * term option) Ord_List.T, 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

30 
thms: (serial * thm_node) Ord_List.T, 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

31 
proof: proof} 
70587  32 
type oracle = string * term option 
70590  33 
type thm = serial * thm_node 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

34 
val proof_of: proof_body > proof 
70587  35 
val join_proof: proof_body future > proof 
70396  36 
val map_proof_of: (proof > proof) > proof_body > proof_body 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

37 
val thm_header: serial > Position.T list > string > string > term > typ list option > 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

38 
thm_header 
70501  39 
val thm_body: proof_body > thm_body 
70493  40 
val thm_body_proof_raw: thm_body > proof 
41 
val thm_body_proof_open: thm_body > proof 

70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

42 
val thm_node_theory_name: thm_node > string 
64573  43 
val thm_node_name: thm_node > string 
44 
val thm_node_prop: thm_node > term 

45 
val thm_node_body: thm_node > proof_body future 

70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

46 
val thm_node_thms: thm_node > thm list 
70590  47 
val join_thms: thm list > proof_body list 
70587  48 
val consolidate: proof_body list > unit 
70590  49 
val make_thm: thm_header > thm_body > thm 
30711  50 
val fold_proof_atoms: bool > (proof > 'a > 'a) > proof list > 'a > 'a 
70413  51 
val fold_body_thms: 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

52 
({serial: serial, name: string, prop: term, body: proof_body} > 'a > 'a) > 
64572  53 
proof_body list > 'a > 'a 
70586  54 
val oracle_ord: oracle ord 
70590  55 
val thm_ord: thm ord 
44334  56 
val unions_oracles: oracle Ord_List.T list > oracle Ord_List.T 
70590  57 
val unions_thms: thm Ord_List.T list > thm Ord_List.T 
70440  58 
val no_proof_body: proof > proof_body 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

59 
val no_thm_proofs: proof > proof 
70440  60 
val no_body_proofs: proof > proof 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

61 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

62 
val encode: Consts.T > proof XML.Encode.T 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

63 
val encode_body: Consts.T > proof_body XML.Encode.T 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

64 
val encode_full: Consts.T > proof XML.Encode.T 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

65 
val decode: Consts.T > proof XML.Decode.T 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

66 
val decode_body: Consts.T > proof_body XML.Decode.T 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

67 

70587  68 
val %> : proof * term > proof 
69 

70397  70 
(*primitive operations*) 
70587  71 
val proofs: int Unsynchronized.ref 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

72 
val proofs_enabled: unit > bool 
64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

73 
val atomic_proof: proof > bool 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

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

75 
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

76 
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

77 
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

78 
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

79 
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

80 
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

81 
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

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

83 
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

84 
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

85 
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

86 
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

87 
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

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

89 
val size_of_proof: proof > int 
70417  90 
val change_types: typ list option > proof > proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

91 
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

92 
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

93 
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

94 
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

95 
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

96 
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

97 
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

98 
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

99 
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

100 
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

101 
val freeze_thaw_prf: proof > proof * (proof > proof) 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

102 
val proofT: typ 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

103 
val term_of_proof: proof > term 
11519  104 

70397  105 
(*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

106 
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

107 
val implies_intr_proof': term > proof > proof 
70814  108 
val forall_intr_proof: string * term > typ option > proof > proof 
37231
e5419ecf92b7
 outer_constraints with original variable names, to ensure that argsP is consistent with args
berghofe
parents:
36883
diff
changeset

109 
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

110 
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

111 
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

112 
val rotate_proof: term list > term > int > proof > proof 
36742  113 
val permute_prems_proof: term list > int > int > proof > proof 
19908  114 
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

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

117 
val lift_proof: term > int > term > proof > proof 
32027  118 
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

119 
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

120 
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

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

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

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

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

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

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

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

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

129 
val combination_axm: proof 
70814  130 
val reflexive_proof: proof 
131 
val symmetric_proof: proof > proof 

132 
val transitive_proof: typ > term > proof > proof > proof 

133 
val equal_intr_proof: term > term > proof > proof > proof 

134 
val equal_elim_proof: term > term > proof > proof > proof 

135 
val abstract_rule_proof: string * term > proof > proof 

136 
val combination_proof: typ > term > term > 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

137 
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

138 
sort list > proof > proof 
70458  139 
val of_sort_proof: Sorts.algebra > 
140 
(class * class > proof) > 

141 
(string * class list list * class > proof) > 

142 
(typ * class > proof) > typ * sort > proof list 

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

143 
val axm_proof: string > term > proof 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

144 
val oracle_proof: string > term > oracle * proof 
63623  145 
val shrink_proof: proof > proof 
11519  146 

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

148 
val add_prf_rrule: proof * proof > theory > theory 
52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

149 
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

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

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

152 
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

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

154 
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

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

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

157 

70449  158 
val reconstruct_proof: theory > term > proof > proof 
70447
755d58b48cec
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
wenzelm
parents:
70442
diff
changeset

159 
val prop_of': term list > proof > term 
755d58b48cec
clarified modules: provide reconstruct_proof / expand_proof at the bottom of proof term construction;
wenzelm
parents:
70442
diff
changeset

160 
val prop_of: proof > term 
70449  161 
val expand_proof: theory > (string * term option) list > proof > proof 
70400
65bbef66e2ec
clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
wenzelm
parents:
70399
diff
changeset

162 

70541
f3fbc7f3559d
more careful treatment of hidden type variable names: smash before zero_var_indexes to get standard enumeration;
wenzelm
parents:
70540
diff
changeset

163 
val standard_vars: Name.context > term * proof option > term * proof option 
70529  164 
val standard_vars_term: Name.context > term > term 
165 

70604  166 
val export_enabled: unit > bool 
36877
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

167 
val fulfill_norm_proof: theory > (serial * proof_body) list > proof_body > proof_body 
70458  168 
val thm_proof: theory > (class * class > proof) > 
70494  169 
(string * class list list * class > proof) > string * Position.T > sort list > 
70590  170 
term list > term > (serial * proof_body future) list > proof_body > thm * proof 
70458  171 
val unconstrain_thm_proof: theory > (class * class > proof) > 
172 
(string * class list list * class > proof) > sort list > term > 

70590  173 
(serial * proof_body future) list > proof_body > thm * proof 
70554  174 
val get_approximative_name: sort list > term list > term > proof > string 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

175 
type thm_id = {serial: serial, theory_name: string} 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

176 
val thm_id: thm > thm_id 
70554  177 
val get_id: sort list > term list > term > proof > thm_id option 
11519  178 
end 
179 

180 
structure Proofterm : PROOFTERM = 

181 
struct 

182 

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

184 

70493  185 
type thm_header = 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

186 
{serial: serial, pos: Position.T list, theory_name: string, name: string, 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

187 
prop: term, types: typ list option}; 
70493  188 

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

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

191 
 PBound of int 
11519  192 
 Abst of string * typ option * proof 
193 
 AbsP of string * term option * proof 

12497  194 
 op % of proof * term option 
195 
 op %% of proof * proof 

11519  196 
 Hyp of term 
197 
 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

198 
 OfClass of typ * class 
70559  199 
 Oracle of string * term option * typ list option 
70493  200 
 PThm of thm_header * thm_body 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

201 
and proof_body = PBody of 
70559  202 
{oracles: (string * term option) Ord_List.T, 
70577
ed651a58afe4
back to uniform serial (reverting 913b4afb6ac2): this allows to treat derivation id like name space entity id;
wenzelm
parents:
70573
diff
changeset

203 
thms: (serial * thm_node) Ord_List.T, 
64573  204 
proof: proof} 
70493  205 
and thm_body = 
70502
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

206 
Thm_Body of {export_proof: unit lazy, open_proof: proof > proof, body: proof_body future} 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

207 
and thm_node = 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

208 
Thm_Node of {theory_name: string, name: string, prop: term, 
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

209 
body: proof_body future, consolidate: unit lazy}; 
11519  210 

70559  211 
type oracle = string * term option; 
70591  212 
val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord); 
70559  213 
val oracle_prop = the_default Term.dummy; 
214 

70590  215 
type thm = serial * thm_node; 
70593  216 
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); 
28815  217 

70587  218 

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

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

220 
val join_proof = Future.join #> proof_of; 
17017  221 

70396  222 
fun map_proof_of f (PBody {oracles, thms, proof}) = 
223 
PBody {oracles = oracles, thms = thms, proof = f proof}; 

224 

70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

225 
fun thm_header serial pos theory_name name prop types : thm_header = 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

226 
{serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; 
70493  227 

70502
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

228 
val no_export_proof = Lazy.value (); 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

229 

b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

230 
fun thm_body body = 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

231 
Thm_Body {export_proof = no_export_proof, open_proof = I, body = Future.value body}; 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

232 
fun thm_body_export_proof (Thm_Body {export_proof, ...}) = export_proof; 
70493  233 
fun thm_body_proof_raw (Thm_Body {body, ...}) = join_proof body; 
70502
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

234 
fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body); 
70493  235 

64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

236 
fun rep_thm_node (Thm_Node args) = args; 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

237 
val thm_node_theory_name = #theory_name o rep_thm_node; 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

238 
val thm_node_name = #name o rep_thm_node; 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

239 
val thm_node_prop = #prop o rep_thm_node; 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

240 
val thm_node_body = #body o rep_thm_node; 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

241 
val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

242 
val thm_node_consolidate = #consolidate o rep_thm_node; 
64573  243 

70590  244 
fun join_thms (thms: thm list) = 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

245 
Future.joins (map (thm_node_body o #2) thms); 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

246 

66168  247 
val consolidate = 
248 
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms) 

67669  249 
#> Lazy.consolidate #> map Lazy.force #> ignore; 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

250 

70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

251 
fun make_thm_node theory_name name prop body = 
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

252 
Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body, 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

253 
consolidate = 
66167  254 
Lazy.lazy_name "Proofterm.make_thm_node" (fn () => 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

255 
let val PBody {thms, ...} = Future.join body 
66168  256 
in consolidate (join_thms thms) end)}; 
44333
cc53ce50f738
reverted to join_bodies/join_proofs based on fold_body_thms to regain performance (escpecially of HOLProofs)  see also aa9c1e9ef2ce and 4e2abb045eac;
wenzelm
parents:
44332
diff
changeset

257 

70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

258 
fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) = 
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

259 
(serial, make_thm_node theory_name name prop body); 
70589  260 

17017  261 

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

263 

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

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

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

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

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

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

269 
 app (prf1 %% prf2) = app prf1 #> app prf2 
70493  270 
 app (prf as PThm ({serial = i, ...}, Thm_Body {body, ...})) = (fn (x, seen) => 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

271 
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

272 
else 
28815  273 
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

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

276 
 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

277 
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

278 

30711  279 
fun fold_body_thms f = 
280 
let 

32726  281 
fun app (PBody {thms, ...}) = 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

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

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

285 
let 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

286 
val name = thm_node_name thm_node; 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

287 
val prop = thm_node_prop thm_node; 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

288 
val body = Future.join (thm_node_body thm_node); 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

289 
val (x', seen') = app body (x, Inttab.update (i, ()) seen); 
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

290 
in (f {serial = i, name = name, prop = prop, body = body} x', seen') end); 
32726  291 
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; 
30711  292 

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

293 

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

295 

44334  296 
val unions_oracles = Ord_List.unions oracle_ord; 
297 
val unions_thms = Ord_List.unions thm_ord; 

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

298 

70440  299 
fun no_proof_body proof = PBody {oracles = [], thms = [], proof = proof}; 
70502
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

300 
val no_thm_body = thm_body (no_proof_body MinProof); 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

301 

70493  302 
fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf) 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

303 
 no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf) 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

304 
 no_thm_proofs (prf % t) = no_thm_proofs prf % t 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

305 
 no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 
70493  306 
 no_thm_proofs (PThm (header, _)) = PThm (header, no_thm_body) 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

307 
 no_thm_proofs a = a; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

308 

70493  309 
fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf) 
70440  310 
 no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) 
311 
 no_body_proofs (prf % t) = no_body_proofs prf % t 

312 
 no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 

70502
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

313 
 no_body_proofs (PThm (header, Thm_Body {export_proof, open_proof, body})) = 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

314 
let 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

315 
val body' = Future.value (no_proof_body (join_proof body)); 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

316 
val thm_body' = Thm_Body {export_proof = export_proof, open_proof = open_proof, body = body'}; 
b053c9ed0b0a
more careful export of unnamed proof boxes: avoid duplicates via memoing;
wenzelm
parents:
70501
diff
changeset

317 
in PThm (header, thm_body') end 
70440  318 
 no_body_proofs a = a; 
319 

52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

320 

70397  321 

322 
(** XML data representation **) 

52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

323 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

324 
(* encode *) 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

325 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

326 
local 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

327 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

328 
open XML.Encode Term_XML.Encode; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

329 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

330 
fun proof consts prf = prf > variant 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

331 
[fn MinProof => ([], []), 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

332 
fn PBound a => ([int_atom a], []), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

333 
fn Abst (a, b, c) => ([a], pair (option typ) (proof consts) (b, c)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

334 
fn AbsP (a, b, c) => ([a], pair (option (term consts)) (proof consts) (b, c)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

335 
fn a % b => ([], pair (proof consts) (option (term consts)) (a, b)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

336 
fn a %% b => ([], pair (proof consts) (proof consts) (a, b)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

337 
fn Hyp a => ([], term consts a), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

338 
fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)), 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

339 
fn OfClass (a, b) => ([b], typ a), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

340 
fn Oracle (a, b, c) => ([a], pair (option (term consts)) (option (list typ)) (b, c)), 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

341 
fn PThm ({serial, pos, theory_name, name, prop, types}, Thm_Body {open_proof, body, ...}) => 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

342 
([int_atom serial, theory_name, name], 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

343 
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) 
70497  344 
(map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))] 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

345 
and proof_body consts (PBody {oracles, thms, proof = prf}) = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

346 
triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

347 
(oracles, thms, prf) 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

348 
and thm consts (a, thm_node) = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

349 
pair int (pair string (pair string (pair (term consts) (proof_body consts)))) 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

350 
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node, 
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

351 
(Future.join (thm_node_body thm_node)))))); 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

352 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

353 
fun full_proof consts prf = prf > variant 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

354 
[fn MinProof => ([], []), 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

355 
fn PBound a => ([int_atom a], []), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

356 
fn Abst (a, SOME b, c) => ([a], pair typ (full_proof consts) (b, c)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

357 
fn AbsP (a, SOME b, c) => ([a], pair (term consts) (full_proof consts) (b, c)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

358 
fn a % SOME b => ([], pair (full_proof consts) (term consts) (a, b)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

359 
fn a %% b => ([], pair (full_proof consts) (full_proof consts) (a, b)), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

360 
fn Hyp a => ([], term consts a), 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

361 
fn PAxm (name, _, SOME Ts) => ([name], list typ Ts), 
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

362 
fn OfClass (T, c) => ([c], typ T), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

363 
fn Oracle (name, prop, SOME Ts) => ([name], pair (option (term consts)) (list typ) (prop, Ts)), 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

364 
fn PThm ({serial, theory_name, name, types = SOME Ts, ...}, _) => 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

365 
([int_atom serial, theory_name, name], list typ Ts)]; 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

366 

52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

367 
in 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

368 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

369 
val encode = proof; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

370 
val encode_body = proof_body; 
70534
fb876ebbf5a7
export facts with reconstructed proof term (if possible), but its PThm boxes need to be collected separately;
wenzelm
parents:
70531
diff
changeset

371 
val encode_full = full_proof; 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

372 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

373 
end; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

374 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

375 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

376 
(* decode *) 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

377 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

378 
local 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

379 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

380 
open XML.Decode Term_XML.Decode; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

381 

70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

382 
fun proof consts prf = prf > variant 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

383 
[fn ([], []) => MinProof, 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

384 
fn ([a], []) => PBound (int_atom a), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

385 
fn ([a], b) => let val (c, d) = pair (option typ) (proof consts) b in Abst (a, c, d) end, 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

386 
fn ([a], b) => let val (c, d) = pair (option (term consts)) (proof consts) b in AbsP (a, c, d) end, 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

387 
fn ([], a) => op % (pair (proof consts) (option (term consts)) a), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

388 
fn ([], a) => op %% (pair (proof consts) (proof consts) a), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

389 
fn ([], a) => Hyp (term consts a), 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

390 
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end, 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

391 
fn ([b], a) => OfClass (typ a, b), 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

392 
fn ([a], b) => 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

393 
let val (c, d) = pair (option (term consts)) (option (list typ)) b in Oracle (a, c, d) end, 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

394 
fn ([a, b, c], d) => 
70497  395 
let 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

396 
val ((e, (f, (g, h)))) = 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

397 
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) d; 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

398 
val header = thm_header (int_atom a) (map Position.of_properties e) b c f g; 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

399 
in PThm (header, thm_body h) end] 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

400 
and proof_body consts x = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

401 
let 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

402 
val (a, b, c) = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

403 
triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x; 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

404 
in PBody {oracles = a, thms = b, proof = c} end 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

405 
and thm consts x = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

406 
let 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

407 
val (a, (b, (c, (d, e)))) = 
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

408 
pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

409 
in (a, make_thm_node b c d (Future.value e)) end; 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

410 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

411 
in 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

412 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

413 
val decode = proof; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

414 
val decode_body = proof_body; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

415 

77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

416 
end; 
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

417 

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

418 

70397  419 
(** proof objects with different levels of detail **) 
11519  420 

70587  421 
val proofs = Unsynchronized.ref 2; 
422 
fun proofs_enabled () = ! proofs >= 2; 

423 

64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

424 
fun atomic_proof prf = 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

425 
(case prf of 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

426 
Abst _ => false 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

427 
 AbsP _ => false 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

428 
 op % _ => false 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

429 
 op %% _ => false 
70402
29d81b53c40b
treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
wenzelm
parents:
70400
diff
changeset

430 
 MinProof => false 
64568
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

431 
 _ => true); 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

432 

a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

433 
fun compact_proof (prf % _) = compact_proof prf 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

434 
 compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

435 
 compact_proof prf = atomic_proof prf; 
a504a3dec35a
more careful derivation_closed / close_derivation;
wenzelm
parents:
64566
diff
changeset

436 

15531  437 
fun (prf %> t) = prf % SOME t; 
11519  438 

15570  439 
val proof_combt = Library.foldl (op %>); 
440 
val proof_combt' = Library.foldl (op %); 

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

11519  442 

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

443 
fun strip_combt prf = 
11615  444 
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

445 
 stripc x = x 
11519  446 
in stripc (prf, []) end; 
447 

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

448 
fun strip_combP prf = 
11615  449 
let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) 
11519  450 
 stripc x = x 
451 
in stripc (prf, []) end; 

452 

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

453 
fun strip_thm (body as PBody {proof, ...}) = 
70493  454 
(case fst (strip_combt (fst (strip_combP proof))) of 
455 
PThm (_, Thm_Body {body = body', ...}) => Future.join body' 

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

456 
 _ => body); 
11519  457 

63857  458 
val mk_Abst = fold_rev (fn (s, _: typ) => fn prf => Abst (s, NONE, prf)); 
15531  459 
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf; 
11519  460 

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

461 
fun map_proof_same term typ ofclass = 
20000  462 
let 
32024  463 
val typs = Same.map typ; 
20000  464 

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

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

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

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

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

471 
 proof (prf % t) = 

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

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

474 
 proof (prf1 %% prf2) = 

475 
(proof prf1 %% Same.commit proof prf2 

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

477 
 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

478 
 proof (OfClass T_c) = ofclass T_c 
32024  479 
 proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts)) 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

480 
 proof (PThm ({serial, pos, theory_name, name, prop, types = SOME Ts}, thm_body)) = 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

481 
PThm (thm_header serial pos theory_name name prop (SOME (typs Ts)), thm_body) 
32024  482 
 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

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

484 

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

485 
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

486 
fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; 
20000  487 

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

489 
let val x' = f x 
32019  490 
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

491 

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

492 
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

493 
fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); 
11519  494 

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

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

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

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

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

501 
 fold_proof_terms f g (prf1 %% prf2) = 

502 
fold_proof_terms f g prf1 #> fold_proof_terms f g prf2 

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

504 
 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

505 
 fold_proof_terms _ g (Oracle (_, _, SOME Ts)) = fold g Ts 
70493  506 
 fold_proof_terms _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts 
20147  507 
 fold_proof_terms _ _ _ = I; 
11519  508 

20300  509 
fun maxidx_proof prf = fold_proof_terms Term.maxidx_term Term.maxidx_typ prf; 
12868  510 

13744  511 
fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf 
63857  512 
 size_of_proof (AbsP (_, _, 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

513 
 size_of_proof (prf % _) = 1 + size_of_proof prf 
13744  514 
 size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 
515 
 size_of_proof _ = 1; 

516 

70417  517 
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types) 
518 
 change_types (SOME [T]) (OfClass (_, c)) = OfClass (T, c) 

519 
 change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types) 

70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

520 
 change_types types (PThm ({serial, pos, theory_name, name, prop, types = _}, thm_body)) = 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

521 
PThm (thm_header serial pos theory_name name prop types, thm_body) 
70417  522 
 change_types _ prf = prf; 
12907
27e6d344d724
New function change_type for changing type assignments of theorems,
berghofe
parents:
12890
diff
changeset

523 

11519  524 

70397  525 
(* utilities *) 
11519  526 

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

528 
 strip_abs _ t = t; 

529 

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

532 

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

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

536 

537 
fun prf_abstract_over v = 

538 
let 

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

539 
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

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

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

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

11519  545 

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

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

549 
 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

550 
 abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 
32019  551 
handle Same.SAME => prf1 %% abst lev prf2) 
15570  552 
 abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t 
32024  553 
handle Same.SAME => prf % Same.map_option (abst' lev) t) 
32019  554 
 abst _ _ = raise Same.SAME 
32024  555 
and absth lev prf = (abst lev prf handle Same.SAME => prf); 
11519  556 

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

557 
in absth 0 end; 
11519  558 

559 

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

561 
required when moving a proof term within abstractions 

562 
inc is increment for bound variables 

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

564 

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

566 

63857  567 
fun prf_incr_bv' incP _ Plev _ (PBound i) = 
32019  568 
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

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

572 
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

573 
 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

574 
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

575 
 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

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

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

582 
and prf_incr_bv incP inct Plev tlev prf = 
32019  583 
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); 
11519  584 

585 
fun incr_pboundvars 0 0 prf = prf 

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

587 

588 

11615  589 
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k 
15531  590 
 prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) 
591 
 prf_loose_bvar1 (_ % NONE) _ = true 

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

63857  593 
 prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true 
11519  594 
 prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) 
595 
 prf_loose_bvar1 _ _ = false; 

596 

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

11615  598 
 prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k 
599 
 prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k 

11519  600 
 prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) 
601 
 prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k 

602 
 prf_loose_Pbvar1 _ _ = false; 

603 

63857  604 
fun prf_add_loose_bnos plev _ (PBound i) (is, js) = 
17492  605 
if i < plev then (is, js) else (insert (op =) (iplev) is, js) 
12279  606 
 prf_add_loose_bnos plev tlev (prf1 %% prf2) p = 
607 
prf_add_loose_bnos plev tlev prf2 

608 
(prf_add_loose_bnos plev tlev prf1 p) 

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

64566  610 
prf_add_loose_bnos plev tlev prf 
611 
(case opt of 

17492  612 
NONE => (is, insert (op =) ~1 js) 
15531  613 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  614 
 prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = 
64566  615 
prf_add_loose_bnos (plev+1) tlev prf 
616 
(case opt of 

17492  617 
NONE => (is, insert (op =) ~1 js) 
15531  618 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  619 
 prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = 
620 
prf_add_loose_bnos plev (tlev+1) prf p 

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

622 

11519  623 

70397  624 
(* substitutions *) 
11519  625 

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

627 
(map_filter (fn ixnS as (_, S) => 
26328  628 
(Type.lookup envT ixnS; NONE) handle TYPE _ => 
70811
785a2112f861
clarified signature  some operations to support fully explicit proof terms;
wenzelm
parents:
70810
diff
changeset

629 
SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvarsT T [])) T; 
18316
4b62e0cb3aa8
Improved norm_proof to handle proofs containing term (type) variables
berghofe
parents:
18030
diff
changeset

630 

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

632 
(map_filter (fn ixnS as (_, S) => 
32019  633 
(Type.lookup (Envir.type_env env) ixnS; NONE) handle TYPE _ => 
70811
785a2112f861
clarified signature  some operations to support fully explicit proof terms;
wenzelm
parents:
70810
diff
changeset

634 
SOME (ixnS, Logic.dummy_tfree S)) (Term.add_tvars t []), 
44118
69e29cf993c0
avoid OldTerm operations  with subtle changes of semantics;
wenzelm
parents:
44116
diff
changeset

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

637 
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

638 

11519  639 
fun norm_proof env = 
640 
let 

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

642 
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

643 
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

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

645 
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

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

647 
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

648 
(msg s; f envT (map (del_conflicting_tvars envT) Ts)); 
32024  649 

32019  650 
fun norm (Abst (s, T, prf)) = 
32024  651 
(Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) 
32019  652 
handle Same.SAME => Abst (s, T, norm prf)) 
653 
 norm (AbsP (s, t, prf)) = 

32024  654 
(AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf) 
32019  655 
handle Same.SAME => AbsP (s, t, norm prf)) 
656 
 norm (prf % t) = 

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

32024  658 
handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) 
32019  659 
 norm (prf1 %% prf2) = 
660 
(norm prf1 %% Same.commit norm prf2 

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

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

32024  663 
PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
32019  664 
 norm (OfClass (T, c)) = 
665 
OfClass (htypeT Envir.norm_type_same T, c) 

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

32024  667 
Oracle (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

668 
 norm (PThm ({serial = i, pos = p, theory_name, name = a, prop = t, types = Ts}, thm_body)) = 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

669 
PThm (thm_header i p theory_name a t 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

670 
(Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body) 
32019  671 
 norm _ = raise Same.SAME; 
672 
in Same.commit norm end; 

11519  673 

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

674 

70397  675 
(* remove some types in proof term (to save space) *) 
11519  676 

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

678 
 remove_types (t $ u) = remove_types t $ remove_types u 

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

680 
 remove_types t = t; 

681 

32032  682 
fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = 
39020  683 
Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; 
11519  684 

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

686 

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

687 

70397  688 
(* substitution of bound variables *) 
11519  689 

690 
fun prf_subst_bounds args prf = 

691 
let 

692 
val n = length args; 

693 
fun subst' lev (Bound i) = 

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

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

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

11519  702 

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

32019  705 
handle Same.SAME => AbsP (a, t, subst lev body)) 
11519  706 
 subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) 
11615  707 
 subst lev (prf %% prf') = (subst lev prf %% substh lev prf' 
32019  708 
handle Same.SAME => prf %% subst lev prf') 
15570  709 
 subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t 
32024  710 
handle Same.SAME => prf % Same.map_option (subst' lev) t) 
32019  711 
 subst _ _ = raise Same.SAME 
32024  712 
and substh lev prf = (subst lev prf handle Same.SAME => prf); 
64566  713 
in (case args of [] => prf  _ => substh 0 prf) end; 
11519  714 

715 
fun prf_subst_pbounds args prf = 

716 
let 

717 
val n = length args; 

718 
fun subst (PBound i) Plev tlev = 

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

11615  724 
 subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev 
32019  725 
handle Same.SAME => prf %% subst prf' Plev tlev) 
11615  726 
 subst (prf % t) Plev tlev = subst prf Plev tlev % t 
63857  727 
 subst _ _ _ = raise Same.SAME 
32019  728 
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) 
64566  729 
in (case args of [] => prf  _ => substh prf 0 0) end; 
11519  730 

731 

70397  732 
(* freezing and thawing of variables in proof terms *) 
11519  733 

44101  734 
local 
735 

11519  736 
fun frzT names = 
44101  737 
map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); 
11519  738 

739 
fun thawT names = 

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

742 
NONE => TFree (a, S) 

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

11519  744 

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

746 
freeze names names' t $ freeze names names' u 

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

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

63857  749 
 freeze _ names' (Const (s, T)) = Const (s, frzT names' T) 
750 
 freeze _ names' (Free (s, T)) = Free (s, frzT names' T) 

11519  751 
 freeze names names' (Var (ixn, T)) = 
44101  752 
Free (the (AList.lookup (op =) names ixn), frzT names' T) 
63857  753 
 freeze _ _ t = t; 
11519  754 

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

756 
thaw names names' t $ thaw names names' u 

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

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

63857  759 
 thaw _ names' (Const (s, T)) = Const (s, thawT names' T) 
21646
c07b5b0e8492
thm/prf: separate official name vs. additional tags;
wenzelm
parents:
20853
diff
changeset

760 
 thaw names names' (Free (s, T)) = 
44101  761 
let val T' = thawT names' T in 
762 
(case AList.lookup (op =) names s of 

15531  763 
NONE => Free (s, T') 
44101  764 
 SOME ixn => Var (ixn, T')) 
11519  765 
end 
63857  766 
 thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T) 
767 
 thaw _ _ t = t; 

11519  768 

44101  769 
in 
770 

11519  771 
fun freeze_thaw_prf prf = 
772 
let 

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

20147  774 
(fn t => fn (fs, Tfs, vs, Tvs) => 
29261  775 
(Term.add_free_names t fs, Term.add_tfree_names t Tfs, 
776 
Term.add_var_names t vs, Term.add_tvar_names t Tvs)) 

20147  777 
(fn T => fn (fs, Tfs, vs, Tvs) => 
29261  778 
(fs, Term.add_tfree_namesT T Tfs, 
779 
vs, Term.add_tvar_namesT T Tvs)) 

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

782 
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); 
11519  783 
val rnames = map swap names; 
784 
val rnames' = map swap names'; 

785 
in 

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

787 
map_proof_terms (thaw rnames rnames') (thawT rnames')) 

788 
end; 

789 

44101  790 
end; 
791 

11519  792 

70397  793 

794 
(** proof terms as pure terms **) 

70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

795 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

796 
val proofT = Type ("Pure.proof", []); 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

797 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

798 
local 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

799 

70392  800 
val AbsPt = Const ("Pure.AbsP", propT > (proofT > proofT) > proofT); 
801 
val AppPt = Const ("Pure.AppP", proofT > proofT > proofT); 

70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

802 
val Hypt = Const ("Pure.Hyp", propT > proofT); 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

803 
val Oraclet = Const ("Pure.Oracle", propT > proofT); 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

804 
val MinProoft = Const ("Pure.MinProof", proofT); 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

805 

70392  806 
fun AppT T prf = 
807 
Const ("Pure.Appt", proofT > Term.itselfT T > proofT) $ prf $ Logic.mk_type T; 

808 

70391  809 
fun OfClasst (T, c) = 
810 
let val U = Term.itselfT T > propT 

811 
in Const ("Pure.OfClass", U > proofT) $ Const (Logic.const_of_class c, U) end; 

812 

70511  813 
fun term_of _ (PThm ({name, types = Ts, ...}, _)) = 
814 
fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT)) 

815 
 term_of _ (PAxm (name, _, Ts)) = 

816 
fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) 

817 
 term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) 

818 
 term_of _ (PBound i) = Bound i 

819 
 term_of Ts (Abst (s, opT, prf)) = 

820 
let val T = the_default dummyT opT in 

821 
Const ("Pure.Abst", (T > proofT) > proofT) $ 

822 
Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) 

823 
end 

824 
 term_of Ts (AbsP (s, t, prf)) = 

825 
AbsPt $ the_default Term.dummy_prop t $ 

826 
Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) 

827 
 term_of Ts (prf1 %% prf2) = 

828 
AppPt $ term_of Ts prf1 $ term_of Ts prf2 

829 
 term_of Ts (prf % opt) = 

830 
let 

831 
val t = the_default Term.dummy opt; 

832 
val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; 

833 
in Const ("Pure.Appt", proofT > T > proofT) $ term_of Ts prf $ t end 

834 
 term_of _ (Hyp t) = Hypt $ t 

70559  835 
 term_of _ (Oracle (_, t, _)) = Oraclet $ oracle_prop t 
70511  836 
 term_of _ MinProof = MinProoft; 
837 

70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

838 
in 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

839 

70511  840 
val term_of_proof = term_of []; 
70388
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

841 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

842 
end; 
e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

843 

e31271559de8
global declaration of abstract syntax for proof terms, with qualified names;
wenzelm
parents:
68068
diff
changeset

844 

70397  845 

846 
(** inference rules **) 

847 

848 
(* implication introduction *) 

11519  849 

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

850 
fun gen_implies_intr_proof f h prf = 
11519  851 
let 
32019  852 
fun abshyp i (Hyp t) = if h aconv t then PBound i else raise Same.SAME 
11519  853 
 abshyp i (Abst (s, T, prf)) = Abst (s, T, abshyp i prf) 
32024  854 
 abshyp i (AbsP (s, t, prf)) = AbsP (s, t, abshyp (i + 1) prf) 
11615  855 
 abshyp i (prf % t) = abshyp i prf % t 
32024  856 
 abshyp i (prf1 %% prf2) = 
857 
(abshyp i prf1 %% abshyph i prf2 

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

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

862 
AbsP ("H", f h, abshyph 0 prf) 
11519  863 
end; 
864 

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

865 
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

866 
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

867 

11519  868 

70397  869 
(* forall introduction *) 
11519  870 

70814  871 
fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf); 
11519  872 

70814  873 
fun forall_intr_proof' v prf = 
874 
let val (a, T) = (case v of Var ((a, _), T) => (a, T)  Free (a, T) => (a, T)) 

875 
in forall_intr_proof (a, v) (SOME T) prf end; 

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

876 

11519  877 

70397  878 
(* varify *) 
11519  879 

880 
fun varify_proof t fixed prf = 

881 
let 

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

29261  884 
val used = Name.context 
885 
> 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

886 
val fmap = fs ~~ #1 (fold_map Name.variant (map fst fs) used); 
63857  887 
fun thaw (a, S) = 
888 
(case AList.lookup (op =) fmap (a, S) of 

889 
NONE => TFree (a, S) 

15531  890 
 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

891 
in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; 
11519  892 

893 

894 
local 

895 

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

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

897 
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

898 
in ((ix, v) :: pairs, v :: used) end; 
11519  899 

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

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

901 
(case AList.lookup (op =) alist ix of 
15531  902 
NONE => TVar (ix, sort) 
903 
 SOME name => TFree (name, sort)); 

11519  904 

905 
in 

906 

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

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

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

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

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

914 
 _ => 

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

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

916 
in map_proof_terms (map_types frzT) frzT prf end) 
11519  917 
end; 
918 

919 
end; 

920 

921 

70397  922 
(* rotate assumptions *) 
11519  923 

924 
fun rotate_proof Bs Bi m prf = 

925 
let 

926 
val params = Term.strip_all_vars Bi; 

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

928 
val i = length asms; 

929 
val j = length Bs; 

930 
in 

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

23178  932 
(j downto 1) @ [mk_Abst params (mk_AbsP (i, 
11519  933 
proof_combP (proof_combt (PBound i, map Bound ((length params  1) downto 0)), 
23178  934 
map PBound (((im1) downto 0) @ ((i1) downto (im))))))])) 
11519  935 
end; 
936 

937 

70397  938 
(* permute premises *) 
11519  939 

36742  940 
fun permute_prems_proof prems j k prf = 
11519  941 
let val n = length prems 
942 
in mk_AbsP (n, proof_combP (prf, 

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

944 
end; 

945 

946 

70397  947 
(* generalization *) 
19908  948 

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

950 
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

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

952 
(Term_Subst.generalizeT_same tfrees idx)); 
19908  953 

954 

70397  955 
(* instantiation *) 
11519  956 

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

958 
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

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

960 
(Term_Subst.instantiateT_same instT)); 
11519  961 

962 

70397  963 
(* lifting *) 
11519  964 

965 
fun lift_proof Bi inc prop prf = 

966 
let 

32024  967 
fun lift'' Us Ts t = 
59787  968 
strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t)); 
11519  969 

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

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

973 
 lift' Us Ts (AbsP (s, t, prf)) = 
32024  974 
(AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) 
32019  975 
handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) 
15570  976 
 lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t 
32024  977 
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

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

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

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

984 
 lift' _ _ (Oracle (s, prop, Ts)) = 
32024  985 
Oracle (s, prop, (Same.map_option o Same.map) (Logic.incr_tvar_same inc) Ts) 
70538
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

986 
 lift' _ _ (PThm ({serial = i, pos = p, theory_name, name = s, prop, types = Ts}, thm_body)) = 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

987 
PThm (thm_header i p theory_name s prop 
fc9ba6fe367f
clarified PThm: theory_name simplifies retrieval from exports;
wenzelm
parents:
70534
diff
changeset

988 
((Same.map_option o Same.map) (Logic.incr_tvar inc) Ts), thm_body) 
32019  989 
 lift' _ _ _ = raise Same.SAME 
990 
and lifth' Us Ts prf = (lift' Us Ts prf handle Same.SAME => prf); 

11519  991 

18030  992 
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); 
11519  993 
val k = length ps; 
994 

23178  995 
fun mk_app b (i, j, prf) = 
11615  996 
if b then (i1, j, prf %% PBound i) else (i, j1, prf %> Bound j); 
11519  997 

56245  998 
fun lift Us bs i j (Const ("Pure.imp", _) $ A $ B) = 
20147  999 
AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B) 
56245  1000 
 lift Us bs i j (Const ("Pure.all", _) $ Abs (a, T, t)) = 
20147  1001 
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

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

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

1007 
end; 

1008 

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

1010 
Same.commit (map_proof_terms_same 
59787  1011 
(Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i)); 
32027  1012 

11519  1013 

70397  1014 
(* proof by assumption *) 
11519  1015 

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

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

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

1018 
fun imp_prf _ i 0 = PBound i 
56245  1019 
 imp_prf (Const ("Pure.imp", _) $ A $ B) i m = AbsP ("H", NONE (*A*), imp_prf B (i+1) (m1)) 
23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

1020 
 imp_prf _ i _ = PBound i; 
56245  1021 
fun all_prf (Const ("Pure.all", _) $ Abs (a, T, t)) = Abst (a, NONE (*T*), all_prf t) 
23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

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

1023 
in all_prf t end; 
11519  1024 

1025 
fun assumption_proof Bs Bi n prf = 

1026 
mk_AbsP (length Bs, proof_combP (prf, 

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

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

1029 

70397  1030 
(* composition of object rule with proof state *) 
11519  1031 

56245  1032 
fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) = 
15531  1033 
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) 
56245  1034 
 flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) = 
15531  1035 
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) 
11519  1036 
 flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), 
19304  1037 
map Bound (j1 downto 0)), map PBound (remove (op =) (in) (i1 downto 0))); 
11519  1038 

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

1039 
fun bicompose_proof flatten Bs oldAs newAs A n m rprf sprf = 
11519  1040 
let 
1041 
val la = length newAs; 

1042 
val lb = length Bs; 

1043 
in 

1044 
mk_AbsP (lb+la, proof_combP (sprf, 

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

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

11519  1049 
end; 
1050 

1051 

70397  1052 

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

1054 

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

1055 
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

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

1057 
fun get S2 (T, S1) = if Sorts.sort_le algebra (S1, S2) then SOME T else NONE; 
70811
785a2112f861
clarified signature  some operations to support fully explicit proof terms;
wenzelm
parents:
70810
diff
changeset

1058 
val extra = map (`Logic.dummy_tfree) 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

1059 
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

1060 
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

1061 
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

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

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

1064 
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

1065 
 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

1066 
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

1067 

70458  1068 
fun of_sort_proof algebra classrel_proof arity_proof hyps = 
1069 
Sorts.of_sort_derivation algebra 

1070 
{class_relation = fn _ => fn _ => fn (prf, c1) => fn c2 => 

1071 
if c1 = c2 then prf else classrel_proof (c1, c2) %% prf, 

1072 
type_constructor = fn (a, _) => fn dom => fn c => 

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

1073 
let val Ss = map (map snd) dom and prfs = maps (map fst) dom 
70458  1074 
in proof_combP (arity_proof (a, Ss, c), prfs) end, 
36741
d65ed9d7275e
added of_sort_proof according to krauss/schropp, with slightly more direct canonical_instance;
wenzelm
parents:
36740
diff
changeset

1075 
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

1076 

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

1077 

70420  1078 

70397  1079 
(** axioms and theorems **) 
11519  1080 

70810  1081 
fun tvars_of t = map TVar (rev (Term.add_tvars t [])); 
1082 
fun tfrees_of t = map TFree (rev (Term.add_tfrees t [])); 

1083 
fun type_variables_of t = tvars_of t @ tfrees_of t; 

1084 

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

1085 
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

1086 
fun frees_of t = map Free (rev (Term.add_frees t [])); 
70809  1087 
fun variables_of t = vars_of t @ frees_of t; 
11519  1088 

1089 
fun test_args _ [] = true 

1090 
 test_args is (Bound i :: ts) = 

17492  1091 
not (member (op =) is i) andalso test_args (i :: is) ts 
11519  1092 
 test_args _ _ = false; 
1093 

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

1095 
 is_fun (TVar _) = true 

1096 
 is_fun _ = false; 

1097 

1098 
fun add_funvars Ts (vs, t) = 

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

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

1101 
if is_fun T then SOME ixn else NONE  _ => NONE) (vars_of t)) 
11519  1102 
else vs; 
1103 

56245  1104 
fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) = 
11519  1105 
add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) 
56245  1106 
 add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) = 
11519  1107 
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) 
12041  1108 
 add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) 
1109 
 add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) 

64566  1110 
and add_npvars' Ts (vs, t) = 
1111 
(case strip_comb t of 

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

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

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

11519  1118 

56245  1119 
fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q) 
1120 
 prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t 

64566  1121 
 prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn]  _ => []); 
11519  1122 

1123 
fun is_proj t = 

1124 
let 

64566  1125 
fun is_p i t = 
1126 
(case strip_comb t of 

63857  1127 
(Bound _, []) => false 
11519  1128 
 (Bound j, ts) => j >= i orelse exists (is_p i) ts 
1129 
 (Abs (_, _, u), _) => is_p (i+1) u 

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

64566  1131 
in 
1132 
(case strip_abs_body t of 

1133 
Bound _ => true 

1134 
 t' => is_p 0 t') 

11519  1135 
end; 
1136 

70416  1137 
fun prop_args prop = 
1138 
let 

1139 
val needed_vars = 

1140 
union (op =) (Library.foldl (uncurry (union (op =))) 

1141 
([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop)))) 

1142 
(prop_vars prop); 

1143 
val vars = 

1144 
vars_of prop > map (fn (v as Var (ixn, _)) => 

1145 
if member (op =) needed_vars ixn then SOME v else NONE); 

1146 
val frees = map SOME (frees_of prop); 

1147 
in vars @ frees end; 

11519  1148 

70559  1149 
fun axm_proof name prop = 
1150 
proof_combt' (PAxm (name, prop, NONE), prop_args prop); 

17017  1151 

52487
48bc24467008
backout dedd7952a62c: static "proofs" value within theory prevents later inferencing with different configuration;
wenzelm
parents:
52470
diff
changeset

1152 
fun oracle_proof name prop = 
70559  1153 
if ! proofs = 0 
1154 
then ((name, NONE), Oracle (name, NONE, NONE)) 

1155 
else ((name, SOME prop), proof_combt' (Oracle (name, SOME prop, NONE), prop_args prop)); 

11519  1156 

63623  1157 
val shrink_proof = 
17492  1158 
let 
1159 
fun shrink ls lev (prf as Abst (a, T, body)) = 

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

51100
18daa3380ff7
discontinued homemade sharing for proof terms  leave memory management to the Poly/ML RTS;
wenzelm
parents:
51047
diff
changeset

1161 
in (b, is, ch, if ch then Abst (a, T, body') else prf) end 
17492  1162 
 shrink ls lev (prf as AbsP (a, t, body)) = 
1163 
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

1164 
in (b orelse member (op =) is 0, map_filter (fn 0 => NONE  i => SOME (i1)) is, 
51100
18daa3380ff7
discontinued homemade sharing for proof terms  leave memory management to the Poly/ML RTS;
wenzelm
parents:
51047
diff
changeset

1165 
ch, if ch then AbsP (a, t, body') else prf) 
17492  1166 
end 
1167 
 shrink ls lev prf = 

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

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

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

1171 
let 

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

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

33042  1174 
in (union (op =) is is', ch orelse ch', ts', 
17492  1175 
if ch orelse ch' then prf'' %% prf' else prf) 
1176 
end 

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

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

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

51100
18daa3380ff7
discontinued homemade sharing for proof terms  leave memory management to the Poly/ML RTS;
wenzelm
parents:
51047
diff
changeset

1180 
if ch orelse ch' then prf' % t' else prf) end 
17492  1181 
 shrink' ls lev ts prfs (prf as PBound i) = 
30146  1182 
(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

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

1184 
(Library.foldl (fn (js, SOME (Bound j)) => j :: js  (js, _) => js) ([], ts)) 
17492  1185 
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf) 
63857  1186 
 shrink' _ _ ts _ (Hyp t) = ([], false, map (pair false) ts, Hyp t) 
1187 
 shrink' _ _ ts _ (prf as MinProof) = ([], false, map (pair false) ts, prf) 

1188 
 shrink' _ _ ts _ (prf as OfClass _) = ([], false, map (pair false) ts, prf) 

1189 
 shrink' _ _ ts prfs prf = 

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

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

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

1193 
PAxm (_, prop, _) => prop 
70559  1194 
 Oracle (_, prop, _) => oracle_prop prop 
70493  1195 
 PThm ({prop, ...}, _) => prop 
36879
201a4afd8533
raise Fail uniformly for proofterm errors, which appear to be rather lowlevel;
wenzelm
parents:
36878
diff
changeset

1196 
 _ => raise Fail "shrink: proof not in normal form"); 
17492  1197 
val vs = vars_of prop; 
19012  1198 
val (ts', ts'') = chop (length vs) ts; 
33957  1199 
val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; 
17492  1200 
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => 
64566  1201 
insert (op =) ixn 
1202 
(case AList.lookup (op =) insts ixn of 

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

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

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

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

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

56245  1210 
and needed (Const ("Pure.imp", _) $ t $ u) ts ((b, _, _, _)::prfs) = 
33042  1211 
union (op =) (if b then map (fst o dest_Var) (vars_of t) else []) (needed u ts prfs) 
17492  1212 
 needed (Var (ixn, _)) (_::_) _ = [ixn] 
1213 
 needed _ _ _ = []; 

63623  1214 
in fn prf => #4 (shrink [] 0 prf) end; 
11519  1215 

1216 

70397  1217 

70420  1218 
(** axioms for equality **) 
1219 

1220 
val aT = TFree ("'a", []); 

1221 
val bT = TFree ("'b", []); 

1222 
val x = Free ("x", aT); 

1223 
val y = Free ("y", aT); 

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

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

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

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

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

1229 

1230 
val equality_axms = 

1231 
[("reflexive", Logic.mk_equals (x, x)), 

1232 
("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))), 

1233 
("transitive", 

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

1235 
("equal_intr", 

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

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

1238 
("abstract_rule", 

1239 
Logic.mk_implies 

70814  1240 
(Logic.all x (Logic.mk_equals (f $ x, g $ x)), 
1241 
Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), 

70420  1242 
("combination", Logic.list_implies 
1243 
([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))]; 

1244 

1245 
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, 

1246 
equal_elim_axm, abstract_rule_axm, combination_axm] = 

1247 
map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms; 

1248 

70814  1249 
val reflexive_proof = reflexive_axm % NONE; 
1250 

1251 
val is_reflexive_proof = fn PAxm ("Pure.reflexive", _, _) % _ => true  _ => false; 

70420  1252 

70814  1253 
fun symmetric_proof prf = 
1254 
if is_reflexive_proof prf then prf 

1255 
else symmetric_axm % NONE % NONE %% prf; 

70420  1256 

70814  1257 
fun transitive_proof U u prf1 prf2 = 
1258 
if is_reflexive_proof prf1 then prf2 

1259 
else if is_reflexive_proof prf2 then prf1 

1260 
else if U = propT then transitive_axm % NONE % SOME (remove_types u) % NONE %% prf1 %% prf2 

1261 
else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; 

70420  1262 

70814  1263 
fun equal_intr_proof A B prf1 prf2 = 
1264 
equal_intr_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 

1265 

1266 
fun equal_elim_proof A B prf1 prf2 = 

1267 
equal_elim_axm %> remove_types A %> remove_types B %% prf1 %% prf2; 

1268 

1269 
fun abstract_rule_proof (a, x) prf = 

1270 
abstract_rule_axm % NONE % NONE %% forall_intr_proof (a, x) NONE prf; 

70420  1271 

1272 
fun check_comb (PAxm ("Pure.combination", _, _) % f % _ % _ % _ %% prf %% _) = 

1273 
is_some f orelse check_comb prf 

1274 
 check_comb (PAxm ("Pure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) = 

1275 
check_comb prf1 andalso check_comb prf2 

1276 
 check_comb (PAxm ("Pure.symmetric", _, _) % _ % _ %% prf) = check_comb prf 

1277 
 check_comb _ = false; 

1278 

70814  1279 
fun combination_proof A f g t u prf1 prf2 = 
70420  1280 
let 
1281 
val f = Envir.beta_norm f; 

1282 
val g = Envir.beta_norm g; 

1283 
val prf = 

1284 
if check_comb prf1 then 

1285 
combination_axm % NONE % NONE 

1286 
else 

1287 
(case prf1 of 

1288 
PAxm ("Pure.reflexive", _, _) % _ => 

328573dd886f
tuned  reorder sections;
wenzelm
< 