author  wenzelm 
Mon, 09 Mar 2020 14:13:44 +0100  
changeset 71528  448c81228daf 
parent 71465  910a081cca74 
child 71529  dd56597e026b 
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 
70834  26 
 Oracle of string * term * 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 
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

29 
{oracles: ((string * Position.T) * 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} 
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

32 
type oracle = (string * Position.T) * term option 
70590  33 
type thm = serial * thm_node 
70976
d86798eddc14
more accurate proof_boxes  from actual proof body;
wenzelm
parents:
70948
diff
changeset

34 
exception MIN_PROOF of unit 
32094
89b9210c7506
prefer simultaneous join  for improved scheduling;
wenzelm
parents:
32057
diff
changeset

35 
val proof_of: proof_body > proof 
70587  36 
val join_proof: proof_body future > proof 
70396  37 
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

38 
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

39 
thm_header 
70501  40 
val thm_body: proof_body > thm_body 
70493  41 
val thm_body_proof_raw: thm_body > proof 
42 
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

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

46 
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

47 
val thm_node_thms: thm_node > thm list 
70590  48 
val join_thms: thm list > proof_body list 
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 
70916
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

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

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

62 

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

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

64 
val encode_body: Consts.T > proof_body XML.Encode.T 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

65 
val encode_standard_term: Consts.T > term XML.Encode.T 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

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

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

68 
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

69 

70587  70 
val %> : proof * term > proof 
71 

70397  72 
(*primitive operations*) 
70587  73 
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

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

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

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

77 
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

78 
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

79 
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

80 
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

81 
val strip_combP: proof > proof * proof list 
70830  82 
val strip_thm_body: 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

83 
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

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

85 
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

86 
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

87 
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

88 
val map_proof_types: (typ > typ) > proof > proof 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

89 
val fold_proof_terms: (term > 'a > 'a) > proof > 'a > 'a 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

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

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

92 
val size_of_proof: proof > int 
70417  93 
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

94 
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

95 
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

96 
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

97 
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

98 
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

99 
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

100 
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

101 
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

102 
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

103 
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

104 
val freeze_thaw_prf: proof > proof * (proof > proof) 
11519  105 

70397  106 
(*proof terms for specific inference rules*) 
70824  107 
val trivial_proof: proof 
28803
d90258bbb18f
reworked type proof: MinProof is vacous, added Promise, refined PThm (with serial);
wenzelm
parents:
28329
diff
changeset

108 
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

109 
val implies_intr_proof': term > proof > proof 
70814  110 
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

111 
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

112 
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

113 
val legacy_freezeT: term > proof > proof 
70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

114 
val rotate_proof: term list > term > (string * typ) list > term list > int > proof > proof 
36742  115 
val permute_prems_proof: term list > int > int > proof > proof 
70827
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

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

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

119 
val lift_proof: term > int > term > proof > proof 
32027  120 
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

121 
val assumption_proof: term list > term > int > proof > proof 
70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

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

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

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

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

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

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

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

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

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

131 
val combination_axm: proof 
70814  132 
val reflexive_proof: proof 
133 
val symmetric_proof: proof > proof 

134 
val transitive_proof: typ > term > proof > proof > proof 

135 
val equal_intr_proof: term > term > proof > proof > proof 

136 
val equal_elim_proof: term > term > proof > proof > proof 

137 
val abstract_rule_proof: string * term > proof > proof 

70908  138 
val combination_proof: 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

139 
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

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

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

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

145 
val axm_proof: string > term > proof 
70834  146 
val oracle_proof: string > term > proof 
63623  147 
val shrink_proof: proof > proof 
11519  148 

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

150 
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

151 
val add_prf_rproc: (typ list > term option list > proof > (proof * proof) option) > theory > theory 
70848  152 
val set_preproc: (theory > proof > proof) > theory > theory 
71010  153 
val apply_preproc: theory > proof > proof 
70978  154 
val forall_intr_variables_term: term > term 
155 
val forall_intr_variables: term > proof > proof 

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

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

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

158 
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

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

160 
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

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

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

163 

70449  164 
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

165 
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

166 
val prop_of: proof > term 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70909
diff
changeset

167 
val expand_name_empty: thm_header > string option 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70909
diff
changeset

168 
val expand_proof: theory > (thm_header > string option) > proof > proof 
70400
65bbef66e2ec
clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named;
wenzelm
parents:
70399
diff
changeset

169 

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

170 
val standard_vars: Name.context > term * proof option > term * proof option 
70529  171 
val standard_vars_term: Name.context > term > term 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

172 
val add_standard_vars: proof > (string * typ) list > (string * typ) list 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

173 
val add_standard_vars_term: term > (string * typ) list > (string * typ) list 
70529  174 

70604  175 
val export_enabled: unit > bool 
70983  176 
val export_standard_enabled: unit > bool 
70984  177 
val export_proof_boxes_required: theory > bool 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

178 
val export_proof_boxes: proof_body list > unit 
36877
7699f7fafde7
added Proofterm.get_name variants according to krauss/schropp;
wenzelm
parents:
36742
diff
changeset

179 
val fulfill_norm_proof: theory > (serial * proof_body) list > proof_body > proof_body 
70458  180 
val thm_proof: theory > (class * class > proof) > 
70494  181 
(string * class list list * class > proof) > string * Position.T > sort list > 
70590  182 
term list > term > (serial * proof_body future) list > proof_body > thm * proof 
70458  183 
val unconstrain_thm_proof: theory > (class * class > proof) > 
184 
(string * class list list * class > proof) > sort list > term > 

70590  185 
(serial * proof_body future) list > proof_body > thm * proof 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70909
diff
changeset

186 
val get_identity: sort list > term list > term > proof > 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70909
diff
changeset

187 
{serial: serial, theory_name: string, name: string} option 
70554  188 
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

189 
type thm_id = {serial: serial, theory_name: string} 
70895
2a318149b01b
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;
wenzelm
parents:
70892
diff
changeset

190 
val make_thm_id: serial * string > thm_id 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70909
diff
changeset

191 
val thm_header_id: thm_header > thm_id 
70595
2ae7e33c950f
clarified thm_id vs. thm_node/thm: retain theory_name;
wenzelm
parents:
70593
diff
changeset

192 
val thm_id: thm > thm_id 
70554  193 
val get_id: sort list > term list > term > proof > thm_id option 
70979  194 
val this_id: thm_id option > thm_id > bool 
70976
d86798eddc14
more accurate proof_boxes  from actual proof body;
wenzelm
parents:
70948
diff
changeset

195 
val proof_boxes: {excluded: thm_id > bool, included: thm_id > bool} > 
d86798eddc14
more accurate proof_boxes  from actual proof body;
wenzelm
parents:
70948
diff
changeset

196 
proof list > (thm_header * proof) list (*exception MIN_PROOF*) 
11519  197 
end 
198 

199 
structure Proofterm : PROOFTERM = 

200 
struct 

201 

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

203 

70493  204 
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

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

206 
prop: term, types: typ list option}; 
70493  207 

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

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

210 
 PBound of int 
11519  211 
 Abst of string * typ option * proof 
212 
 AbsP of string * term option * proof 

12497  213 
 op % of proof * term option 
214 
 op %% of proof * proof 

11519  215 
 Hyp of term 
216 
 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

217 
 OfClass of typ * class 
70834  218 
 Oracle of string * term * typ list option 
70493  219 
 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

220 
and proof_body = PBody of 
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

221 
{oracles: ((string * Position.T) * 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

222 
thms: (serial * thm_node) Ord_List.T, 
64573  223 
proof: proof} 
70493  224 
and thm_body = 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

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

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

227 
Thm_Node of {theory_name: string, name: string, prop: term, 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

228 
body: proof_body future, export: unit lazy, consolidate: unit lazy}; 
11519  229 

71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

230 
type oracle = (string * Position.T) * term option; 
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

231 
val oracle_ord: oracle ord = 
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

232 
prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord); 
70559  233 

70590  234 
type thm = serial * thm_node; 
70593  235 
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i); 
28815  236 

70587  237 

70976
d86798eddc14
more accurate proof_boxes  from actual proof body;
wenzelm
parents:
70948
diff
changeset

238 
exception MIN_PROOF of unit; 
d86798eddc14
more accurate proof_boxes  from actual proof body;
wenzelm
parents:
70948
diff
changeset

239 

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

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

241 
val join_proof = Future.join #> proof_of; 
17017  242 

70396  243 
fun map_proof_of f (PBody {oracles, thms, proof}) = 
244 
PBody {oracles = oracles, thms = thms, proof = f proof}; 

245 

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

246 
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

247 
{serial = serial, pos = pos, theory_name = theory_name, name = name, prop = prop, types = types}; 
70493  248 

71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

249 
fun thm_body body = Thm_Body {open_proof = I, body = Future.value body}; 
70493  250 
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

251 
fun thm_body_proof_open (Thm_Body {open_proof, body, ...}) = open_proof (join_proof body); 
70493  252 

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

253 
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

254 
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

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

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

257 
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

258 
val thm_node_thms = thm_node_body #> Future.join #> (fn PBody {thms, ...} => thms); 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

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

260 
val thm_node_consolidate = #consolidate o rep_thm_node; 
64573  261 

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

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

264 

71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

265 
val consolidate_bodies = 
66168  266 
maps (fn PBody {thms, ...} => map (thm_node_consolidate o #2) thms) 
67669  267 
#> Lazy.consolidate #> map Lazy.force #> ignore; 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64573
diff
changeset

268 

71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

269 
fun make_thm_node theory_name name prop body export = 
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

270 
let 
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

271 
val consolidate = 
66167  272 
Lazy.lazy_name "Proofterm.make_thm_node" (fn () => 
71022
6504ea98623c
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of reused nodes;
wenzelm
parents:
71018
diff
changeset

273 
let val PBody {thms, ...} = Future.join body 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

274 
in consolidate_bodies (join_thms thms) end); 
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

275 
in 
71022
6504ea98623c
uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of reused nodes;
wenzelm
parents:
71018
diff
changeset

276 
Thm_Node {theory_name = theory_name, name = name, prop = prop, body = body, 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

277 
export = export, consolidate = consolidate} 
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

278 
end; 
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

279 

d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

280 
val no_export = Lazy.value (); 
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

281 

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

282 
fun make_thm ({serial, theory_name, name, prop, ...}: thm_header) (Thm_Body {body, ...}) = 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

283 
(serial, make_thm_node theory_name name prop body no_export); 
70589  284 

17017  285 

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

287 

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

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

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

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

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

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

293 
 app (prf1 %% prf2) = app prf1 #> app prf2 
70493  294 
 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

295 
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

296 
else 
28815  297 
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

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

300 
 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

301 
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

302 

30711  303 
fun fold_body_thms f = 
304 
let 

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

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

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

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

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

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

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

313 
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

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

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

317 

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

319 

44334  320 
val unions_oracles = Ord_List.unions oracle_ord; 
321 
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

322 

70440  323 
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

324 
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

325 

70916
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

326 
fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

327 
 no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

328 
 no_thm_names (prf % t) = no_thm_names prf % t 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

329 
 no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

330 
 no_thm_names (PThm ({serial, pos, theory_name, name = _, prop, types}, thm_body)) = 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

331 
PThm (thm_header serial pos theory_name "" prop types, thm_body) 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

332 
 no_thm_names a = a; 
4c15217d6266
clarified signature: name of standard_proof is authentic, otherwise empty;
wenzelm
parents:
70915
diff
changeset

333 

70493  334 
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

335 
 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

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

337 
 no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2 
70493  338 
 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

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

340 

70493  341 
fun no_body_proofs (Abst (x, T, prf)) = Abst (x, T, no_body_proofs prf) 
70440  342 
 no_body_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_body_proofs prf) 
343 
 no_body_proofs (prf % t) = no_body_proofs prf % t 

344 
 no_body_proofs (prf1 %% prf2) = no_body_proofs prf1 %% no_body_proofs prf2 

71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

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

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

347 
val body' = Future.value (no_proof_body (join_proof body)); 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

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

349 
in PThm (header, thm_body') end 
70440  350 
 no_body_proofs a = a; 
351 

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

352 

70397  353 

354 
(** XML data representation **) 

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

355 

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

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

357 

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

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

359 

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

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

361 

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

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

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

365 
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

366 
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

367 
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

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

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

370 
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

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

373 
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

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

375 
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) 
70497  376 
(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

377 
and proof_body consts (PBody {oracles, thms, proof = prf}) = 
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

378 
triple (list (pair (pair string (properties o Position.properties_of)) 
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

379 
(option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf) 
70784
799437173553
Term_XML.Encode/Decode.term uses Const "typargs";
wenzelm
parents:
70604
diff
changeset

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

381 
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

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

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

384 

70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

385 
fun standard_term consts t = t > variant 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

386 
[fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))), 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

387 
fn Free (a, _) => ([a], []), 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

388 
fn Var (a, _) => (indexname a, []), 
70844  389 
fn Bound a => ([], int a), 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

390 
fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)), 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

391 
fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)]; 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

392 

70829  393 
fun standard_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

394 
[fn MinProof => ([], []), 
70844  395 
fn PBound a => ([], int a), 
70829  396 
fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)), 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

397 
fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)), 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

398 
fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)), 
70829  399 
fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)), 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

400 
fn Hyp a => ([], standard_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

401 
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

402 
fn OfClass (T, c) => ([c], typ T), 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

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

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

405 
([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

406 

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

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

408 

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

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

410 
val encode_body = proof_body; 
70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

411 
val encode_standard_term = standard_term; 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

412 
val encode_standard_proof = standard_proof; 
52424
77075c576d4c
support for XML data representation of proof terms;
wenzelm
parents:
51700
diff
changeset

413 

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

414 
end; 
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 

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

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

418 

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

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

420 

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

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

422 

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

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

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

426 
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

427 
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

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

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

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

431 
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

432 
fn ([b], a) => OfClass (typ a, b), 
70834  433 
fn ([a], b) => let val (c, d) = pair (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

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

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

437 
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

438 
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

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

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

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

442 
val (a, b, c) = 
71465
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

443 
triple (list (pair (pair string (Position.of_properties o properties)) 
910a081cca74
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
wenzelm
parents:
71022
diff
changeset

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

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

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

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

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

449 
pair int (pair string (pair string (pair (term consts) (proof_body consts)))) x 
71018
d32ed8927a42
more robust expose_proofs corresponding to register_proofs/consolidate_theory;
wenzelm
parents:
71010
diff
changeset

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

451 

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

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

453 

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

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

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

456 

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

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

458 

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

459 

70397  460 
(** proof objects with different levels of detail **) 
11519  461 

70587  462 
val proofs = Unsynchronized.ref 2; 
463 
fun proofs_enabled () = ! proofs >= 2; 

464 

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

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

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

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

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

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

470 
 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

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

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

473 

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

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

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

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

477 

15531  478 
fun (prf %> t) = prf % SOME t; 
11519  479 

15570  480 
val proof_combt = Library.foldl (op %>); 
481 
val proof_combt' = Library.foldl (op %); 

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

11519  483 

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

484 
fun strip_combt prf = 
11615  485 
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

486 
 stripc x = x 
11519  487 
in stripc (prf, []) end; 
488 

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

489 
fun strip_combP prf = 
11615  490 
let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs) 
11519  491 
 stripc x = x 
492 
in stripc (prf, []) end; 

493 

70830  494 
fun strip_thm_body (body as PBody {proof, ...}) = 
70493  495 
(case fst (strip_combt (fst (strip_combP proof))) of 
496 
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

497 
 _ => body); 
11519  498 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

499 
val mk_Abst = fold_rev (fn (x, _: typ) => fn prf => Abst (x, NONE, prf)); 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

500 
val mk_AbsP = fold_rev (fn _: term => fn prf => AbsP ("H", NONE, prf)); 
11519  501 

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

502 
fun map_proof_same term typ ofclass = 
20000  503 
let 
32024  504 
val typs = Same.map typ; 
20000  505 

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

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

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

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

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

512 
 proof (prf % t) = 

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

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

515 
 proof (prf1 %% prf2) = 

516 
(proof prf1 %% Same.commit proof prf2 

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

518 
 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

519 
 proof (OfClass T_c) = ofclass T_c 
32024  520 
 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

521 
 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

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

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

525 

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

526 
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

527 
fun map_proof_types_same typ = map_proof_terms_same (Term_Subst.map_types_same typ) typ; 
20000  528 

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

530 
let val x' = f x 
32019  531 
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

532 

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

533 
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

534 
fun map_proof_types f = Same.commit (map_proof_types_same (same (op =) f)); 
11519  535 

70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

536 
fun fold_proof_terms f (Abst (_, _, prf)) = fold_proof_terms f prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

537 
 fold_proof_terms f (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms f prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

538 
 fold_proof_terms f (AbsP (_, NONE, prf)) = fold_proof_terms f prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

539 
 fold_proof_terms f (prf % SOME t) = fold_proof_terms f prf #> f t 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

540 
 fold_proof_terms f (prf % NONE) = fold_proof_terms f prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

541 
 fold_proof_terms f (prf1 %% prf2) = fold_proof_terms f prf1 #> fold_proof_terms f prf2 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

542 
 fold_proof_terms _ _ = I; 
11519  543 

70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

544 
fun fold_proof_terms_types f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms_types f g prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

545 
 fold_proof_terms_types f g (Abst (_, NONE, prf)) = fold_proof_terms_types f g prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

546 
 fold_proof_terms_types f g (AbsP (_, SOME t, prf)) = f t #> fold_proof_terms_types f g prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

547 
 fold_proof_terms_types f g (AbsP (_, NONE, prf)) = fold_proof_terms_types f g prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

548 
 fold_proof_terms_types f g (prf % SOME t) = fold_proof_terms_types f g prf #> f t 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

549 
 fold_proof_terms_types f g (prf % NONE) = fold_proof_terms_types f g prf 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

550 
 fold_proof_terms_types f g (prf1 %% prf2) = 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

551 
fold_proof_terms_types f g prf1 #> fold_proof_terms_types f g prf2 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

552 
 fold_proof_terms_types _ g (PAxm (_, _, SOME Ts)) = fold g Ts 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

553 
 fold_proof_terms_types _ g (OfClass (T, _)) = g T 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

554 
 fold_proof_terms_types _ g (Oracle (_, _, SOME Ts)) = fold g Ts 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

555 
 fold_proof_terms_types _ g (PThm ({types = SOME Ts, ...}, _)) = fold g Ts 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

556 
 fold_proof_terms_types _ _ _ = I; 
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

557 

cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

558 
fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf; 
12868  559 

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

562 
 size_of_proof (prf % _) = 1 + size_of_proof prf 
13744  563 
 size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 
564 
 size_of_proof _ = 1; 

565 

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

568 
 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

569 
 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

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

572 

11519  573 

70397  574 
(* utilities *) 
11519  575 

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

577 
 strip_abs _ t = t; 

578 

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

581 

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

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

585 

586 
fun prf_abstract_over v = 

587 
let 

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

588 
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

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

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

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

11519  594 

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

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

598 
 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

599 
 abst lev (prf1 %% prf2) = (abst lev prf1 %% absth lev prf2 
32019  600 
handle Same.SAME => prf1 %% abst lev prf2) 
15570  601 
 abst lev (prf % t) = (abst lev prf % Option.map (absth' lev) t 
32024  602 
handle Same.SAME => prf % Same.map_option (abst' lev) t) 
32019  603 
 abst _ _ = raise Same.SAME 
32024  604 
and absth lev prf = (abst lev prf handle Same.SAME => prf); 
11519  605 

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

606 
in absth 0 end; 
11519  607 

608 

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

610 
required when moving a proof term within abstractions 

611 
inc is increment for bound variables 

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

613 

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

615 

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

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

621 
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

622 
 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

623 
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

624 
 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

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

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

631 
and prf_incr_bv incP inct Plev tlev prf = 
32019  632 
(prf_incr_bv' incP inct Plev tlev prf handle Same.SAME => prf); 
11519  633 

634 
fun incr_pboundvars 0 0 prf = prf 

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

636 

637 

11615  638 
fun prf_loose_bvar1 (prf1 %% prf2) k = prf_loose_bvar1 prf1 k orelse prf_loose_bvar1 prf2 k 
15531  639 
 prf_loose_bvar1 (prf % SOME t) k = prf_loose_bvar1 prf k orelse loose_bvar1 (t, k) 
640 
 prf_loose_bvar1 (_ % NONE) _ = true 

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

63857  642 
 prf_loose_bvar1 (AbsP (_, NONE, _)) _ = true 
11519  643 
 prf_loose_bvar1 (Abst (_, _, prf)) k = prf_loose_bvar1 prf (k+1) 
644 
 prf_loose_bvar1 _ _ = false; 

645 

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

11615  647 
 prf_loose_Pbvar1 (prf1 %% prf2) k = prf_loose_Pbvar1 prf1 k orelse prf_loose_Pbvar1 prf2 k 
648 
 prf_loose_Pbvar1 (prf % _) k = prf_loose_Pbvar1 prf k 

11519  649 
 prf_loose_Pbvar1 (AbsP (_, _, prf)) k = prf_loose_Pbvar1 prf (k+1) 
650 
 prf_loose_Pbvar1 (Abst (_, _, prf)) k = prf_loose_Pbvar1 prf k 

651 
 prf_loose_Pbvar1 _ _ = false; 

652 

63857  653 
fun prf_add_loose_bnos plev _ (PBound i) (is, js) = 
17492  654 
if i < plev then (is, js) else (insert (op =) (iplev) is, js) 
12279  655 
 prf_add_loose_bnos plev tlev (prf1 %% prf2) p = 
656 
prf_add_loose_bnos plev tlev prf2 

657 
(prf_add_loose_bnos plev tlev prf1 p) 

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

64566  659 
prf_add_loose_bnos plev tlev prf 
660 
(case opt of 

17492  661 
NONE => (is, insert (op =) ~1 js) 
15531  662 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  663 
 prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) = 
64566  664 
prf_add_loose_bnos (plev+1) tlev prf 
665 
(case opt of 

17492  666 
NONE => (is, insert (op =) ~1 js) 
15531  667 
 SOME t => (is, add_loose_bnos (t, tlev, js))) 
12279  668 
 prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p = 
669 
prf_add_loose_bnos plev (tlev+1) prf p 

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

671 

11519  672 

70397  673 
(* substitutions *) 
11519  674 

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

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

678 
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

679 

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

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

683 
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

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

686 
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

687 

11519  688 
fun norm_proof env = 
689 
let 

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

691 
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

692 
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

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

694 
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

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

696 
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

697 
(msg s; f envT (map (del_conflicting_tvars envT) Ts)); 
32024  698 

32019  699 
fun norm (Abst (s, T, prf)) = 
32024  700 
(Abst (s, Same.map_option (htypeT Envir.norm_type_same) T, Same.commit norm prf) 
32019  701 
handle Same.SAME => Abst (s, T, norm prf)) 
702 
 norm (AbsP (s, t, prf)) = 

32024  703 
(AbsP (s, Same.map_option (htype Envir.norm_term_same) t, Same.commit norm prf) 
32019  704 
handle Same.SAME => AbsP (s, t, norm prf)) 
705 
 norm (prf % t) = 

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

32024  707 
handle Same.SAME => prf % Same.map_option (htype Envir.norm_term_same) t) 
32019  708 
 norm (prf1 %% prf2) = 
709 
(norm prf1 %% Same.commit norm prf2 

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

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

32024  712 
PAxm (s, prop, Same.map_option (htypeTs Envir.norm_types_same) Ts) 
32019  713 
 norm (OfClass (T, c)) = 
714 
OfClass (htypeT Envir.norm_type_same T, c) 

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

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

717 
 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

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

719 
(Same.map_option (htypeTs Envir.norm_types_same) Ts), thm_body) 
32019  720 
 norm _ = raise Same.SAME; 
721 
in Same.commit norm end; 

11519  722 

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

723 

70397  724 
(* remove some types in proof term (to save space) *) 
11519  725 

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

727 
 remove_types (t $ u) = remove_types t $ remove_types u 

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

729 
 remove_types t = t; 

730 

32032  731 
fun remove_types_env (Envir.Envir {maxidx, tenv, tyenv}) = 
39020  732 
Envir.Envir {maxidx = maxidx, tenv = Vartab.map (K (apsnd remove_types)) tenv, tyenv = tyenv}; 
11519  733 

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

735 

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

736 

70397  737 
(* substitution of bound variables *) 
11519  738 

739 
fun prf_subst_bounds args prf = 

740 
let 

741 
val n = length args; 

742 
fun subst' lev (Bound i) = 

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

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

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

11519  751 

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

32019  754 
handle Same.SAME => AbsP (a, t, subst lev body)) 
11519  755 
 subst lev (Abst (a, T, body)) = Abst (a, T, subst (lev+1) body) 
11615  756 
 subst lev (prf %% prf') = (subst lev prf %% substh lev prf' 
32019  757 
handle Same.SAME => prf %% subst lev prf') 
15570  758 
 subst lev (prf % t) = (subst lev prf % Option.map (substh' lev) t 
32024  759 
handle Same.SAME => prf % Same.map_option (subst' lev) t) 
32019  760 
 subst _ _ = raise Same.SAME 
32024  761 
and substh lev prf = (subst lev prf handle Same.SAME => prf); 
64566  762 
in (case args of [] => prf  _ => substh 0 prf) end; 
11519  763 

764 
fun prf_subst_pbounds args prf = 

765 
let 

766 
val n = length args; 

767 
fun subst (PBound i) Plev tlev = 

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

11615  773 
 subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev 
32019  774 
handle Same.SAME => prf %% subst prf' Plev tlev) 
11615  775 
 subst (prf % t) Plev tlev = subst prf Plev tlev % t 
63857  776 
 subst _ _ _ = raise Same.SAME 
32019  777 
and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf) 
64566  778 
in (case args of [] => prf  _ => substh prf 0 0) end; 
11519  779 

780 

70397  781 
(* freezing and thawing of variables in proof terms *) 
11519  782 

44101  783 
local 
784 

11519  785 
fun frzT names = 
44101  786 
map_type_tvar (fn (ixn, S) => TFree (the (AList.lookup (op =) names ixn), S)); 
11519  787 

788 
fun thawT names = 

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

791 
NONE => TFree (a, S) 

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

11519  793 

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

795 
freeze names names' t $ freeze names names' u 

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

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

63857  798 
 freeze _ names' (Const (s, T)) = Const (s, frzT names' T) 
799 
 freeze _ names' (Free (s, T)) = Free (s, frzT names' T) 

11519  800 
 freeze names names' (Var (ixn, T)) = 
44101  801 
Free (the (AList.lookup (op =) names ixn), frzT names' T) 
63857  802 
 freeze _ _ t = t; 
11519  803 

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

805 
thaw names names' t $ thaw names names' u 

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

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

63857  808 
 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

809 
 thaw names names' (Free (s, T)) = 
44101  810 
let val T' = thawT names' T in 
811 
(case AList.lookup (op =) names s of 

15531  812 
NONE => Free (s, T') 
44101  813 
 SOME ixn => Var (ixn, T')) 
11519  814 
end 
63857  815 
 thaw _ names' (Var (ixn, T)) = Var (ixn, thawT names' T) 
816 
 thaw _ _ t = t; 

11519  817 

44101  818 
in 
819 

11519  820 
fun freeze_thaw_prf prf = 
821 
let 

70843
cc987440d776
more compact XML: separate environment for free variables;
wenzelm
parents:
70839
diff
changeset

822 
val (fs, Tfs, vs, Tvs) = fold_proof_terms_types 
20147  823 
(fn t => fn (fs, Tfs, vs, Tvs) => 
29261  824 
(Term.add_free_names t fs, Term.add_tfree_names t Tfs, 
825 
Term.add_var_names t vs, Term.add_tvar_names t Tvs)) 

20147  826 
(fn T => fn (fs, Tfs, vs, Tvs) => 
29261  827 
(fs, Term.add_tfree_namesT T Tfs, 
828 
vs, Term.add_tvar_namesT T Tvs)) 

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

831 
val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs); 
11519  832 
val rnames = map swap names; 
833 
val rnames' = map swap names'; 

834 
in 

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

836 
map_proof_terms (thaw rnames rnames') (thawT rnames')) 

837 
end; 

838 

44101  839 
end; 
840 

11519  841 

70397  842 

843 
(** inference rules **) 

844 

70824  845 
(* trivial implication *) 
846 

847 
val trivial_proof = AbsP ("H", NONE, PBound 0); 

848 

849 

70397  850 
(* implication introduction *) 
11519  851 

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

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

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

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

864 
AbsP ("H", f h, abshyph 0 prf) 
11519  865 
end; 
866 

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

867 
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

868 
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

869 

11519  870 

70397  871 
(* forall introduction *) 
11519  872 

70814  873 
fun forall_intr_proof (a, v) opt_T prf = Abst (a, opt_T, prf_abstract_over v prf); 
11519  874 

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

877 
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

878 

11519  879 

70397  880 
(* varify *) 
11519  881 

882 
fun varify_proof t fixed prf = 

883 
let 

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

29261  886 
val used = Name.context 
887 
> 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

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

891 
NONE => TFree (a, S) 

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

893 
in map_proof_terms (map_types (map_type_tfree thaw)) (map_type_tfree thaw) prf end; 
11519  894 

895 

896 
local 

897 

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

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

899 
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

900 
in ((ix, v) :: pairs, v :: used) end; 
11519  901 

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

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

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

11519  906 

907 
in 

908 

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

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

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

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

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

916 
 _ => 

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

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

918 
in map_proof_terms (map_types frzT) frzT prf end) 
11519  919 
end; 
920 

921 
end; 

922 

923 

70397  924 
(* rotate assumptions *) 
11519  925 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

926 
fun rotate_proof Bs Bi' params asms m prf = 
11519  927 
let 
928 
val i = length asms; 

929 
val j = length Bs; 

930 
in 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

931 
mk_AbsP (Bs @ [Bi']) (proof_combP (prf, map PBound 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

932 
(j downto 1) @ [mk_Abst params (mk_AbsP asms 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

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 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

940 
fun permute_prems_proof prems' j k prf = 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

941 
let val n = length prems' in 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

942 
mk_AbsP prems' 
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

943 
(proof_combP (prf, map PBound ((n1 downto nj) @ (k1 downto 0) @ (nj1 downto k)))) 
11519  944 
end; 
945 

946 

70397  947 
(* generalization *) 
19908  948 

70827
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

949 
fun generalize_proof (tfrees, frees) idx prop prf = 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

950 
let 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

951 
val gen = 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

952 
if null frees then [] 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

953 
else 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

954 
fold_aterms (fn Free (x, T) => member (op =) frees x ? insert (op =) (x, T)  _ => I) 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

955 
(Term_Subst.generalize (tfrees, []) idx prop) []; 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

956 
in 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

957 
prf 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

958 
> Same.commit (map_proof_terms_same 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

959 
(Term_Subst.generalize_same (tfrees, []) idx) 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

960 
(Term_Subst.generalizeT_same tfrees idx)) 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

961 
> fold (fn (x, T) => forall_intr_proof (x, Free (x, T)) NONE) gen 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

962 
> fold_rev (fn (x, T) => fn prf' => prf' %> Var (Name.clean_index (x, idx), T)) gen 
730251503341
proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation);
wenzelm
parents:
70824
diff
changeset

963 
end; 
19908  964 

965 

70397  966 
(* instantiation *) 
11519  967 

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

969 
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

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

971 
(Term_Subst.instantiateT_same instT)); 
11519  972 

973 

70397  974 
(* lifting *) 
11519  975 

976 
fun lift_proof Bi inc prop prf = 

977 
let 

32024  978 
fun lift'' Us Ts t = 
59787  979 
strip_abs Ts (Logic.incr_indexes ([], Us, inc) (mk_abs Ts t)); 
11519  980 

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

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

984 
 lift' Us Ts (AbsP (s, t, prf)) = 
32024  985 
(AbsP (s, Same.map_option (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf) 
32019  986 
handle Same.SAME => AbsP (s, t, lift' Us Ts prf)) 
15570  987 
 lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t 
32024  988 
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

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

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

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

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

997 
 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

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

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

11519  1002 

18030  1003 
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop); 
11519  1004 
val k = length ps; 
1005 

23178  1006 
fun mk_app b (i, j, prf) = 
11615  1007 
if b then (i1, j, prf %% PBound i) else (i, j1, prf %> Bound j); 
11519  1008 

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

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

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

1017 
mk_AbsP ps (lift [] [] 0 0 Bi) 
11519  1018 
end; 
1019 

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

1021 
Same.commit (map_proof_terms_same 
59787  1022 
(Logic.incr_indexes_same ([], [], i)) (Logic.incr_tvar_same i)); 
32027  1023 

11519  1024 

70397  1025 
(* proof by assumption *) 
11519  1026 

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

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

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

1029 
fun imp_prf _ i 0 = PBound i 
56245  1030 
 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

1031 
 imp_prf _ i _ = PBound i; 
56245  1032 
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

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

1034 
in all_prf t end; 
11519  1035 

1036 
fun assumption_proof Bs Bi n prf = 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

1037 
mk_AbsP Bs (proof_combP (prf, map PBound (length Bs  1 downto 0) @ [mk_asm_prf Bi n ~1])); 
11519  1038 

1039 

70397  1040 
(* composition of object rule with proof state *) 
11519  1041 

56245  1042 
fun flatten_params_proof i j n (Const ("Pure.imp", _) $ A $ B, k) = 
15531  1043 
AbsP ("H", NONE (*A*), flatten_params_proof (i+1) j n (B, k)) 
56245  1044 
 flatten_params_proof i j n (Const ("Pure.all", _) $ Abs (a, T, t), k) = 
15531  1045 
Abst (a, NONE (*T*), flatten_params_proof i (j+1) n (t, k)) 
11519  1046 
 flatten_params_proof i j n (_, k) = proof_combP (proof_combt (PBound (k+i), 
19304  1047 
map Bound (j1 downto 0)), map PBound (remove (op =) (in) (i1 downto 0))); 
11519  1048 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

1049 
fun bicompose_proof flatten Bs As A oldAs n m rprf sprf = 
11519  1050 
let 
1051 
val lb = length Bs; 

70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

1052 
val la = length As; 
11519  1053 
in 
70822
22e2f5acc0b4
more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons;
wenzelm
parents:
70815
diff
changeset

1054 
mk_AbsP (Bs @ As) (proof_combP (sprf, 
11615  1055 
map PBound (lb + la  1 downto la)) %% 
23296
25f28f9c28a3
Adapted Proofterm.bicompose_proof to Larry's changes in
berghofe
parents:
23178
diff
changeset

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

11519  1059 
end; 
1060 

1061 

70397  1062 

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

1064 

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

1065 
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

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

1068 
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

1069 
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

1070 
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

1071 
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

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

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

1074 
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

1075 
 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

1076 
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

1077 

70458  1078 
fun of_sort_proof algebra classrel_proof arity_proof hyps = 
1079 
Sorts.of_sort_derivation algebra 

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

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

1082 
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

1083 
let val Ss = map (map snd) dom and prfs = maps (map fst) dom 
70458  1084 
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

1085 
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

1086 

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

1087 

70420  1088 

70397  1089 
(** axioms and theorems **) 
11519  1090 

70948
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1091 
val add_type_variables = (fold_types o fold_atyps) (insert (op =)); 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1092 
fun type_variables_of t = rev (add_type_variables t []); 
70810  1093 

70948
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1094 
val add_variables = fold_aterms (fn a => (is_Var a orelse is_Free a) ? insert (op =) a); 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1095 
fun variables_of t = rev (add_variables t []); 
11519  1096 

1097 
fun test_args _ [] = true 

1098 
 test_args is (Bound i :: ts) = 

17492  1099 
not (member (op =) is i) andalso test_args (i :: is) ts 
11519  1100 
 test_args _ _ = false; 
1101 

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

1103 
 is_fun (TVar _) = true 

1104 
 is_fun _ = false; 

1105 

70948
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1106 
fun vars_of t = map Var (rev (Term.add_vars t [])); 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1107 

11519  1108 
fun add_funvars Ts (vs, t) = 
1109 
if is_fun (fastype_of1 (Ts, t)) then 

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

1111 
if is_fun T then SOME ixn else NONE  _ => NONE) (vars_of t)) 
11519  1112 
else vs; 
1113 

56245  1114 
fun add_npvars q p Ts (vs, Const ("Pure.imp", _) $ t $ u) = 
11519  1115 
add_npvars q p Ts (add_npvars q (not p) Ts (vs, t), u) 
56245  1116 
 add_npvars q p Ts (vs, Const ("Pure.all", Type (_, [Type (_, [T, _]), _])) $ t) = 
11519  1117 
add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t) 
12041  1118 
 add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t) 
1119 
 add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t) 

64566  1120 
and add_npvars' Ts (vs, t) = 
1121 
(case strip_comb t of 

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

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

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

11519  1128 

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

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

1133 
fun is_proj t = 

1134 
let 

64566  1135 
fun is_p i t = 
1136 
(case strip_comb t of 

63857  1137 
(Bound _, []) => false 
11519  1138 
 (Bound j, ts) => j >= i orelse exists (is_p i) ts 
1139 
 (Abs (_, _, u), _) => is_p (i+1) u 

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

64566  1141 
in 
1142 
(case strip_abs_body t of 

1143 
Bound _ => true 

1144 
 t' => is_p 0 t') 

11519  1145 
end; 
1146 

70416  1147 
fun prop_args prop = 
1148 
let 

1149 
val needed_vars = 

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

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

1152 
(prop_vars prop); 

70948
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1153 
in 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1154 
variables_of prop > map 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1155 
(fn var as Var (ixn, _) => if member (op =) needed_vars ixn then SOME var else NONE 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1156 
 free => SOME free) 
5ed8c7e826a2
proper order of variables, independently of varify/unvarify state  relevant for export of locale conclusions;
wenzelm
parents:
70916
diff
changeset

1157 
end; 
11519  1158 

70835
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1159 
fun const_proof mk name prop = 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1160 
let 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1161 
val args = prop_args prop; 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1162 
val ({outer_constraints, ...}, prop1) = Logic.unconstrainT [] prop; 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1163 
val head = mk (name, prop1, NONE); 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1164 
in proof_combP (proof_combt' (head, args), map OfClass outer_constraints) end; 
17017  1165 

70835
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1166 
val axm_proof = const_proof PAxm; 
2d991e01a671
proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps;
wenzelm
parents:
70834
diff
changeset

1167 
val oracle_proof = const_proof Oracle; 
11519  1168 

63623  1169 
val shrink_proof = 
17492  1170 
let 
1171 
fun shrink ls lev (prf as Abst (a, T, body)) = 

1172 
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

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

1176 
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

1177 
ch, if ch then AbsP (a, t, body') else prf) 
17492  1178 
end 
1179 
 shrink ls lev prf = 

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

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

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

1183 
let 

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

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

33042  1186 
in (union (op =) is is', ch orelse ch', ts', 
17492  1187 
if ch orelse ch' then prf'' %% prf' else prf) 
1188 
end 

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

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

1191 
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

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

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

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

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

1201 
 shrink' _ _ ts prfs prf = 

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

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

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

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

1208 
 _ => raise Fail "shrink: proof not in normal form"); 
17492  1209 
val vs = vars_of prop; 
19012  1210 
val (ts', ts'') = chop (length vs) ts; 
33957  1211 
val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts'; 
17492  1212 
val nvs = Library.foldl (fn (ixns', (ixn, ixns)) => 
64566  1213 
insert (op =) ixn 
1214 
(case AList.lookup (op =) insts ixn of 

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

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

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

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

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

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

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

1228 

70397  1229 

70420  1230 
(** axioms for equality **) 
1231 

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

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

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

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

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

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

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

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

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

1241 

1242 
val equality_axms = 

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

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

1245 
("transitive", 

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

1247 
("equal_intr", 

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

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

1250 
("abstract_rule", 

1251 
Logic.mk_implies 

70814  1252 
(Logic.all x (Logic.mk_equals (f $ x, g $ x)), 
1253 
Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))), 

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

1256 

1257 
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm, 

1258 
equal_elim_axm, abstract_rule_axm, combination_axm] = 

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

1260 

70814  1261 
val reflexive_proof = reflexive_axm % NONE; 
1262 

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

70420  1264 

70814  1265 
fun symmetric_proof prf = 
1266 
if is_reflexive_proof prf then prf 

1267 
else symmetric_axm % NONE % NONE %% prf; 

70420  1268 

70814  1269 
fun transitive_proof U u prf1 prf2 = 
1270 
if is_reflexive_proof prf1 then prf2 

1271 
else if is_reflexive_proof prf2 then prf1 

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

1273 
else transitive_axm % NONE % NONE % NONE %% prf1 %% prf2; 

70420  1274 

70814  1275 
fun equal_intr_proof A B prf1 prf2 = 
