author  wenzelm 
Thu, 03 Nov 2011 23:32:31 +0100  
changeset 45329  dd8208a3655a 
parent 45295  255200892a42 
child 45345  2cb00d068e3b 
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 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

49 
val instT_type: typ Symtab.table > typ > typ 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

50 
val instT_term: typ Symtab.table > term > term 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

51 
val instT_thm: theory > typ Symtab.table > thm > thm 
21481  52 
val instT_morphism: theory > typ Symtab.table > morphism 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

53 
val inst_term: typ Symtab.table * term Symtab.table > term > term 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

54 
val inst_thm: theory > typ Symtab.table * term Symtab.table > thm > thm 
21481  55 
val inst_morphism: theory > typ Symtab.table * term Symtab.table > morphism 
19777  56 
val satisfy_thm: witness list > thm > thm 
21481  57 
val satisfy_morphism: witness list > morphism 
20264  58 
val satisfy_facts: witness list > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

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

60 
(Attrib.binding * (thm list * Attrib.src list) list) list 
36674
d95f39448121
eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents:
36323
diff
changeset

61 
val eq_morphism: theory > thm list > morphism option 
29218  62 
val transfer_morphism: theory > morphism 
38108  63 
val generic_note_thmss: string > (Attrib.binding * (thm list * Attrib.src list) list) list > 
64 
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

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

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

67 
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

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

69 

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

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

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

72 

19777  73 
(** language elements **) 
74 

75 
(* statement *) 

19259  76 

77 
datatype ('typ, 'term) stmt = 

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

78 
Shows of (Attrib.binding * ('term * 'term list) list) list  
29578  79 
Obtains of (binding * ((binding * 'typ option) list * 'term list)) list; 
19259  80 

81 
type statement = (string, string) stmt; 

82 
type statement_i = (typ, term) stmt; 

83 

84 

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

86 

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

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

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

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

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

92 
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

93 

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

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

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

96 

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

29603  99 
fun map_ctxt {binding, typ, term, pattern, fact, attrib} = 
100 
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

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

103 
 Assumes asms => Assumes (asms > map (fn ((a, atts), propps) => 
29603  104 
((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

105 
 Defines defs => Defines (defs > map (fn ((a, atts), (t, ps)) => 
29603  106 
((binding a, map attrib atts), (term t, map pattern ps)))) 
21440  107 
 Notes (kind, facts) => Notes (kind, facts > map (fn ((a, atts), bs) => 
28965  108 
((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

109 

21528  110 
fun map_ctxt_attrib attrib = 
29603  111 
map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib}; 
21528  112 

45290  113 
fun transform_ctxt phi = map_ctxt 
28965  114 
{binding = Morphism.binding phi, 
21481  115 
typ = Morphism.typ phi, 
116 
term = Morphism.term phi, 

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

120 

19808  121 

18894  122 

19259  123 
(** pretty printing **) 
124 

19267  125 
fun pretty_items _ _ [] = [] 
126 
 pretty_items keyword sep (x :: ys) = 

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

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

19259  129 

28862  130 
fun pretty_name_atts ctxt (b, atts) sep = 
30219  131 
if Binding.is_empty b andalso null atts then [] 
43547
f3a8476285c6
clarified Binding.pretty/print: no quotes, only markup  Binding.str_of is rendered obsolete;
wenzelm
parents:
42495
diff
changeset

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

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

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

136 

137 
(* pretty_stmt *) 

138 

139 
fun pretty_stmt ctxt = 

140 
let 

24920  141 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
142 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 

19267  143 
val prt_terms = separate (Pretty.keyword "and") o map prt_term; 
19259  144 
val prt_name_atts = pretty_name_atts ctxt; 
145 

146 
fun prt_show (a, ts) = 

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

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

149 
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

150 
[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

151 
 prt_var (x, NONE) = Pretty.str (Binding.name_of x); 
26721  152 
val prt_vars = separate (Pretty.keyword "and") o map prt_var; 
19259  153 

19267  154 
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) 
19259  155 
 prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks 
19585  156 
(prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts)); 
19259  157 
in 
19267  158 
fn Shows shows => pretty_items "shows" "and" (map prt_show shows) 
159 
 Obtains obtains => pretty_items "obtains" "" (map prt_obtain obtains) 

19259  160 
end; 
161 

18894  162 

19259  163 
(* pretty_ctxt *) 
164 

165 
fun pretty_ctxt ctxt = 

166 
let 

24920  167 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
168 
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

169 
val prt_thm = Pretty.backquote o Display.pretty_thm ctxt; 
19259  170 
val prt_name_atts = pretty_name_atts ctxt; 
171 

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

173 
 prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx]; 
19267  174 

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

175 
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

176 
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

177 
 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

178 
Pretty.brk 1 :: prt_mixfix mx); 
28965  179 
fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn); 
18894  180 

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

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

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

185 

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

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

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

190 
Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths))); 
19259  191 
in 
19267  192 
fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) 
193 
 Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) 

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

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

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

19259  198 
end; 
18894  199 

19267  200 

201 
(* pretty_statement *) 

202 

203 
local 

204 

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

205 
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

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

207 
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

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

209 
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

210 
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

211 
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

212 
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

213 
 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

214 

19267  215 
fun thm_name kind th prts = 
216 
let val head = 

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

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

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

219 
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

220 
else Pretty.command kind 
19267  221 
in Pretty.block (Pretty.fbreaks (head :: prts)) end; 
222 

223 
fun obtain prop ctxt = 

224 
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

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

226 
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

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

228 
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

229 
in ((Binding.empty, (xs, As)), ctxt') end; 
19267  230 

231 
in 

232 

233 
fun pretty_statement ctxt kind raw_th = 

234 
let 

42360  235 
val thy = Proof_Context.theory_of ctxt; 
20150  236 

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

237 
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

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

35625  241 
val concl_term = Object_Logic.drop_judgment thy concl; 
19267  242 

20150  243 
val fixes = fold_aterms (fn v as Free (x, T) => 
244 
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

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

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

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

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

253 
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

254 
in pretty_stmt ctxt'' (Obtains clauses) end) 
19267  255 
end > thm_name kind raw_th; 
256 

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

257 
end; 
19267  258 

19777  259 

260 

261 
(** logical operations **) 

262 

263 
(* witnesses  hypotheses as protected facts *) 

264 

265 
datatype witness = Witness of term * thm; 

266 

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

44058  269 
fun witness_hyps (Witness (_, th)) = Thm.hyps_of th; 
19777  270 
fun map_witness f (Witness witn) = Witness (f witn); 
271 

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

20058  274 
fun prove_witness ctxt t tac = 
29578  275 
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

276 
Tactic.rtac Drule.protectI 1 THEN tac))); 
19777  277 

29603  278 

29578  279 
local 
280 

281 
val refine_witness = 

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

282 
Proof.refine (Method.Basic (K (RAW_METHOD 
29578  283 
(K (ALLGOALS 
284 
(CONJUNCTS (ALLGOALS 

32194  285 
(CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))))); 
25624  286 

29578  287 
fun gen_witness_proof proof after_qed wit_propss eq_props = 
288 
let 

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

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

291 
fun after_qed' thmss = 

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

295 

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

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

41425  300 

29578  301 
in 
302 

303 
fun witness_proof after_qed wit_propss = 

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

304 
gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits) 
29578  305 
wit_propss []; 
306 

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

307 
val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE); 
29578  308 

309 
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int = 

38108  310 
gen_witness_proof (proof_local cmd goal_ctxt int) 
29578  311 
(fn wits => fn _ => after_qed wits) wit_propss []; 
312 

38108  313 
fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int = 
314 
gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props; 

41425  315 

29603  316 
end; 
317 

19777  318 

25302  319 
fun compose_witness (Witness (_, th)) r = 
320 
let 

321 
val th' = Goal.conclude th; 

322 
val A = Thm.cprem_of r 1; 

25739  323 
in 
324 
Thm.implies_elim 

325 
(Conv.gconv_rule Drule.beta_eta_conversion 1 r) 

326 
(Conv.fconv_rule Drule.beta_eta_conversion 

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

328 
end; 

25302  329 

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

331 
Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th)); 
19777  332 

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

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

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

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

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

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

339 

19777  340 

341 
(* derived rules *) 

342 

20007  343 
fun instantiate_tfrees thy subst th = 
19777  344 
let 
345 
val certT = Thm.ctyp_of thy; 

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

348 

349 
fun add_inst (a, S) insts = 

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

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

352 
val insts = 

353 
Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v  _ => I)) 

354 
(Thm.full_prop_of th) []; 

19777  355 
in 
20007  356 
th 
357 
> Thm.generalize (map fst insts, []) idx 

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

19777  359 
end; 
360 

361 
fun instantiate_frees thy subst = 

362 
let val cert = Thm.cterm_of thy in 

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

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

365 
end; 

366 

367 
fun hyps_rule rule th = 

21521  368 
let val {hyps, ...} = Thm.crep_thm th in 
19777  369 
Drule.implies_elim_list 
370 
(rule (Drule.implies_intr_list hyps th)) 

21521  371 
(map (Thm.assume o Drule.cterm_rule rule) hyps) 
19777  372 
end; 
373 

374 

375 
(* instantiate types *) 

376 

377 
fun instT_type env = 

378 
if Symtab.is_empty env then I 

379 
else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x)); 

380 

381 
fun instT_term env = 

382 
if Symtab.is_empty env then I 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20304
diff
changeset

383 
else Term.map_types (instT_type env); 
19777  384 

22691  385 
fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps) 
20304  386 
(fn T as TFree (a, _) => 
387 
let val T' = the_default T (Symtab.lookup env a) 

388 
in if T = T' then I else insert (op =) (a, T') end 

389 
 _ => I) th []; 

19777  390 

391 
fun instT_thm thy env th = 

392 
if Symtab.is_empty env then th 

393 
else 

394 
let val subst = instT_subst env th 

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

396 

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

397 
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

398 
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

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

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

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

403 
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

404 
end; 
19777  405 

406 

407 
(* instantiate types and terms *) 

408 

409 
fun inst_term (envT, env) = 

410 
if Symtab.is_empty env then instT_term envT 

411 
else 

412 
let 

413 
val instT = instT_type envT; 

414 
fun inst (Const (x, T)) = Const (x, instT T) 

415 
 inst (Free (x, T)) = 

416 
(case Symtab.lookup env x of 

417 
NONE => Free (x, instT T) 

418 
 SOME t => t) 

419 
 inst (Var (xi, T)) = Var (xi, instT T) 

420 
 inst (b as Bound _) = b 

421 
 inst (Abs (x, T, t)) = Abs (x, instT T, inst t) 

422 
 inst (t $ u) = inst t $ inst u; 

423 
in Envir.beta_norm o inst end; 

424 

425 
fun inst_thm thy (envT, env) th = 

426 
if Symtab.is_empty env then instT_thm thy envT th 

427 
else 

428 
let 

429 
val substT = instT_subst envT th; 

22691  430 
val subst = (Thm.fold_terms o Term.fold_aterms) 
20304  431 
(fn Free (x, T) => 
19777  432 
let 
433 
val T' = instT_type envT T; 

434 
val t = Free (x, T'); 

435 
val t' = the_default t (Symtab.lookup env x); 

20304  436 
in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end 
437 
 _ => I) th []; 

19777  438 
in 
439 
if null substT andalso null subst then th 

440 
else th > hyps_rule 

441 
(instantiate_tfrees thy substT #> 

442 
instantiate_frees thy subst #> 

22900  443 
Conv.fconv_rule (Thm.beta_conversion true)) 
19777  444 
end; 
445 

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

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

447 
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

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

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

450 
typ = [instT_type (#1 envs)], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

451 
term = [inst_term envs], 
25e9e7f527b4
slightly more explicit/syntactic modelling of morphisms;
wenzelm
parents:
44058
diff
changeset

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

453 
end; 
19777  454 

455 

456 
(* satisfy hypotheses *) 

457 

458 
fun satisfy_thm witns thm = thm > fold (fn hyp => 

459 
(case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of 

460 
NONE => I 

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

29603  463 
val satisfy_morphism = Morphism.thm_morphism o satisfy_thm; 
45290  464 
val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism; 
20264  465 

466 

29525  467 
(* rewriting with equalities *) 
468 

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

469 
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

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

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

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

473 
fact = [map (Raw_Simplifier.rewrite_rule thms)]}); 
29525  474 

475 

29218  476 
(* transfer to theory using closure *) 
477 

478 
fun transfer_morphism thy = 

29603  479 
let val thy_ref = Theory.check_thy thy 
38709  480 
in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end; 
29603  481 

29218  482 

483 

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

484 
(** activate in context **) 
28832  485 

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

486 
(* init *) 
28832  487 

38108  488 
fun generic_note_thmss kind facts context = 
489 
let 

490 
val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts; 

491 
in 

492 
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

493 
(Global_Theory.note_thmss kind facts') 
42360  494 
(Proof_Context.note_thmss kind facts') 
38108  495 
end; 
496 

42360  497 
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

498 
 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

499 
 init (Assumes asms) = Context.map_proof (fn ctxt => 
28832  500 
let 
42360  501 
val asms' = Attrib.map_specs (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

502 
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

503 
> fold Variable.auto_fixes (maps (map #1 o #2) asms') 
42360  504 
> 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

505 
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

506 
 init (Defines defs) = Context.map_proof (fn ctxt => 
28832  507 
let 
42360  508 
val defs' = Attrib.map_specs (Attrib.attribute_i (Proof_Context.theory_of ctxt)) defs; 
28832  509 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 
35624  510 
let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *) 
30434  511 
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

512 
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

513 
> fold Variable.auto_fixes (map #1 asms) 
42360  514 
> 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

515 
in ctxt' end) 
38108  516 
 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

517 

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

518 

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

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

520 

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

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

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

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

525 
in (map_ctxt_attrib Args.closure elem', ctxt') end; 
28832  526 

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

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

528 
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

529 
{binding = I, 
29603  530 
typ = I, 
531 
term = I, 

532 
pattern = I, 

42360  533 
fact = Proof_Context.get_fact ctxt, 
534 
attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)} 

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

535 
in activate_i elem ctxt end; 
28832  536 

19267  537 
end; 