summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | ballarin |

Thu, 11 Dec 2003 14:10:27 +0100 | |

changeset 14291 | 61df18481f53 |

parent 14290 | 84fda1b39947 |

child 14292 | 5b57cc196b12 |

Change to prune_prems in Pure/Isar/locale.ML.

src/HOL/Real/HahnBanach/HahnBanach.thy | file | annotate | diff | comparison | revisions | |

src/Pure/Isar/locale.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Dec 11 10:52:41 2003 +0100 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Dec 11 14:10:27 2003 +0100 @@ -340,7 +340,7 @@ have F: "vectorspace F" .. have linearform: "linearform F f" . have F_norm: "normed_vectorspace F norm" - by (rule subspace_normed_vs [OF _ _ _ norm.intro]) + by (rule subspace_normed_vs [OF _ _ norm.intro]) have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule normed_vectorspace.fn_norm_ge_zero [OF F_norm _ continuous.intro, folded B_def fn_norm_def])

--- a/src/Pure/Isar/locale.ML Thu Dec 11 10:52:41 2003 +0100 +++ b/src/Pure/Isar/locale.ML Thu Dec 11 14:10:27 2003 +0100 @@ -89,7 +89,15 @@ type 'att element_i = (typ, term, thm list, 'att) elem_expr; type locale = - {view: cterm list * thm list, (*external view on assumptions*) + {view: cterm list * thm list, + (* If locale <loc> contains assumptions these are encoded in the + predicate <loc>. If these assumptions are accumulated + fragments via import, the context generated when entering the + locale will contain a list of assumptions corresponding to the + assumptions of all locale fragments. + The first part of view (called statement) represents these assumptions, + the second part (called axioms) contains projections from <loc> to the + assumption fragments. *) import: expr, (*dynamic import*) elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) params: (string * typ option) list * string list}; (*all/local params*) @@ -203,17 +211,26 @@ in -(* Prune premises: remove internal delta predicates. +(** Prune premises: + Remove internal delta predicates (generated by "includes") from the + premises of a theorem. Assumes no outer quanfifiers and no flex-flex pairs. May change names of TVars. - Performs compress and close_derivation on result, if modified. *) + Performs compress and close_derivation on result, if modified. **) + +(* Note: reconstruction of the correct premises fails for subspace_normed_vs + in HOL/Real/HahnBanach/NormedSpace.thy. This cannot be fixed since in the + current setup there is no way of distinguishing whether the theorem + statement involved "includes subspace F E + normed_vectorspace E" or + "includes subspace F E + vectorspace E + norm E norm". +*) fun prune_prems thy thm = let val sign = Theory.sign_of thy; fun analyse cprem = (* Returns None if head of premise is not a predicate defined by a locale, - returns also None if locale has import but predicate is not *_axioms + returns also None if locale has a view but predicate is not *_axioms since this is a premise that wasn't generated by includes. *) case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of (Const (raw_name, T), args) => let @@ -221,8 +238,8 @@ handle LIST _ => raw_name in case get_locale thy name of None => None - | Some {import, ...} => - if name = raw_name andalso import <> empty + | Some {view = (_, axioms), ...} => + if name = raw_name andalso not (null axioms) then None else Some (((name, args), T), name = raw_name) end @@ -246,7 +263,7 @@ | (trie, Some id) => insert_ident subs id trie) (Trie [], ids); (* Assemble new theorem; new prems will be hyps. - Axioms is an intermeditate list of locale axioms required to + Axioms is an intermediate list of locale axioms required to replace old premises by new ones. *) fun scan ((roots, thm, cprems', axioms), (cprem, id)) = case id of