author  wenzelm 
Tue, 22 Oct 2019 20:08:25 +0200  
changeset 70922  539dfd4c166b 
parent 70915  bd4d37edfee4 
child 71006  41685289b8eb 
permissions  rwrr 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/more_thm.ML 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

3 

22907  4 
Further operations on type ctyp/cterm/thm, outside the inference kernel. 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

5 
*) 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

6 

23169  7 
infix aconvc; 
8 

32842  9 
signature BASIC_THM = 
10 
sig 

11 
include BASIC_THM 

61268  12 
val show_consts: bool Config.T 
13 
val show_hyps: bool Config.T 

14 
val show_tags: bool Config.T 

32842  15 
structure Ctermtab: TABLE 
16 
structure Thmtab: TABLE 

17 
val aconvc: cterm * cterm > bool 

45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
43780
diff
changeset

18 
type attribute = Context.generic * thm > Context.generic option * thm option 
32842  19 
end; 
20 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

21 
signature THM = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

22 
sig 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

23 
include THM 
32842  24 
structure Ctermtab: TABLE 
25 
structure Thmtab: TABLE 

60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

26 
val eq_ctyp: ctyp * ctyp > bool 
24948  27 
val aconvc: cterm * cterm > bool 
60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

28 
val add_tvars: thm > ctyp list > ctyp list 
60818  29 
val add_frees: thm > cterm list > cterm list 
30 
val add_vars: thm > cterm list > cterm list 

70159  31 
val dest_funT: ctyp > ctyp * ctyp 
70152  32 
val strip_type: ctyp > ctyp list * ctyp 
60938  33 
val all_name: Proof.context > string * cterm > cterm > cterm 
34 
val all: Proof.context > cterm > cterm > cterm 

22907  35 
val mk_binop: cterm > cterm > cterm > cterm 
36 
val dest_binop: cterm > cterm * cterm 

37 
val dest_implies: cterm > cterm * cterm 

38 
val dest_equals: cterm > cterm * cterm 

39 
val dest_equals_lhs: cterm > cterm 

40 
val dest_equals_rhs: cterm > cterm 

41 
val lhs_of: thm > cterm 

42 
val rhs_of: thm > cterm 

70586  43 
val fast_term_ord: cterm ord 
44 
val term_ord: cterm ord 

45 
val thm_ord: thm ord 

32842  46 
val cterm_cache: (cterm > 'a) > cterm > 'a 
47 
val thm_cache: (thm > 'a) > thm > 'a 

23599  48 
val is_reflexive: thm > bool 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

49 
val eq_thm: thm * thm > bool 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

50 
val eq_thm_prop: thm * thm > bool 
52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset

51 
val eq_thm_strict: thm * thm > bool 
60817  52 
val equiv_thm: theory > thm * thm > bool 
31944  53 
val class_triv: theory > class > thm 
54 
val of_sort: ctyp * sort > thm list 

24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

55 
val is_dummy: thm > bool 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

56 
val add_thm: thm > thm list > thm list 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

57 
val del_thm: thm > thm list > thm list 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

58 
val merge_thms: thm list * thm list > thm list 
33453  59 
val full_rules: thm Item_Net.T 
30560  60 
val intro_rules: thm Item_Net.T 
61 
val elim_rules: thm Item_Net.T 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

62 
val declare_hyps: cterm > Proof.context > Proof.context 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

63 
val assume_hyps: cterm > Proof.context > thm * Proof.context 
54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

64 
val unchecked_hyps: Proof.context > Proof.context 
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

65 
val restore_hyps: Proof.context > Proof.context > Proof.context 
55633  66 
val undeclared_hyps: Context.generic > thm > term list 
54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

67 
val check_hyps: Context.generic > thm > thm 
61508  68 
val declare_term_sorts: term > Proof.context > Proof.context 
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

69 
val extra_shyps': Proof.context > thm > sort list 
61508  70 
val check_shyps: Proof.context > thm > thm 
71 
val weaken_sorts': Proof.context > cterm > cterm 

27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

72 
val elim_implies: thm > thm > thm 
61339  73 
val forall_intr_name: string * cterm > thm > thm 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

74 
val forall_elim_var: int > thm > thm 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

75 
val forall_elim_vars: int > thm > thm 
67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

76 
val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list > thm > thm 
60801  77 
val instantiate': ctyp option list > cterm option list > thm > thm 
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

78 
val forall_intr_frees: thm > thm 
60825  79 
val unvarify_global: theory > thm > thm 
80 
val unvarify_axiom: theory > string > thm 

59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

81 
val rename_params_rule: string list * int > thm > thm 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

82 
val rename_boundvars: term > term > thm > thm 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

83 
val add_axiom: Proof.context > binding * term > theory > (string * thm) * theory 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

84 
val add_axiom_global: binding * term > theory > (string * thm) * theory 
61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset

85 
val add_def: Defs.context > bool > bool > binding * term > theory > (string * thm) * theory 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

86 
val add_def_global: bool > bool > binding * term > theory > (string * thm) * theory 
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
43780
diff
changeset

87 
type attribute = Context.generic * thm > Context.generic option * thm option 
30210  88 
type binding = binding * attribute list 
46830  89 
val tag_rule: string * string > thm > thm 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

90 
val untag_rule: string > thm > thm 
61852  91 
val is_free_dummy: thm > bool 
92 
val tag_free_dummy: thm > thm 

30342  93 
val def_name: string > string 
94 
val def_name_optional: string > string > string 

35238  95 
val def_binding: Binding.binding > Binding.binding 
30433
ce5138c92ca7
added def_binding_optional  robust version of def_name_optional for bindings;
wenzelm
parents:
30342
diff
changeset

96 
val def_binding_optional: Binding.binding > Binding.binding > Binding.binding 
62093  97 
val make_def_binding: bool > Binding.binding > Binding.binding 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

98 
val has_name_hint: thm > bool 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

99 
val get_name_hint: thm > string 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

100 
val put_name_hint: string > thm > thm 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

101 
val theoremK: string 
42473  102 
val legacy_get_kind: thm > string 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

103 
val kind_rule: string > thm > thm 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

104 
val rule_attribute: thm list > (Context.generic > thm > thm) > attribute 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

105 
val declaration_attribute: (thm > Context.generic > Context.generic) > attribute 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

106 
val mixed_attribute: (Context.generic * thm > Context.generic * thm) > attribute 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

107 
val apply_attribute: attribute > thm > Context.generic > thm * Context.generic 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

108 
val attribute_declaration: attribute > thm > Context.generic > Context.generic 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

109 
val theory_attributes: attribute list > thm > theory > thm * theory 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

110 
val proof_attributes: attribute list > thm > Proof.context > thm * Proof.context 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

111 
val no_attributes: 'a > 'a * 'b list 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

112 
val simple_fact: 'a > ('a * 'b list) list 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

113 
val tag: string * string > attribute 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

114 
val untag: string > attribute 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

115 
val kind: string > attribute 
70449  116 
val reconstruct_proof_of: thm > Proofterm.proof 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

117 
val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header > string option} > 
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

118 
thm > Proofterm.proof 
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset

119 
val register_proofs: thm list lazy > theory > theory 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
64568
diff
changeset

120 
val consolidate_theory: theory > unit 
61268  121 
val show_consts: bool Config.T 
122 
val show_hyps: bool Config.T 

123 
val show_tags: bool Config.T 

124 
val pretty_thm_raw: Proof.context > {quote: bool, show_hyps: bool} > thm > Pretty.T 

125 
val pretty_thm: Proof.context > thm > Pretty.T 

126 
val pretty_thm_item: Proof.context > thm > Pretty.T 

127 
val pretty_thm_global: theory > thm > Pretty.T 

128 
val string_of_thm: Proof.context > thm > string 

129 
val string_of_thm_global: theory > thm > string 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

130 
end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

131 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

132 
structure Thm: THM = 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

133 
struct 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

134 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

135 
(** basic operations **) 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

136 

60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

137 
(* collecting ctyps and cterms *) 
23491  138 

60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

139 
val eq_ctyp = op = o apply2 Thm.typ_of; 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58001
diff
changeset

140 
val op aconvc = op aconv o apply2 Thm.term_of; 
23491  141 

60952
762cb38a3147
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60951
diff
changeset

142 
val add_tvars = Thm.fold_atomic_ctyps (fn a => is_TVar (Thm.typ_of a) ? insert eq_ctyp a); 
60818  143 
val add_frees = Thm.fold_atomic_cterms (fn a => is_Free (Thm.term_of a) ? insert (op aconvc) a); 
144 
val add_vars = Thm.fold_atomic_cterms (fn a => is_Var (Thm.term_of a) ? insert (op aconvc) a); 

23491  145 

146 

70155  147 
(* ctyp operations *) 
70152  148 

70159  149 
fun dest_funT cT = 
70155  150 
(case Thm.typ_of cT of 
151 
Type ("fun", _) => let val [A, B] = Thm.dest_ctyp cT in (A, B) end 

70159  152 
 T => raise TYPE ("dest_funT", [T], [])); 
70152  153 

154 
(* ctyp version of strip_type: maps [T1,...,Tn]>T to ([T1,T2,...,Tn], T) *) 

155 
fun strip_type cT = 

156 
(case Thm.typ_of cT of 

157 
Type ("fun", _) => 

158 
let 

70159  159 
val (cT1, cT2) = dest_funT cT; 
70152  160 
val (cTs, cT') = strip_type cT2 
161 
in (cT1 :: cTs, cT') end 

162 
 _ => ([], cT)); 

163 

164 

70155  165 
(* cterm operations *) 
22907  166 

60938  167 
fun all_name ctxt (x, t) A = 
32198  168 
let 
59586  169 
val T = Thm.typ_of_cterm t; 
60938  170 
val all_const = Thm.cterm_of ctxt (Const ("Pure.all", (T > propT) > propT)); 
171 
in Thm.apply all_const (Thm.lambda_name (x, t) A) end; 

32198  172 

60938  173 
fun all ctxt t A = all_name ctxt ("", t) A; 
32198  174 

46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
45382
diff
changeset

175 
fun mk_binop c a b = Thm.apply (Thm.apply c a) b; 
22907  176 
fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct); 
177 

178 
fun dest_implies ct = 

179 
(case Thm.term_of ct of 

56245  180 
Const ("Pure.imp", _) $ _ $ _ => dest_binop ct 
22907  181 
 _ => raise TERM ("dest_implies", [Thm.term_of ct])); 
182 

183 
fun dest_equals ct = 

184 
(case Thm.term_of ct of 

56245  185 
Const ("Pure.eq", _) $ _ $ _ => dest_binop ct 
22907  186 
 _ => raise TERM ("dest_equals", [Thm.term_of ct])); 
187 

188 
fun dest_equals_lhs ct = 

189 
(case Thm.term_of ct of 

56245  190 
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg1 ct 
22907  191 
 _ => raise TERM ("dest_equals_lhs", [Thm.term_of ct])); 
192 

193 
fun dest_equals_rhs ct = 

194 
(case Thm.term_of ct of 

56245  195 
Const ("Pure.eq", _) $ _ $ _ => Thm.dest_arg ct 
22907  196 
 _ => raise TERM ("dest_equals_rhs", [Thm.term_of ct])); 
197 

198 
val lhs_of = dest_equals_lhs o Thm.cprop_of; 

199 
val rhs_of = dest_equals_rhs o Thm.cprop_of; 

200 

201 

67559  202 
(* certified term order *) 
203 

204 
val fast_term_ord = Term_Ord.fast_term_ord o apply2 Thm.term_of; 

205 
val term_ord = Term_Ord.term_ord o apply2 Thm.term_of; 

206 

207 

22907  208 
(* thm order: ignores theory context! *) 
22682  209 

70464  210 
val thm_ord = 
211 
Term_Ord.fast_term_ord o apply2 Thm.prop_of 

212 
<<< list_ord (prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord) o apply2 Thm.tpairs_of 

213 
<<< list_ord Term_Ord.fast_term_ord o apply2 Thm.hyps_of 

214 
<<< list_ord Term_Ord.sort_ord o apply2 Thm.shyps_of; 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

215 

22682  216 

32842  217 
(* tables and caches *) 
218 

67559  219 
structure Ctermtab = Table(type key = cterm val ord = fast_term_ord); 
32842  220 
structure Thmtab = Table(type key = thm val ord = thm_ord); 
221 

222 
fun cterm_cache f = Cache.create Ctermtab.empty Ctermtab.lookup Ctermtab.update f; 

223 
fun thm_cache f = Cache.create Thmtab.empty Thmtab.lookup Thmtab.update f; 

224 

225 

22682  226 
(* equality *) 
227 

23599  228 
fun is_reflexive th = op aconv (Logic.dest_equals (Thm.prop_of th)) 
229 
handle TERM _ => false; 

230 

55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOLIMP);
wenzelm
parents:
54996
diff
changeset

231 
val eq_thm = is_equal o thm_ord; 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

232 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58001
diff
changeset

233 
val eq_thm_prop = op aconv o apply2 Thm.full_prop_of; 
22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

234 

52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset

235 
fun eq_thm_strict ths = 
55547
384bfd19ee61
subtle change of semantics of Thm.eq_thm, e.g. relevant for merge of src/HOL/Tools/Predicate_Compile/core_data.ML (cf. HOLIMP);
wenzelm
parents:
54996
diff
changeset

236 
eq_thm ths andalso 
65458  237 
Context.eq_thy_id (apply2 Thm.theory_id ths) andalso 
61040  238 
op = (apply2 Thm.maxidx_of ths) andalso 
239 
op = (apply2 Thm.get_tags ths); 

52683
fb028440473e
more official Thm.eq_thm_strict, without demanding ML equality type;
wenzelm
parents:
51316
diff
changeset

240 

22682  241 

242 
(* pattern equivalence *) 

243 

60817  244 
fun equiv_thm thy ths = 
245 
Pattern.equiv thy (apply2 (Thm.full_prop_of o Thm.transfer thy) ths); 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

246 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

247 

31904
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset

248 
(* type classes and sorts *) 
a86896359ca4
renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
wenzelm
parents:
31177
diff
changeset

249 

31944  250 
fun class_triv thy c = 
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59616
diff
changeset

251 
Thm.of_class (Thm.global_ctyp_of thy (TVar ((Name.aT, 0), [c])), c); 
31944  252 

253 
fun of_sort (T, S) = map (fn c => Thm.of_class (T, c)) S; 

28621
a60164e8fff0
added check_shyps, which reject pending sort hypotheses;
wenzelm
parents:
28116
diff
changeset

254 

a60164e8fff0
added check_shyps, which reject pending sort hypotheses;
wenzelm
parents:
28116
diff
changeset

255 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

256 
(* misc operations *) 
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

257 

24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

258 
fun is_dummy thm = 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

259 
(case try Logic.dest_term (Thm.concl_of thm) of 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

260 
NONE => false 
58001
934d85f14d1d
more general dummy: may contain "parked arguments", for example;
wenzelm
parents:
56245
diff
changeset

261 
 SOME t => Term.is_dummy_pattern (Term.head_of t)); 
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

262 

22695
17073e9b94f2
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
wenzelm
parents:
22682
diff
changeset

263 

30564  264 
(* collections of theorems in canonical order *) 
24048
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

265 

a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

266 
val add_thm = update eq_thm_prop; 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

267 
val del_thm = remove eq_thm_prop; 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

268 
val merge_thms = merge eq_thm_prop; 
a12b4faff474
moved Drule.add/del/merge_rules to Thm.add/del/merge_thms;
wenzelm
parents:
23599
diff
changeset

269 

33453  270 
val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of); 
33373  271 
val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of); 
272 
val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of); 

30560  273 

274 

22682  275 

61508  276 
(** declared hyps and sort hyps **) 
54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

277 

da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

278 
structure Hyps = Proof_Data 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

279 
( 
61508  280 
type T = {checked_hyps: bool, hyps: Termtab.set, shyps: sort Ord_List.T}; 
281 
fun init _ : T = {checked_hyps = true, hyps = Termtab.empty, shyps = []}; 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

282 
); 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

283 

61508  284 
fun map_hyps f = Hyps.map (fn {checked_hyps, hyps, shyps} => 
285 
let val (checked_hyps', hyps', shyps') = f (checked_hyps, hyps, shyps) 

286 
in {checked_hyps = checked_hyps', hyps = hyps', shyps = shyps'} end); 

287 

288 

289 
(* hyps *) 

290 

291 
fun declare_hyps raw_ct ctxt = ctxt > map_hyps (fn (checked_hyps, hyps, shyps) => 

292 
let 

293 
val ct = Thm.transfer_cterm (Proof_Context.theory_of ctxt) raw_ct; 

294 
val hyps' = Termtab.update (Thm.term_of ct, ()) hyps; 

295 
in (checked_hyps, hyps', shyps) end); 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

296 

da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

297 
fun assume_hyps ct ctxt = (Thm.assume ct, declare_hyps ct ctxt); 
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

298 

61508  299 
val unchecked_hyps = map_hyps (fn (_, hyps, shyps) => (false, hyps, shyps)); 
300 

301 
fun restore_hyps ctxt = 

302 
map_hyps (fn (_, hyps, shyps) => (#checked_hyps (Hyps.get ctxt), hyps, shyps)); 

54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

303 

55633  304 
fun undeclared_hyps context th = 
305 
Thm.hyps_of th 

306 
> filter_out 

307 
(case context of 

308 
Context.Theory _ => K false 

309 
 Context.Proof ctxt => 

310 
(case Hyps.get ctxt of 

61508  311 
{checked_hyps = false, ...} => K true 
312 
 {hyps, ...} => Termtab.defined hyps)); 

55633  313 

54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

314 
fun check_hyps context th = 
55633  315 
(case undeclared_hyps context th of 
316 
[] => th 

317 
 undeclared => 

61263  318 
error (Pretty.string_of (Pretty.big_list "Undeclared hyps:" 
319 
(map (Pretty.item o single o Syntax.pretty_term (Syntax.init_pretty context)) undeclared)))); 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

320 

da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

321 

61508  322 
(* shyps *) 
323 

324 
fun declare_term_sorts t = 

325 
map_hyps (fn (checked_hyps, hyps, shyps) => 

326 
(checked_hyps, hyps, Sorts.insert_term t shyps)); 

327 

61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

328 
fun extra_shyps' ctxt th = 
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

329 
Sorts.subtract (#shyps (Hyps.get ctxt)) (Thm.extra_shyps th); 
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

330 

61508  331 
fun check_shyps ctxt raw_th = 
332 
let 

333 
val th = Thm.strip_shyps raw_th; 

61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

334 
val extra_shyps = extra_shyps' ctxt th; 
61508  335 
in 
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

336 
if null extra_shyps then th 
61508  337 
else error (Pretty.string_of (Pretty.block (Pretty.str "Pending sort hypotheses:" :: 
61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

338 
Pretty.brk 1 :: Pretty.commas (map (Syntax.pretty_sort ctxt) extra_shyps)))) 
61508  339 
end; 
340 

341 
val weaken_sorts' = Thm.weaken_sorts o #shyps o Hyps.get; 

342 

343 

54984
da70ab8531f4
more elementary management of declared hyps, below structure Assumption;
wenzelm
parents:
53206
diff
changeset

344 

24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

345 
(** basic derived rules **) 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

346 

16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

347 
(*Elimination of implication 
67721  348 
A A \<Longrightarrow> B 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

349 
 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

350 
B 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

351 
*) 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

352 
fun elim_implies thA thAB = Thm.implies_elim thAB thA; 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

353 

26653  354 

61339  355 
(* forall_intr_name *) 
356 

357 
fun forall_intr_name (a, x) th = 

358 
let 

359 
val th' = Thm.forall_intr x th; 

360 
val prop' = (case Thm.prop_of th' of all $ Abs (_, T, b) => all $ Abs (a, T, b)); 

361 
in Thm.renamed_prop prop' th' end; 

362 

363 

26653  364 
(* forall_elim_var(s) *) 
365 

366 
local 

367 

60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

368 
fun dest_all ct = 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

369 
(case Thm.term_of ct of 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

370 
Const ("Pure.all", _) $ Abs (a, _, _) => 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

371 
let val (x, ct') = Thm.dest_abs NONE (Thm.dest_arg ct) 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

372 
in SOME ((a, Thm.ctyp_of_cterm x), ct') end 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

373 
 _ => NONE); 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

374 

b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

375 
fun dest_all_list ct = 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

376 
(case dest_all ct of 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

377 
NONE => [] 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

378 
 SOME (v, ct') => v :: dest_all_list ct'); 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

379 

b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

380 
fun forall_elim_vars_list vars i th = 
26653  381 
let 
60950  382 
val used = 
383 
(Thm.fold_terms o Term.fold_aterms) 

384 
(fn Var ((x, j), _) => if i = j then insert (op =) x else I  _ => I) th []; 

60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

385 
val vars' = (Name.variant_list used (map #1 vars), vars) 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

386 
> ListPair.map (fn (x, (_, T)) => Thm.var ((x, i), T)); 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

387 
in fold Thm.forall_elim vars' th end; 
26653  388 

389 
in 

390 

60950  391 
fun forall_elim_vars i th = 
60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

392 
forall_elim_vars_list (dest_all_list (Thm.cprop_of th)) i th; 
26653  393 

33697  394 
fun forall_elim_var i th = 
60950  395 
let 
396 
val vars = 

60951
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

397 
(case dest_all (Thm.cprop_of th) of 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

398 
SOME (v, _) => [v] 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

399 
 NONE => raise THM ("forall_elim_var", i, [th])); 
b70c4db3874f
produce certified vars without access to theory_of_thm, and without context;
wenzelm
parents:
60950
diff
changeset

400 
in forall_elim_vars_list vars i th end; 
26653  401 

402 
end; 

403 

404 

67698
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

405 
(* instantiate frees *) 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

406 

67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

407 
fun instantiate_frees ([], []) th = th 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

408 
 instantiate_frees (instT, inst) th = 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

409 
let 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

410 
val idx = Thm.maxidx_of th + 1; 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

411 
fun index ((a, A), b) = (((a, idx), A), b); 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

412 
val insts = (map index instT, map index inst); 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

413 
val frees = (map (#1 o #1) instT, map (#1 o #1) inst); 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

414 

67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

415 
val hyps = Thm.chyps_of th; 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

416 
val inst_cterm = 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

417 
Thm.generalize_cterm frees idx #> 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

418 
Thm.instantiate_cterm insts; 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

419 
in 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

420 
th 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

421 
> fold_rev Thm.implies_intr hyps 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

422 
> Thm.generalize frees idx 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

423 
> Thm.instantiate insts 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

424 
> fold (elim_implies o Thm.assume o inst_cterm) hyps 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

425 
end; 
67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

426 

67caf783b9ee
explicit operations to instantiate frees: typ, term, thm, morphism;
wenzelm
parents:
67671
diff
changeset

427 

60801  428 
(* instantiate by lefttoright occurrence of variables *) 
429 

430 
fun instantiate' cTs cts thm = 

431 
let 

432 
fun err msg = 

433 
raise TYPE ("instantiate': " ^ msg, 

434 
map_filter (Option.map Thm.typ_of) cTs, 

435 
map_filter (Option.map Thm.term_of) cts); 

436 

437 
fun zip_vars xs ys = 

438 
zip_options xs ys handle ListPair.UnequalLengths => 

439 
err "more instantiations than variables in thm"; 

440 

441 
val thm' = 

442 
Thm.instantiate ((zip_vars (rev (Thm.fold_terms Term.add_tvars thm [])) cTs), []) thm; 

443 
val thm'' = 

444 
Thm.instantiate ([], zip_vars (rev (Thm.fold_terms Term.add_vars thm' [])) cts) thm'; 

445 
in thm'' end; 

446 

447 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

448 
(* forall_intr_frees: generalization over all suitable Free variables *) 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

449 

0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

450 
fun forall_intr_frees th = 
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

451 
let 
61041  452 
val fixed = 
453 
fold Term.add_frees (Thm.terms_of_tpairs (Thm.tpairs_of th) @ Thm.hyps_of th) []; 

60821  454 
val frees = 
455 
Thm.fold_atomic_cterms (fn a => 

456 
(case Thm.term_of a of 

457 
Free v => not (member (op =) fixed v) ? insert (op aconvc) a 

458 
 _ => I)) th []; 

459 
in fold Thm.forall_intr frees th end; 

35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

460 

0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35857
diff
changeset

461 

35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35715
diff
changeset

462 
(* unvarify_global: global schematic variables *) 
26653  463 

60825  464 
fun unvarify_global thy th = 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

465 
let 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

466 
val prop = Thm.full_prop_of th; 
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
35715
diff
changeset

467 
val _ = map Logic.unvarify_global (prop :: Thm.hyps_of th) 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

468 
handle TERM (msg, _) => raise THM (msg, 0, [th]); 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

469 

32279  470 
val instT = rev (Term.add_tvars prop []) > map (fn v as ((a, _), S) => (v, TFree (a, S))); 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

471 
val inst = rev (Term.add_vars prop []) > map (fn ((a, i), T) => 
32279  472 
let val T' = Term_Subst.instantiateT instT T 
60805  473 
in (((a, i), T'), Thm.global_cterm_of thy (Free ((a, T')))) end); 
474 
in Thm.instantiate (map (apsnd (Thm.global_ctyp_of thy)) instT, inst) th end; 

24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

475 

60825  476 
fun unvarify_axiom thy = unvarify_global thy o Thm.axiom thy; 
477 

26653  478 

59969
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

479 
(* user renaming of parameters in a subgoal *) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

480 

bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

481 
(*The names, if distinct, are used for the innermost parameters of subgoal i; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

482 
preceding parameters may be renamed to make all parameters distinct.*) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

483 
fun rename_params_rule (names, i) st = 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

484 
let 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

485 
val (_, Bs, Bi, C) = Thm.dest_state (st, i); 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

486 
val params = map #1 (Logic.strip_params Bi); 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

487 
val short = length params  length names; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

488 
val names' = 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

489 
if short < 0 then error "More names than parameters in subgoal!" 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

490 
else Name.variant_list names (take short params) @ names; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

491 
val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x  _ => I) Bi []; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

492 
val Bi' = Logic.list_rename_params names' Bi; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

493 
in 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

494 
(case duplicates (op =) names of 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

495 
a :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ a); st) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

496 
 [] => 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

497 
(case inter (op =) names free_names of 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

498 
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); st) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

499 
 [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st)) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

500 
end; 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

501 

bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

502 

bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

503 
(* preservation of bound variable names *) 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

504 

bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

505 
fun rename_boundvars pat obj th = 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

506 
(case Term.rename_abs pat obj (Thm.prop_of th) of 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

507 
NONE => th 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

508 
 SOME prop' => Thm.renamed_prop prop' th); 
bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

509 

bcccad156236
explicitly checked alpha conversion  actual renaming happens outside kernel;
wenzelm
parents:
59623
diff
changeset

510 

24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

511 

16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

512 
(** specification primitives **) 
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

513 

30342  514 
(* rules *) 
515 

35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

516 
fun stripped_sorts thy t = 
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

517 
let 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset

518 
val tfrees = rev (Term.add_tfrees t []); 
70922
539dfd4c166b
more conservative type names, e.g. relevant for Isabelle/MMT export;
wenzelm
parents:
70915
diff
changeset

519 
val tfrees' = map (fn a => (a, [])) (Name.variant_list [] (map #1 tfrees)); 
60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset

520 
val recover = 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset

521 
map2 (fn (a', S') => fn (a, S) => (((a', 0), S'), Thm.global_ctyp_of thy (TVar ((a, 0), S)))) 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset

522 
tfrees' tfrees; 
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
60367
diff
changeset

523 
val strip = map (apply2 TFree) (tfrees ~~ tfrees'); 
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

524 
val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t; 
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

525 
in (strip, recover, t') end; 
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

526 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

527 
fun add_axiom ctxt (b, prop) thy = 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

528 
let 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

529 
val _ = Sign.no_vars ctxt prop; 
35855
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

530 
val (strip, recover, prop') = stripped_sorts thy prop; 
e7d004b89ca8
add_axiom: axiomatize "unconstrained" version, with explicit of_class premises;
wenzelm
parents:
35853
diff
changeset

531 
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip; 
60367  532 
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of ctxt T, S)) strip; 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

533 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

534 
val thy' = thy 
51316
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
49062
diff
changeset

535 
> Theory.add_axiom ctxt (b, Logic.list_implies (maps Logic.mk_of_sort constraints, prop')); 
dfe469293eb4
discontinued empty name bindings in 'axiomatization';
wenzelm
parents:
49062
diff
changeset

536 
val axm_name = Sign.full_name thy' b; 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

537 
val axm' = Thm.axiom thy' axm_name; 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

538 
val thm = 
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

539 
Thm.instantiate (recover, []) axm' 
60825  540 
> unvarify_global thy' 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

541 
> fold elim_implies of_sorts; 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

542 
in ((axm_name, thm), thy') end; 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

543 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

544 
fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; 
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

545 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset

546 
fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

547 
let 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

548 
val _ = Sign.no_vars ctxt prop; 
60367  549 
val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

550 
val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

551 

61261
ddb2da7cb2e4
more explicit Defs.context: use proper name spaces as far as possible;
wenzelm
parents:
61059
diff
changeset

552 
val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

553 
val axm_name = Sign.full_name thy' b; 
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

554 
val axm' = Thm.axiom thy' axm_name; 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

555 
val thm = 
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

556 
Thm.instantiate (recover, []) axm' 
60825  557 
> unvarify_global thy' 
35988
76ca601c941e
disallow premises in primitive Theory.add_def  handle in Thm.add_def;
wenzelm
parents:
35985
diff
changeset

558 
> fold_rev Thm.implies_intr prems; 
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35988
diff
changeset

559 
in ((axm_name, thm), thy') end; 
24980
16a74cfca971
added elim_implies (more convenient argument order);
wenzelm
parents:
24948
diff
changeset

560 

42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

561 
fun add_def_global unchecked overloaded arg thy = 
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset

562 
add_def (Defs.global_context thy) unchecked overloaded arg thy; 
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
40238
diff
changeset

563 

27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

564 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

565 

70443  566 
(** theorem tags **) 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

567 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

568 
(* add / delete tags *) 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

569 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

570 
fun tag_rule tg = Thm.map_tags (insert (op =) tg); 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

571 
fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

572 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

573 

61852  574 
(* free dummy thm  for abstract closure *) 
575 

576 
val free_dummyN = "free_dummy"; 

577 
fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN; 

578 
val tag_free_dummy = tag_rule (free_dummyN, ""); 

579 

580 

30342  581 
(* def_name *) 
582 

583 
fun def_name c = c ^ "_def"; 

584 

585 
fun def_name_optional c "" = def_name c 

586 
 def_name_optional _ name = name; 

587 

63041
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset

588 
val def_binding = Binding.map_name def_name #> Binding.reset_pos; 
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset

589 
fun def_binding_optional b name = if Binding.is_empty name then def_binding b else name; 
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
62093
diff
changeset

590 
fun make_def_binding cond b = if cond then def_binding b else Binding.empty; 
62093  591 

30342  592 

27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

593 
(* unofficial theorem names *) 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

594 

68036
4c9e79aeadf0
tuned  avoid spurious exception trace for "the";
wenzelm
parents:
67778
diff
changeset

595 
fun has_name_hint thm = AList.defined (op =) (Thm.get_tags thm) Markup.nameN; 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

596 
fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); 
68036
4c9e79aeadf0
tuned  avoid spurious exception trace for "the";
wenzelm
parents:
67778
diff
changeset

597 
fun get_name_hint thm = if has_name_hint thm then the_name_hint thm else "??.unknown"; 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

598 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

599 
fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

600 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

601 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

602 
(* theorem kinds *) 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

603 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

604 
val theoremK = "theorem"; 
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

605 

42473  606 
fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

607 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

608 
fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

609 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

610 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

611 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

612 
(** attributes **) 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

613 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

614 
(*attributes subsume any kind of rules or context modifiers*) 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

615 
type attribute = Context.generic * thm > Context.generic option * thm option; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

616 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

617 
type binding = binding * attribute list; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

618 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

619 
fun rule_attribute ths f (x, th) = 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

620 
(NONE, 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

621 
(case find_first is_free_dummy (th :: ths) of 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

622 
SOME th' => SOME th' 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

623 
 NONE => SOME (f x th))); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

624 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

625 
fun declaration_attribute f (x, th) = 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

626 
(if is_free_dummy th then NONE else SOME (f th x), NONE); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

627 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

628 
fun mixed_attribute f (x, th) = 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

629 
let val (x', th') = f (x, th) in (SOME x', SOME th') end; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

630 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

631 
fun apply_attribute (att: attribute) th x = 
67649  632 
let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th)) 
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

633 
in (the_default th th', the_default x x') end; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

634 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

635 
fun attribute_declaration att th x = #2 (apply_attribute att th x); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

636 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

637 
fun apply_attributes mk dest = 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

638 
let 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

639 
fun app [] th x = (th, x) 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

640 
 app (att :: atts) th x = apply_attribute att th (mk x) > dest > app atts; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

641 
in app end; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

642 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

643 
val theory_attributes = apply_attributes Context.Theory Context.the_theory; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

644 
val proof_attributes = apply_attributes Context.Proof Context.the_proof; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

645 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

646 
fun no_attributes x = (x, []); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

647 
fun simple_fact x = [(x, [])]; 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

648 

fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

649 
fun tag tg = rule_attribute [] (K (tag_rule tg)); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

650 
fun untag s = rule_attribute [] (K (untag_rule s)); 
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset

651 
fun kind k = rule_attribute [] (K (k <> "" ? kind_rule k)); 
27866
c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

652 

c721ea6e0eb4
moved basic thm operations from structure PureThy to Thm;
wenzelm
parents:
27255
diff
changeset

653 

70443  654 

655 
(** proof terms **) 

656 

70449  657 
fun reconstruct_proof_of thm = 
658 
Proofterm.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm); 

70443  659 

70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

660 
fun standard_proof_of {full, expand_name} thm = 
70839
2136e4670ad2
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
wenzelm
parents:
70830
diff
changeset

661 
let val thy = Thm.theory_of_thm thm in 
2136e4670ad2
clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof;
wenzelm
parents:
70830
diff
changeset

662 
reconstruct_proof_of thm 
70915
bd4d37edfee4
clarified expand_proof/expand_name: allow more detailed control via thm_header;
wenzelm
parents:
70914
diff
changeset

663 
> Proofterm.expand_proof thy expand_name 
70449  664 
> Proofterm.rew_proof thy 
70443  665 
> Proofterm.no_thm_proofs 
666 
> not full ? Proofterm.shrink_proof 

667 
end; 

668 

669 

70444  670 

70443  671 
(** forked proofs **) 
49010  672 

49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset

673 
structure Proofs = Theory_Data 
49010  674 
( 
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset

675 
type T = thm list lazy list; 
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49058
diff
changeset

676 
val empty = []; 
49010  677 
fun extend _ = empty; 
678 
fun merge _ = empty; 

679 
); 

680 

67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset

681 
fun register_proofs ths = 
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67649
diff
changeset

682 
(Proofs.map o cons) (Lazy.map_finished (map Thm.trim_context) ths); 
61059  683 

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

684 
fun consolidate_theory thy = 
67778
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset

685 
rev (Proofs.get thy) 
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset

686 
> maps (map (Thm.transfer thy) o Lazy.force) 
a25f9076a0b3
eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
wenzelm
parents:
67725
diff
changeset

687 
> Thm.consolidate; 
49010  688 

689 

61268  690 

691 
(** print theorems **) 

692 

693 
(* options *) 

694 

69575  695 
val show_consts = Config.declare_option_bool ("show_consts", \<^here>); 
696 
val show_hyps = Config.declare_bool ("show_hyps", \<^here>) (K false); 

697 
val show_tags = Config.declare_bool ("show_tags", \<^here>) (K false); 

61268  698 

699 

700 
(* pretty_thm etc. *) 

701 

702 
fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; 

703 
val pretty_tags = Pretty.list "[" "]" o map pretty_tag; 

704 

705 
fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th = 

706 
let 

707 
val show_tags = Config.get ctxt show_tags; 

708 
val show_hyps = Config.get ctxt show_hyps; 

709 

710 
val th = raw_th 

67649  711 
> perhaps (try (Thm.transfer' ctxt)) 
61268  712 
> perhaps (try Thm.strip_shyps); 
713 

714 
val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th; 

61509
358dfae15d83
print thm wrt. local shyps (from full proof context);
wenzelm
parents:
61508
diff
changeset

715 
val extra_shyps = extra_shyps' ctxt th; 
61268  716 
val tags = Thm.get_tags th; 
717 
val tpairs = Thm.tpairs_of th; 

718 

719 
val q = if quote then Pretty.quote else I; 

720 
val prt_term = q o Syntax.pretty_term ctxt; 

721 

722 

723 
val hlen = length extra_shyps + length hyps + length tpairs; 

724 
val hsymbs = 

725 
if hlen = 0 then [] 

726 
else if show_hyps orelse show_hyps' then 

727 
[Pretty.brk 2, Pretty.list "[" "]" 

70443  728 
(map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @ 
61268  729 
map (Syntax.pretty_sort ctxt) extra_shyps)] 
730 
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")]; 

731 
val tsymbs = 

732 
if null tags orelse not show_tags then [] 

733 
else [Pretty.brk 1, pretty_tags tags]; 

734 
in Pretty.block (prt_term (Thm.prop_of th) :: (hsymbs @ tsymbs)) end; 

735 

736 
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true}; 

737 
fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th]; 

738 

739 
fun pretty_thm_global thy = 

740 
pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false}; 

741 

742 
val string_of_thm = Pretty.string_of oo pretty_thm; 

743 
val string_of_thm_global = Pretty.string_of oo pretty_thm_global; 

744 

745 

22362
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

746 
open Thm; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

747 

6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

748 
end; 
6470ce514b6e
Further operations on type thm, outside the inference kernel.
wenzelm
parents:
diff
changeset

749 

32842  750 
structure Basic_Thm: BASIC_THM = Thm; 
751 
open Basic_Thm; 