author  ballarin 
Wed, 19 Nov 2008 17:00:00 +0100  
changeset 28850  6882e110c29a 
parent 28832  cf7237498e7a 
child 28862  53f13f763d4f 
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 
ID: $Id$ 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

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

4 

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

18140
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 

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

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

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

12 
Shows of (Attrib.binding * ('term * 'term list) list) list  
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

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

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

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

16 
datatype ('typ, 'term, 'fact) ctxt = 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

17 
Fixes of (Name.binding * 'typ option * mixfix) list  
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

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

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

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

21 
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

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

23 
type context_i = (typ, term, thm list) ctxt 
21581  24 
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

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

26 
(Attrib.binding * ('c * Attrib.src list) list) list 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

27 
val map_ctxt: {name: Name.binding > Name.binding, 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

28 
var: Name.binding * mixfix > Name.binding * mixfix, 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

29 
typ: 'typ > 'a, term: 'term > 'b, fact: 'fact > 'c, 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

30 
attrib: Attrib.src > Attrib.src} > ('typ, 'term, 'fact) ctxt > ('a, 'b, 'c) ctxt 
21528  31 
val map_ctxt_attrib: (Attrib.src > Attrib.src) > 
32 
('typ, 'term, 'fact) ctxt > ('typ, 'term, 'fact) ctxt 

21481  33 
val morph_ctxt: morphism > context_i > context_i 
19808  34 
val params_of: context_i > (string * typ) list 
35 
val prems_of: context_i > term list 

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

36 
val facts_of: theory > context_i > (Attrib.binding * (thm list * Attrib.src list) list) list 
19777  37 
val pretty_stmt: Proof.context > statement_i > Pretty.T list 
38 
val pretty_ctxt: Proof.context > context_i > Pretty.T list 

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

40 
type witness 

41 
val map_witness: (term * thm > term * thm) > witness > witness 

21481  42 
val morph_witness: morphism > witness > witness 
19777  43 
val witness_prop: witness > term 
44 
val witness_hyps: witness > term list 

45 
val assume_witness: theory > term > witness 

20058  46 
val prove_witness: Proof.context > term > tactic > witness 
25624  47 
val close_witness: witness > witness 
19777  48 
val conclude_witness: witness > thm 
49 
val mark_witness: term > term 

50 
val make_witness: term > thm > witness 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19897
diff
changeset

51 
val dest_witness: witness > term * thm 
20068
19c7361db4a3
New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents:
20058
diff
changeset

52 
val transfer_witness: theory > witness > witness 
19808  53 
val refine_witness: Proof.state > Proof.state Seq.seq 
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

54 
val pretty_witness: Proof.context > witness > Pretty.T 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

55 
val rename: (string * (string * mixfix option)) list > string > string 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

56 
val rename_var_name: (string * (string * mixfix option)) list > 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

57 
string * mixfix > string * mixfix 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

58 
val rename_var: (string * (string * mixfix option)) list > 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

59 
Name.binding * mixfix > Name.binding * mixfix 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

60 
val rename_term: (string * (string * mixfix option)) list > term > term 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

61 
val rename_thm: (string * (string * mixfix option)) list > thm > thm 
21481  62 
val rename_morphism: (string * (string * mixfix option)) list > morphism 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

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

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

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

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

68 
val inst_thm: theory > typ Symtab.table * term Symtab.table > thm > thm 
21481  69 
val inst_morphism: theory > typ Symtab.table * term Symtab.table > morphism 
19777  70 
val satisfy_thm: witness list > thm > thm 
21481  71 
val satisfy_morphism: witness list > morphism 
20264  72 
val satisfy_facts: witness list > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

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

74 
(Attrib.binding * (thm list * Attrib.src list) list) list 
21581  75 
val generalize_facts: Proof.context > Proof.context > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

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

77 
(Attrib.binding * (thm list * Attrib.src list) list) list 
28850  78 
val activate: (typ, term, Facts.ref) ctxt list > Proof.context > 
28832  79 
(context_i list * (Name.binding * Thm.thm list) list) * Proof.context 
80 
val activate_i: context_i list > Proof.context > 

81 
(context_i list * (Name.binding * Thm.thm list) list) * Proof.context 

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

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

83 

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

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

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

86 

19777  87 
(** language elements **) 
88 

89 
(* statement *) 

19259  90 

91 
datatype ('typ, 'term) stmt = 

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

92 
Shows of (Attrib.binding * ('term * 'term list) list) list  
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

93 
Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list; 
19259  94 

95 
type statement = (string, string) stmt; 

96 
type statement_i = (typ, term) stmt; 

97 

98 

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

100 

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

101 
datatype ('typ, 'term, 'fact) ctxt = 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

102 
Fixes of (Name.binding * 'typ option * mixfix) list  
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

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

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

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

106 
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

107 

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

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

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

110 

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

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

113 
fun map_ctxt {name, var, typ, term, fact, attrib} = 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

114 
fn Fixes fixes => Fixes (fixes > map (fn (x, T, mx) => 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

115 
let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end)) 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

116 
 Constrains xs => Constrains (xs > map (fn (x, T) => 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

117 
let val x' = Name.name_of (#1 (var (Name.binding x, NoSyn))) in (x', typ T) end)) 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

118 
 Assumes asms => Assumes (asms > map (fn ((a, atts), propps) => 
19585  119 
((name a, map attrib atts), propps > map (fn (t, ps) => (term t, map term ps))))) 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

120 
 Defines defs => Defines (defs > map (fn ((a, atts), (t, ps)) => 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

121 
((name a, map attrib atts), (term t, map term ps)))) 
21440  122 
 Notes (kind, facts) => Notes (kind, facts > map (fn ((a, atts), bs) => 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

123 
((name a, map attrib atts), bs > map (fn (ths, btts) => (fact ths, map attrib btts))))); 
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

124 

21528  125 
fun map_ctxt_attrib attrib = 
126 
map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib}; 

127 

21481  128 
fun morph_ctxt phi = map_ctxt 
129 
{name = Morphism.name phi, 

130 
var = Morphism.var phi, 

131 
typ = Morphism.typ phi, 

132 
term = Morphism.term phi, 

21521  133 
fact = Morphism.fact phi, 
21481  134 
attrib = Args.morph_values phi}; 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

135 

19808  136 

137 
(* logical content *) 

138 

19777  139 
fun params_of (Fixes fixes) = fixes > map 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

140 
(fn (x, SOME T, _) => (Name.name_of x, T) 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

141 
 (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.name_of x), [])) 
19777  142 
 params_of _ = []; 
18140
691c64d615a5
Explicit data structures for some Isar language elements.
wenzelm
parents:
diff
changeset

143 

19777  144 
fun prems_of (Assumes asms) = maps (map fst o snd) asms 
145 
 prems_of (Defines defs) = map (fst o snd) defs 

146 
 prems_of _ = []; 

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

147 

20233  148 
fun assume thy t = Assumption.assume (Thm.cterm_of thy t); 
19808  149 

150 
fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms 

151 
 facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs 

21440  152 
 facts_of _ (Notes (_, facts)) = facts 
19808  153 
 facts_of _ _ = []; 
154 

18894  155 

156 

19259  157 
(** pretty printing **) 
158 

19267  159 
fun pretty_items _ _ [] = [] 
160 
 pretty_items keyword sep (x :: ys) = 

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

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

19259  163 

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

164 
fun pretty_name_atts ctxt (binding, atts) sep = 
28733  165 
let 
28737  166 
val name = Name.output binding; 
28733  167 
in if name = "" andalso null atts then [] 
28079
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

168 
else [Pretty.block 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

169 
(Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))] 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

170 
end; 
19259  171 

172 

173 
(* pretty_stmt *) 

174 

175 
fun pretty_stmt ctxt = 

176 
let 

24920  177 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
178 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 

19267  179 
val prt_terms = separate (Pretty.keyword "and") o map prt_term; 
19259  180 
val prt_name_atts = pretty_name_atts ctxt; 
181 

182 
fun prt_show (a, ts) = 

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

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

185 
fun prt_var (x, SOME T) = Pretty.block 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

186 
[Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T] 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

187 
 prt_var (x, NONE) = Pretty.str (Name.name_of x); 
26721  188 
val prt_vars = separate (Pretty.keyword "and") o map prt_var; 
19259  189 

19267  190 
fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts)) 
19259  191 
 prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks 
19585  192 
(prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts)); 
19259  193 
in 
19267  194 
fn Shows shows => pretty_items "shows" "and" (map prt_show shows) 
195 
 Obtains obtains => pretty_items "obtains" "" (map prt_obtain obtains) 

19259  196 
end; 
197 

18894  198 

19259  199 
(* pretty_ctxt *) 
200 

201 
fun pretty_ctxt ctxt = 

202 
let 

24920  203 
val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt; 
204 
val prt_term = Pretty.quote o Syntax.pretty_term ctxt; 

19259  205 
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt; 
206 
val prt_name_atts = pretty_name_atts ctxt; 

207 

19267  208 
fun prt_mixfix NoSyn = [] 
209 
 prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx]; 

210 

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

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

212 
Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx) 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

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

214 
Pretty.brk 1 :: prt_mixfix mx); 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

215 
fun prt_constrain (x, T) = prt_fix (Name.binding x, SOME T, NoSyn); 
18894  216 

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

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

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

221 

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

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

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

226 
Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths))); 
19259  227 
in 
19267  228 
fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes) 
229 
 Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs) 

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

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

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

19259  234 
end; 
18894  235 

19267  236 

237 
(* pretty_statement *) 

238 

239 
local 

240 

241 
fun thm_name kind th prts = 

242 
let val head = 

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

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

244 
Pretty.block [Pretty.command kind, 
27865
27a8ad9612a3
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents:
26721
diff
changeset

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

246 
else Pretty.command kind 
19267  247 
in Pretty.block (Pretty.fbreaks (head :: prts)) end; 
248 

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

249 
fun fix (x, T) = (Name.binding x, SOME T); 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

250 

19267  251 
fun obtain prop ctxt = 
252 
let 

20150  253 
val ((xs, prop'), ctxt') = Variable.focus prop ctxt; 
254 
val As = Logic.strip_imp_prems (Thm.term_of prop'); 

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

255 
in ((Name.no_binding, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end; 
19267  256 

257 
in 

258 

259 
fun pretty_statement ctxt kind raw_th = 

260 
let 

261 
val thy = ProofContext.theory_of ctxt; 

20150  262 
val cert = Thm.cterm_of thy; 
263 

21605  264 
val th = MetaSimplifier.norm_hhf raw_th; 
20150  265 
val is_elim = ObjectLogic.is_elim th; 
19267  266 

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

267 
val ((_, [th']), ctxt') = Variable.import_thms true [th] (Variable.set_body false ctxt); 
20150  268 
val prop = Thm.prop_of th'; 
269 
val (prems, concl) = Logic.strip_horn prop; 

270 
val concl_term = ObjectLogic.drop_judgment thy concl; 

19267  271 

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

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

274 
then insert (op =) (x, T) else I  _ => I) prop [] > rev; 
20150  275 
val (assumes, cases) = take_suffix (fn prem => 
276 
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems; 

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

278 
pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @ 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

279 
pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @ 
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28079
diff
changeset

280 
(if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])]) 
26716
8690e75e1395
print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents:
26628
diff
changeset

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

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

283 
in pretty_stmt ctxt'' (Obtains clauses) end) 
19267  284 
end > thm_name kind raw_th; 
285 

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

286 
end; 
19267  287 

19777  288 

289 

290 
(** logical operations **) 

291 

292 
(* witnesses  hypotheses as protected facts *) 

293 

294 
datatype witness = Witness of term * thm; 

295 

296 
fun map_witness f (Witness witn) = Witness (f witn); 

297 

21481  298 
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th)); 
299 

19777  300 
fun witness_prop (Witness (t, _)) = t; 
301 
fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th); 

302 

303 
fun assume_witness thy t = 

304 
Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t))); 

305 

20058  306 
fun prove_witness ctxt t tac = 
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26336
diff
changeset

307 
Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ => 
25202
3a539d9995fb
proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
wenzelm
parents:
24920
diff
changeset

308 
Tactic.rtac Drule.protectI 1 THEN tac))); 
19777  309 

26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26336
diff
changeset

310 
val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th)); 
25624  311 

25202
3a539d9995fb
proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
wenzelm
parents:
24920
diff
changeset

312 
fun conclude_witness (Witness (_, th)) = 
26628
63306cb94313
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents:
26336
diff
changeset

313 
Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th)); 
19777  314 

25302  315 
fun compose_witness (Witness (_, th)) r = 
316 
let 

317 
val th' = Goal.conclude th; 

318 
val A = Thm.cprem_of r 1; 

25739  319 
in 
320 
Thm.implies_elim 

321 
(Conv.gconv_rule Drule.beta_eta_conversion 1 r) 

322 
(Conv.fconv_rule Drule.beta_eta_conversion 

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

324 
end; 

25302  325 

19777  326 
val mark_witness = Logic.protect; 
327 

328 
fun make_witness t th = Witness (t, th); 

19931
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19897
diff
changeset

329 
fun dest_witness (Witness w) = w; 
fb32b43e7f80
Restructured locales with predicates: import is now an interpretation.
ballarin
parents:
19897
diff
changeset

330 

20068
19c7361db4a3
New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents:
20058
diff
changeset

331 
fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th); 
19c7361db4a3
New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents:
20058
diff
changeset

332 

19777  333 
val refine_witness = 
334 
Proof.refine (Method.Basic (K (Method.RAW_METHOD 

335 
(K (ALLGOALS 

23414
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23351
diff
changeset

336 
(CONJUNCTS (ALLGOALS 
927203ad4b3a
tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents:
23351
diff
changeset

337 
(CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none)); 
19777  338 

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

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

341 
Pretty.block (prt_term (witness_prop witn) :: 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

342 
(if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]" 
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22568
diff
changeset

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

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

345 

19777  346 

347 
(* derived rules *) 

348 

20007  349 
fun instantiate_tfrees thy subst th = 
19777  350 
let 
351 
val certT = Thm.ctyp_of thy; 

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

354 

355 
fun add_inst (a, S) insts = 

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

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

358 
val insts = 

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

360 
(Thm.full_prop_of th) []; 

19777  361 
in 
20007  362 
th 
363 
> Thm.generalize (map fst insts, []) idx 

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

19777  365 
end; 
366 

367 
fun instantiate_frees thy subst = 

368 
let val cert = Thm.cterm_of thy in 

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

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

371 
end; 

372 

373 
fun hyps_rule rule th = 

21521  374 
let val {hyps, ...} = Thm.crep_thm th in 
19777  375 
Drule.implies_elim_list 
376 
(rule (Drule.implies_intr_list hyps th)) 

21521  377 
(map (Thm.assume o Drule.cterm_rule rule) hyps) 
19777  378 
end; 
379 

380 

381 
(* rename *) 

382 

383 
fun rename ren x = 

384 
(case AList.lookup (op =) ren (x: string) of 

385 
NONE => x 

386 
 SOME (x', _) => x'); 

387 

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

388 
fun rename_var_name ren (x, mx) = 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

389 
(case (AList.lookup (op =) ren x, mx) of 
19777  390 
(NONE, _) => (x, mx) 
391 
 (SOME (x', NONE), Structure) => (x', mx) 

392 
 (SOME (x', SOME _), Structure) => 

393 
error ("Attempt to change syntax of structure parameter " ^ quote x) 

394 
 (SOME (x', NONE), _) => (x', NoSyn) 

395 
 (SOME (x', SOME mx'), _) => (x', mx')); 

396 

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

397 
fun rename_var ren (binding, mx) = 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

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

399 
val x = Name.name_of binding; 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

400 
val (x', mx') = rename_var_name ren (x, mx); 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

401 
in (Name.binding x', mx') end; 
955c42c8a5e4
explicit type Name.binding for higherspecification elements;
wenzelm
parents:
27865
diff
changeset

402 

19777  403 
fun rename_term ren (Free (x, T)) = Free (rename ren x, T) 
404 
 rename_term ren (t $ u) = rename_term ren t $ rename_term ren u 

405 
 rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t) 

406 
 rename_term _ a = a; 

407 

408 
fun rename_thm ren th = 

409 
let 

20304  410 
val thy = Thm.theory_of_thm th; 
22691  411 
val subst = (Thm.fold_terms o Term.fold_aterms) 
20304  412 
(fn Free (x, T) => 
19777  413 
let val x' = rename ren x 
20304  414 
in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end 
415 
 _ => I) th []; 

19777  416 
in 
417 
if null subst then th 

20304  418 
else th > hyps_rule (instantiate_frees thy subst) 
19777  419 
end; 
420 

21481  421 
fun rename_morphism ren = Morphism.morphism 
21521  422 
{name = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)}; 
19777  423 

424 

425 
(* instantiate types *) 

426 

427 
fun instT_type env = 

428 
if Symtab.is_empty env then I 

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

430 

431 
fun instT_term env = 

432 
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

433 
else Term.map_types (instT_type env); 
19777  434 

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

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

439 
 _ => I) th []; 

19777  440 

441 
fun instT_thm thy env th = 

442 
if Symtab.is_empty env then th 

443 
else 

444 
let val subst = instT_subst env th 

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

446 

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

447 
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

448 
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

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

450 
{name = I, var = I, 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

451 
typ = instT_type env, 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

452 
term = instT_term env, 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

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

454 
end; 
19777  455 

456 

457 
(* instantiate types and terms *) 

458 

459 
fun inst_term (envT, env) = 

460 
if Symtab.is_empty env then instT_term envT 

461 
else 

462 
let 

463 
val instT = instT_type envT; 

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

465 
 inst (Free (x, T)) = 

466 
(case Symtab.lookup env x of 

467 
NONE => Free (x, instT T) 

468 
 SOME t => t) 

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

470 
 inst (b as Bound _) = b 

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

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

473 
in Envir.beta_norm o inst end; 

474 

475 
fun inst_thm thy (envT, env) th = 

476 
if Symtab.is_empty env then instT_thm thy envT th 

477 
else 

478 
let 

479 
val substT = instT_subst envT th; 

22691  480 
val subst = (Thm.fold_terms o Term.fold_aterms) 
20304  481 
(fn Free (x, T) => 
19777  482 
let 
483 
val T' = instT_type envT T; 

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

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

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

19777  488 
in 
489 
if null substT andalso null subst then th 

490 
else th > hyps_rule 

491 
(instantiate_tfrees thy substT #> 

492 
instantiate_frees thy subst #> 

22900  493 
Conv.fconv_rule (Thm.beta_conversion true)) 
19777  494 
end; 
495 

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

496 
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

497 
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

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

499 
{name = I, var = I, 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

500 
typ = instT_type (#1 envs), 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

501 
term = inst_term envs, 
777af26d5713
inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents:
22658
diff
changeset

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

503 
end; 
19777  504 

505 

506 
(* satisfy hypotheses *) 

507 

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

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

510 
NONE => I 

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

21497  513 
fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns); 
19843  514 

21581  515 
fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns)); 
20264  516 

517 

518 
(* generalize type/term parameters *) 

519 

520 
val maxidx_atts = fold Args.maxidx_values; 

521 

21581  522 
fun generalize_facts inner outer facts = 
20264  523 
let 
524 
val thy = ProofContext.theory_of inner; 

525 
val maxidx = 

526 
fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1; 

21581  527 
val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer; 
21521  528 
val exp_term = Drule.term_rule thy (singleton exp_fact); 
529 
val exp_typ = Logic.type_map exp_term; 

530 
val morphism = 

531 
Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact}; 

21581  532 
in facts_map (morph_ctxt morphism) facts end; 
20886
f26672c248ee
replaced generalize_facts by full export_(standard_)facts;
wenzelm
parents:
20548
diff
changeset

533 

28832  534 

535 
(** activate in context, return elements and facts **) 

536 

537 
local 

538 

539 
fun axioms_export axs _ As = 

540 
(satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); 

541 

542 
fun activate_elem (Fixes fixes) ctxt = 

543 
([], ctxt > ProofContext.add_fixes_i fixes > snd) 

544 
 activate_elem (Constrains _) ctxt = 

545 
([], ctxt) 

546 
 activate_elem (Assumes asms) ctxt = 

547 
let 

548 
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; 

549 
val ts = maps (map #1 o #2) asms'; 

550 
val (_, ctxt') = 

551 
ctxt > fold Variable.auto_fixes ts 

552 
> ProofContext.add_assms_i (axioms_export []) asms'; 

553 
in ([], ctxt') end 

554 
 activate_elem (Defines defs) ctxt = 

555 
let 

556 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 

557 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 

558 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

559 
in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end); 

560 
val (_, ctxt') = 

561 
ctxt > fold (Variable.auto_fixes o #1) asms 

562 
> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); 

563 
in ([], ctxt') end 

564 
 activate_elem (Notes (kind, facts)) ctxt = 

565 
let 

566 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 

567 
val (res, ctxt') = ctxt > ProofContext.note_thmss_i kind facts'; 

568 
in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end; 

569 

570 
fun gen_activate prep_facts raw_elems ctxt = 

571 
let 

572 
val elems = map (map_ctxt_attrib Args.assignable o prep_facts ctxt) raw_elems; 

573 
val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt); 

574 
val elems' = elems > map (map_ctxt_attrib Args.closure); 

575 
in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end; 

576 

577 
fun check_name name = 

578 
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) 

579 
else name; 

580 

581 
fun prep_facts prep_name get intern ctxt elem = elem > map_ctxt 

582 
{var = I, typ = I, term = I, 

583 
name = Name.map_name prep_name, 

584 
fact = get ctxt, 

585 
attrib = intern (ProofContext.theory_of ctxt)}; 

586 

587 
in 

588 

589 
fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x; 

590 
fun activate_i x = gen_activate (K I) x; 

591 

19267  592 
end; 
28832  593 

594 
end; 