author  wenzelm 
Sat, 19 Nov 2011 13:02:50 +0100  
changeset 45584  41a768a431a6 
parent 45390  e29521ef9059 
child 45601  d5178f19b671 
permissions  rwrr 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Isar/element.ML 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

3 

19777  4 
Explicit data structures for some Isar language elements, with derived 
5 
logical operations. 

18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

6 
*) 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

7 

691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

8 
signature ELEMENT = 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

9 
sig 
19259  10 
datatype ('typ, 'term) stmt = 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

11 
Shows of (Attrib.binding * ('term * 'term list) list) list  
29578  12 
Obtains of (binding * ((binding * 'typ option) list * 'term list)) list 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25739
diff
changeset

13 
type statement = (string, string) stmt 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25739
diff
changeset

14 
type statement_i = (typ, term) stmt 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

15 
datatype ('typ, 'term, 'fact) ctxt = 
29578  16 
Fixes of (binding * 'typ option * mixfix) list  
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

17 
Constrains of (string * 'typ) list  
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

18 
Assumes of (Attrib.binding * ('term * 'term list) list) list  
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

19 
Defines of (Attrib.binding * ('term * 'term list)) list  
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

20 
Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list 
26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25739
diff
changeset

21 
type context = (string, string, Facts.ref) ctxt 
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25739
diff
changeset

22 
type context_i = (typ, term, thm list) ctxt 
21581  23 
val facts_map: (('typ, 'term, 'fact) ctxt > ('a, 'b, 'c) ctxt) > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

24 
(Attrib.binding * ('fact * Attrib.src list) list) list > 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

25 
(Attrib.binding * ('c * Attrib.src list) list) list 
29603  26 
val map_ctxt: {binding: binding > binding, typ: 'typ > 'a, term: 'term > 'b, 
27 
pattern: 'term > 'b, fact: 'fact > 'c, attrib: Attrib.src > Attrib.src} > 

28 
('typ, 'term, 'fact) ctxt > ('a, 'b, 'c) ctxt 

21528  29 
val map_ctxt_attrib: (Attrib.src > Attrib.src) > 
30 
('typ, 'term, 'fact) ctxt > ('typ, 'term, 'fact) ctxt 

45290  31 
val transform_ctxt: morphism > context_i > context_i 
19777  32 
val pretty_stmt: Proof.context > statement_i > Pretty.T list 
33 
val pretty_ctxt: Proof.context > context_i > Pretty.T list 

34 
val pretty_statement: Proof.context > string > thm > Pretty.T 

35 
type witness 

29578  36 
val prove_witness: Proof.context > term > tactic > witness 
37 
val witness_proof: (witness list list > Proof.context > Proof.context) > 

38 
term list list > Proof.context > Proof.state 

39 
val witness_proof_eqs: (witness list list > thm list > Proof.context > Proof.context) > 

40 
term list list > term list > Proof.context > Proof.state 

41 
val witness_local_proof: (witness list list > Proof.state > Proof.state) > 

42 
string > term list list > Proof.context > bool > Proof.state > Proof.state 

38108  43 
val witness_local_proof_eqs: (witness list list > thm list > Proof.state > Proof.state) > 
44 
string > term list list > term list > Proof.context > bool > Proof.state > 

45 
Proof.state 

45290  46 
val transform_witness: morphism > witness > witness 
19777  47 
val conclude_witness: witness > thm 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

48 
val pretty_witness: Proof.context > witness > Pretty.T 
21481  49 
val instT_morphism: theory > typ Symtab.table > morphism 
50 
val inst_morphism: theory > typ Symtab.table * term Symtab.table > morphism 

51 
val satisfy_morphism: witness list > morphism 

36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36323
diff
changeset

52 
val eq_morphism: theory > thm list > morphism option 
29218  53 
val transfer_morphism: theory > morphism 
38108  54 
val generic_note_thmss: string > (Attrib.binding * (thm list * Attrib.src list) list) list > 
55 
Context.generic > (string * thm list) list * Context.generic 

30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

56 
val init: context_i > Context.generic > Context.generic 
30777
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

57 
val activate_i: context_i > Proof.context > context_i * Proof.context 
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

58 
val activate: (typ, term, Facts.ref) ctxt > Proof.context > context_i * Proof.context 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

59 
end; 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

60 

691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

61 
structure Element: ELEMENT = 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

62 
struct 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

63 

19777  64 
(** language elements **) 
65 

66 
(* statement *) 

19259  67 

68 
datatype ('typ, 'term) stmt = 

28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

69 
Shows of (Attrib.binding * ('term * 'term list) list) list  
29578  70 
Obtains of (binding * ((binding * 'typ option) list * 'term list)) list; 
19259  71 

72 
type statement = (string, string) stmt; 

73 
type statement_i = (typ, term) stmt; 

74 

75 

19777  76 
(* context *) 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

77 

691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

78 
datatype ('typ, 'term, 'fact) ctxt = 
29578  79 
Fixes of (binding * 'typ option * mixfix) list  
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

80 
Constrains of (string * 'typ) list  
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

81 
Assumes of (Attrib.binding * ('term * 'term list) list) list  
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

82 
Defines of (Attrib.binding * ('term * 'term list)) list  
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

83 
Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list; 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

84 

26336
a0e2b706ce73
renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents:
25739
diff
changeset

85 
type context = (string, string, Facts.ref) ctxt; 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

86 
type context_i = (typ, term, thm list) ctxt; 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

87 

21581  88 
fun facts_map f facts = Notes ("", facts) > f > (fn Notes (_, facts') => facts'); 
89 

29603  90 
fun map_ctxt {binding, typ, term, pattern, fact, attrib} = 
91 
fn Fixes fixes => Fixes (fixes > map (fn (x, T, mx) => (binding x, Option.map typ T, mx))) 

28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

92 
 Constrains xs => Constrains (xs > map (fn (x, T) => 
42494  93 
(Variable.check_name (binding (Binding.name x)), typ T))) 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

94 
 Assumes asms => Assumes (asms > map (fn ((a, atts), propps) => 
29603  95 
((binding a, map attrib atts), propps > map (fn (t, ps) => (term t, map pattern ps))))) 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

96 
 Defines defs => Defines (defs > map (fn ((a, atts), (t, ps)) => 
29603  97 
((binding a, map attrib atts), (term t, map pattern ps)))) 
21440  98 
 Notes (kind, facts) => Notes (kind, facts > map (fn ((a, atts), bs) => 
28965  99 
((binding a, map attrib atts), bs > map (fn (ths, btts) => (fact ths, map attrib btts))))); 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

100 

21528  101 
fun map_ctxt_attrib attrib = 
29603  102 
map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib}; 
21528  103 

45290  104 
fun transform_ctxt phi = map_ctxt 
28965  105 
{binding = Morphism.binding phi, 
21481  106 
typ = Morphism.typ phi, 
107 
term = Morphism.term phi, 

29603  108 
pattern = Morphism.term phi, 
21521  109 
fact = Morphism.fact phi, 
45290  110 
attrib = Args.transform_values phi}; 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

111 

19808  112 

18894  113 

19259  114 
(** pretty printing **) 
115 

19267  116 
fun pretty_items _ _ [] = [] 
117 
 pretty_items keyword sep (x :: ys) = 

118 
Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] :: 

119 
map (fn y => Pretty.block [Pretty.str " ", Pretty.keyword sep, Pretty.brk 1, y]) ys; 

19259  120 

28862  121 
fun pretty_name_atts ctxt (b, atts) sep = 
45584
41a768a431a6
do not store vacuous theorem specifications  relevant for frugal local theory content;
wenzelm
parents:
45390
diff
changeset

122 
if Attrib.is_empty_binding (b, atts) then [] 
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42495
diff
changeset

123 
else 
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42495
diff
changeset

124 
[Pretty.block (Pretty.breaks 
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42495
diff
changeset

125 
(Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]; 
19259  126 

127 

128 
(* pretty_stmt *) 

129 

130 
fun pretty_stmt ctxt = 

131 
let 

24920  132 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
133 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 

19267  134 
val prt_terms = separate (Pretty.keyword "and") o map prt_term; 
19259  135 
val prt_name_atts = pretty_name_atts ctxt; 
136 

137 
fun prt_show (a, ts) = 

19267  138 
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts))); 
19259  139 

28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

140 
fun prt_var (x, SOME T) = Pretty.block 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30219
diff
changeset

141 
[Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T] 
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30219
diff
changeset

142 
 prt_var (x, NONE) = Pretty.str (Binding.name_of x); 
26721  143 
val prt_vars = separate (Pretty.keyword "and") o map prt_var; 
19259  144 

19267  145 
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) 
19259  146 
 prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks 
19585  147 
(prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts)); 
19259  148 
in 
19267  149 
fn Shows shows => pretty_items "shows" "and" (map prt_show shows) 
150 
 Obtains obtains => pretty_items "obtains" "" (map prt_obtain obtains) 

19259  151 
end; 
152 

18894  153 

19259  154 
(* pretty_ctxt *) 
155 

156 
fun pretty_ctxt ctxt = 

157 
let 

24920  158 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
159 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31794
diff
changeset

160 
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; 
19259  161 
val prt_name_atts = pretty_name_atts ctxt; 
162 

19267  163 
fun prt_mixfix NoSyn = [] 
42287
d98eb048a2e4
discontinued special treatment of structure Mixfix;
wenzelm
parents:
41581
diff
changeset

164 
 prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx]; 
19267  165 

30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30219
diff
changeset

166 
fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") :: 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

167 
Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) 
30223
24d975352879
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents:
30219
diff
changeset

168 
 prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) :: 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

169 
Pretty.brk 1 :: prt_mixfix mx); 
28965  170 
fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); 
18894  171 

19259  172 
fun prt_asm (a, ts) = 
173 
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts)); 

174 
fun prt_def (a, (t, _)) = 

175 
Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t])); 

176 

177 
fun prt_fact (ths, []) = map prt_thm ths 

178 
 prt_fact (ths, atts) = Pretty.enclose "(" ")" 

21032  179 
(Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts; 
19259  180 
fun prt_note (a, ths) = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19466
diff
changeset

181 
Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths))); 
19259  182 
in 
19267  183 
fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) 
184 
 Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) 

185 
 Assumes asms => pretty_items "assumes" "and" (map prt_asm asms) 

186 
 Defines defs => pretty_items "defines" "and" (map prt_def defs) 

21440  187 
 Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts) 
188 
 Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts) 

19259  189 
end; 
18894  190 

19267  191 

192 
(* pretty_statement *) 

193 

194 
local 

195 

41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

196 
fun standard_elim th = 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

197 
(case Object_Logic.elim_concl th of 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

198 
SOME C => 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

199 
let 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

200 
val cert = Thm.cterm_of (Thm.theory_of_thm th); 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

201 
val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C); 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

202 
val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th; 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

203 
in (th', true) end 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

204 
 NONE => (th, false)); 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

205 

19267  206 
fun thm_name kind th prts = 
207 
let val head = 

27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26721
diff
changeset

208 
if Thm.has_name_hint th then 
21965
7120ef5bc378
pretty_statement: more careful handling of name_hint;
wenzelm
parents:
21646
diff
changeset

209 
Pretty.block [Pretty.command kind, 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

210 
Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")] 
21965
7120ef5bc378
pretty_statement: more careful handling of name_hint;
wenzelm
parents:
21646
diff
changeset

211 
else Pretty.command kind 
19267  212 
in Pretty.block (Pretty.fbreaks (head :: prts)) end; 
213 

214 
fun obtain prop ctxt = 

215 
let 

41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

216 
val ((ps, prop'), ctxt') = Variable.focus prop ctxt; 
42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42360
diff
changeset

217 
fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T); 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

218 
val xs = map (fix o #2) ps; 
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

219 
val As = Logic.strip_imp_prems prop'; 
41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

220 
in ((Binding.empty, (xs, As)), ctxt') end; 
19267  221 

222 
in 

223 

224 
fun pretty_statement ctxt kind raw_th = 

225 
let 

42360  226 
val thy = Proof_Context.theory_of ctxt; 
20150  227 

41581
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

228 
val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th); 
72a02e3dec7e
clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents:
41425
diff
changeset

229 
val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt); 
20150  230 
val prop = Thm.prop_of th'; 
231 
val (prems, concl) = Logic.strip_horn prop; 

35625  232 
val concl_term = Object_Logic.drop_judgment thy concl; 
19267  233 

20150  234 
val fixes = fold_aterms (fn v as Free (x, T) => 
235 
if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term) 

42488
4638622bcaa1
reorganized fixes as specialized (global) name space;
wenzelm
parents:
42360
diff
changeset

236 
then insert (op =) (Variable.revert_fixed ctxt' x, T) else I  _ => I) prop [] > rev; 
20150  237 
val (assumes, cases) = take_suffix (fn prem => 
238 
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems; 

19267  239 
in 
28965  240 
pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @ 
241 
pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @ 

242 
(if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])]) 

26716
8690e75e1395
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents:
26628
diff
changeset

243 
else 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42494
diff
changeset

244 
let val (clauses, ctxt'') = fold_map obtain cases ctxt' 
26716
8690e75e1395
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents:
26628
diff
changeset

245 
in pretty_stmt ctxt'' (Obtains clauses) end) 
19267  246 
end > thm_name kind raw_th; 
247 

18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

248 
end; 
19267  249 

19777  250 

251 

252 
(** logical operations **) 

253 

254 
(* witnesses  hypotheses as protected facts *) 

255 

256 
datatype witness = Witness of term * thm; 

257 

29578  258 
val mark_witness = Logic.protect; 
259 
fun witness_prop (Witness (t, _)) = t; 

44058  260 
fun witness_hyps (Witness (_, th)) = Thm.hyps_of th; 
19777  261 
fun map_witness f (Witness witn) = Witness (f witn); 
262 

45290  263 
fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); 
21481  264 

20058  265 
fun prove_witness ctxt t tac = 
29578  266 
Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ => 
25202
3a539d9995fb
proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
wenzelm
parents:
24920
diff
changeset

267 
Tactic.rtac Drule.protectI 1 THEN tac))); 
19777  268 

29603  269 

29578  270 
local 
271 

272 
val refine_witness = 

30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30438
diff
changeset

273 
Proof.refine (Method.Basic (K (RAW_METHOD 
29578  274 
(K (ALLGOALS 
275 
(CONJUNCTS (ALLGOALS 

32194  276 
(CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))))); 
25624  277 

29578  278 
fun gen_witness_proof proof after_qed wit_propss eq_props = 
279 
let 

280 
val propss = (map o map) (fn prop => (mark_witness prop, [])) wit_propss 

281 
@ [map (rpair []) eq_props]; 

282 
fun after_qed' thmss = 

29603  283 
let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss); 
29578  284 
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end; 
285 
in proof after_qed' propss #> refine_witness #> Seq.hd end; 

286 

38108  287 
fun proof_local cmd goal_ctxt int after_qed' propss = 
45329  288 
Proof.map_context (K goal_ctxt) #> 
289 
Proof.local_goal (Proof_Display.print_results int) (K I) Proof_Context.bind_propp_i 

290 
cmd NONE after_qed' (map (pair Thm.empty_binding) propss); 

41425  291 

29578  292 
in 
293 

294 
fun witness_proof after_qed wit_propss = 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35767
diff
changeset

295 
gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits) 
29578  296 
wit_propss []; 
297 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
35767
diff
changeset

298 
val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE); 
29578  299 

300 
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int = 

38108  301 
gen_witness_proof (proof_local cmd goal_ctxt int) 
29578  302 
(fn wits => fn _ => after_qed wits) wit_propss []; 
303 

38108  304 
fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int = 
305 
gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props; 

41425  306 

29603  307 
end; 
308 

19777  309 

25302  310 
fun compose_witness (Witness (_, th)) r = 
311 
let 

312 
val th' = Goal.conclude th; 

313 
val A = Thm.cprem_of r 1; 

25739  314 
in 
315 
Thm.implies_elim 

316 
(Conv.gconv_rule Drule.beta_eta_conversion 1 r) 

317 
(Conv.fconv_rule Drule.beta_eta_conversion 

318 
(Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th')) 

319 
end; 

25302  320 

29578  321 
fun conclude_witness (Witness (_, th)) = 
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
39557
diff
changeset

322 
Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th)); 
19777  323 

22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

324 
fun pretty_witness ctxt witn = 
24920  325 
let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

326 
Pretty.block (prt_term (witness_prop witn) :: 
39166
19efc2af3e6c
turned show_hyps and show_tags into proper configuration option;
wenzelm
parents:
38709
diff
changeset

327 
(if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]" 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

328 
(map prt_term (witness_hyps witn))] else [])) 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

329 
end; 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

330 

19777  331 

332 
(* derived rules *) 

333 

20007  334 
fun instantiate_tfrees thy subst th = 
19777  335 
let 
336 
val certT = Thm.ctyp_of thy; 

20007  337 
val idx = Thm.maxidx_of th + 1; 
338 
fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T); 

339 

340 
fun add_inst (a, S) insts = 

341 
if AList.defined (op =) insts a then insts 

342 
else (case AList.lookup (op =) subst a of NONE => insts  SOME T => (a, (S, T)) :: insts); 

343 
val insts = 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

344 
(Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v  _ => I) 
20007  345 
(Thm.full_prop_of th) []; 
19777  346 
in 
20007  347 
th 
348 
> Thm.generalize (map fst insts, []) idx 

349 
> Thm.instantiate (map cert_inst insts, []) 

19777  350 
end; 
351 

352 
fun instantiate_frees thy subst = 

353 
let val cert = Thm.cterm_of thy in 

354 
Drule.forall_intr_list (map (cert o Free o fst) subst) #> 

355 
Drule.forall_elim_list (map (cert o snd) subst) 

356 
end; 

357 

358 
fun hyps_rule rule th = 

21521  359 
let val {hyps, ...} = Thm.crep_thm th in 
19777  360 
Drule.implies_elim_list 
361 
(rule (Drule.implies_intr_list hyps th)) 

21521  362 
(map (Thm.assume o Drule.cterm_rule rule) hyps) 
19777  363 
end; 
364 

365 

366 
(* instantiate types *) 

367 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

368 
fun instT_type_same env = 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

369 
if Symtab.is_empty env then Same.same 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

370 
else 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

371 
Term_Subst.map_atypsT_same 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

372 
(fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T  NONE => raise Same.SAME) 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

373 
 _ => raise Same.SAME); 
19777  374 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

375 
fun instT_term_same env = 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

376 
if Symtab.is_empty env then Same.same 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

377 
else Term_Subst.map_types_same (instT_type_same env); 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

378 

439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

379 
val instT_type = Same.commit o instT_type_same; 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

380 
val instT_term = Same.commit o instT_term_same; 
19777  381 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

382 
fun instT_subst env th = 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

383 
(Thm.fold_terms o Term.fold_types o Term.fold_atyps) 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

384 
(fn T as TFree (a, _) => 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

385 
let val T' = the_default T (Symtab.lookup env a) 
45349
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

386 
in if T = T' then I else insert (eq_fst (op =)) (a, T') end 
45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

387 
 _ => I) th []; 
19777  388 

389 
fun instT_thm thy env th = 

390 
if Symtab.is_empty env then th 

391 
else 

392 
let val subst = instT_subst env th 

393 
in if null subst then th else th > hyps_rule (instantiate_tfrees thy subst) end; 

394 

22672
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

395 
fun instT_morphism thy env = 
24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23414
diff
changeset

396 
let val thy_ref = Theory.check_thy thy in 
22672
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

397 
Morphism.morphism 
45295  398 
{binding = [], 
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

399 
typ = [instT_type env], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

400 
term = [instT_term env], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

401 
fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]} 
22672
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

402 
end; 
19777  403 

404 

405 
(* instantiate types and terms *) 

406 

407 
fun inst_term (envT, env) = 

408 
if Symtab.is_empty env then instT_term envT 

409 
else 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

410 
instT_term envT #> 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

411 
Same.commit (Term_Subst.map_aterms_same 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

412 
(fn Free (x, _) => (case Symtab.lookup env x of SOME t => t  NONE => raise Same.SAME) 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

413 
 _ => raise Same.SAME)) #> 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

414 
Envir.beta_norm; 
19777  415 

45349
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

416 
fun inst_subst (envT, env) th = 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

417 
(Thm.fold_terms o Term.fold_aterms) 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

418 
(fn Free (x, T) => 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

419 
let 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

420 
val T' = instT_type envT T; 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

421 
val t = Free (x, T'); 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

422 
val t' = the_default t (Symtab.lookup env x); 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

423 
in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

424 
 _ => I) th []; 
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

425 

19777  426 
fun inst_thm thy (envT, env) th = 
427 
if Symtab.is_empty env then instT_thm thy envT th 

428 
else 

429 
let 

430 
val substT = instT_subst envT th; 

45349
7fb63b469cd2
more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents:
45346
diff
changeset

431 
val subst = inst_subst (envT, env) th; 
19777  432 
in 
433 
if null substT andalso null subst then th 

434 
else th > hyps_rule 

435 
(instantiate_tfrees thy substT #> 

436 
instantiate_frees thy subst #> 

22900  437 
Conv.fconv_rule (Thm.beta_conversion true)) 
19777  438 
end; 
439 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

440 
fun inst_morphism thy (envT, env) = 
24137
8d7896398147
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents:
23414
diff
changeset

441 
let val thy_ref = Theory.check_thy thy in 
22672
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

442 
Morphism.morphism 
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

443 
{binding = [], 
45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

444 
typ = [instT_type envT], 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

445 
term = [inst_term (envT, env)], 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

446 
fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]} 
22672
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

447 
end; 
19777  448 

449 

450 
(* satisfy hypotheses *) 

451 

45346
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

452 
fun satisfy_thm witns thm = 
439101d8eeec
some performance tuning via Term_Subst/Same.operation;
wenzelm
parents:
45345
diff
changeset

453 
thm > fold (fn hyp => 
19777  454 
(case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of 
455 
NONE => I 

25302  456 
 SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm)); 
19777  457 

29603  458 
val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; 
20264  459 

460 

29525  461 
(* rewriting with equalities *) 
462 

36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36323
diff
changeset

463 
fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism 
45289
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

464 
{binding = [], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

465 
typ = [], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

466 
term = [Raw_Simplifier.rewrite_term thy thms []], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

467 
fact = [map (Raw_Simplifier.rewrite_rule thms)]}); 
29525  468 

469 

29218  470 
(* transfer to theory using closure *) 
471 

472 
fun transfer_morphism thy = 

29603  473 
let val thy_ref = Theory.check_thy thy 
38709  474 
in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end; 
29603  475 

29218  476 

477 

30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

478 
(** activate in context **) 
28832  479 

30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

480 
(* init *) 
28832  481 

38108  482 
fun generic_note_thmss kind facts context = 
483 
let 

45390
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

484 
val facts' = 
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

485 
Attrib.map_facts (map (Attrib.attribute_i (Context.theory_of context))) facts; 
38108  486 
in 
487 
context > Context.mapping_result 

39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is globalonly;
wenzelm
parents:
39166
diff
changeset

488 
(Global_Theory.note_thmss kind facts') 
42360  489 
(Proof_Context.note_thmss kind facts') 
38108  490 
end; 
491 

42360  492 
fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2) 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

493 
 init (Constrains _) = I 
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

494 
 init (Assumes asms) = Context.map_proof (fn ctxt => 
28832  495 
let 
45390
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

496 
val asms' = 
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

497 
Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) asms; 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

498 
val (_, ctxt') = ctxt 
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

499 
> fold Variable.auto_fixes (maps (map #1 o #2) asms') 
42360  500 
> Proof_Context.add_assms_i Assumption.assume_export asms'; 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

501 
in ctxt' end) 
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

502 
 init (Defines defs) = Context.map_proof (fn ctxt => 
28832  503 
let 
45390
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

504 
val defs' = 
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45349
diff
changeset

505 
Attrib.map_specs (map (Attrib.attribute_i (Proof_Context.theory_of ctxt))) defs; 
28832  506 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
35624  507 
let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) 
30434  508 
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end); 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

509 
val (_, ctxt') = ctxt 
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

510 
> fold Variable.auto_fixes (map #1 asms) 
42360  511 
> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms); 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

512 
in ctxt' end) 
38108  513 
 init (Notes (kind, facts)) = generic_note_thmss kind facts #> #2; 
30775
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

514 

71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

515 

71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

516 
(* activate *) 
71f777103225
added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents:
30763
diff
changeset

517 

30777
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

518 
fun activate_i elem ctxt = 
28832  519 
let 
30777
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

520 
val elem' = map_ctxt_attrib Args.assignable elem; 
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

521 
val ctxt' = Context.proof_map (init elem') ctxt; 
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

522 
in (map_ctxt_attrib Args.closure elem', ctxt') end; 
28832  523 

30777
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

524 
fun activate raw_elem ctxt = 
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

525 
let val elem = raw_elem > map_ctxt 
43842
f035d867fb41
Element.activate: leave check of binding where actually applied to the context  allow internal qualifications, or nonidentifier fact names like "assumes *: A" (see also 1183951365de);
wenzelm
parents:
43837
diff
changeset

526 
{binding = I, 
29603  527 
typ = I, 
528 
term = I, 

529 
pattern = I, 

42360  530 
fact = Proof_Context.get_fact ctxt, 
531 
attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)} 

30777
9960ff945c52
simplified Element.activate(_i): singleton version;
wenzelm
parents:
30775
diff
changeset

532 
in activate_i elem ctxt end; 
28832  533 

19267  534 
end; 