# HG changeset patch # User Norbert Schirmer # Date 1229595408 -3600 # Node ID 95d3a82857e5926c13b4f33af5e2f7753f03ea6a # Parent eddc08920f4a24517e7fd0ae892336f17bab59e0 adapted statespace module to new locales; diff -r eddc08920f4a -r 95d3a82857e5 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Tue Dec 16 21:11:39 2008 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Thu Dec 18 11:16:48 2008 +0100 @@ -30,6 +30,10 @@ n::nat b::bool +print_locale vars_namespace +print_locale vars_valuetypes +print_locale vars + text {* \noindent This resembles a \isacommand{record} definition, but introduces sophisticated locale infrastructure instead of HOL type schemes. The resulting context @@ -196,18 +200,25 @@ by simp +text {* Hmm, I hoped this would work now...*} + +locale fooX = foo + + assumes "s\b = k" + +(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *) text {* There are known problems with syntax-declarations. They currently only work, when the context is already built. Hopefully this will be implemented correctly in future Isabelle versions. *} +(* lemma assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4" shows True proof - class_interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact + interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact term "s\a = i" qed - +*) (* lemma includes foo diff -r eddc08920f4a -r 95d3a82857e5 src/HOL/Statespace/StateSpaceLocale.thy --- a/src/HOL/Statespace/StateSpaceLocale.thy Tue Dec 16 21:11:39 2008 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Thu Dec 18 11:16:48 2008 +0100 @@ -16,7 +16,7 @@ concrete values.*} -class_locale project_inject = +locale project_inject = fixes project :: "'value \ 'a" and "inject":: "'a \ 'value" assumes project_inject_cancel [statefun_simp]: "project (inject x) = x" diff -r eddc08920f4a -r 95d3a82857e5 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Dec 16 21:11:39 2008 +0100 +++ b/src/HOL/Statespace/state_space.ML Thu Dec 18 11:16:48 2008 +0100 @@ -17,7 +17,7 @@ val namespace_definition : bstring -> typ -> - Locale.expr -> + Expression.expression -> string list -> string list -> theory -> theory val define_statespace : @@ -61,7 +61,7 @@ val update_tr' : Proof.context -> term list -> term end; -structure StateSpace: STATE_SPACE = +structure StateSpace : STATE_SPACE = struct (* Theorems *) @@ -148,11 +148,25 @@ fun prove_interpretation_in ctxt_tac (name, expr) thy = thy - |> Locale.interpretation_in_locale I (name, expr) + |> Expression.sublocale_cmd name expr |> Proof.global_terminal_proof (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE) |> ProofContext.theory_of +fun add_locale name expr elems thy = + thy + |> Expression.add_locale name name expr elems + |> (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes) + |> LocalTheory.exit; + +fun add_locale_cmd name expr elems thy = + thy + |> Expression.add_locale_cmd name name expr elems + |> (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> + fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes) + |> LocalTheory.exit; + type statespace_info = {args: (string * sort) list, (* type arguments *) parents: (typ list * string * string option list) list, @@ -252,7 +266,7 @@ in EVERY [rtac rule i] st end - fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [], + fun tac ctxt = EVERY [NewLocale.intro_locales_tac true ctxt [], ALLGOALS (SUBGOAL (solve_tac ctxt))] in thy @@ -264,16 +278,11 @@ fun namespace_definition name nameT parent_expr parent_comps new_comps thy = let val all_comps = parent_comps @ new_comps; - val vars = Locale.Merge - (map (fn n => Locale.Rename (Locale.Locale (Locale.intern thy "var") - ,[SOME (n,NONE)])) all_comps); - + val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps); val full_name = Sign.full_bname thy name; val dist_thm_name = distinct_compsN; - val dist_thm_full_name = - let val prefix = fold1' (fn name => fn prfx => prfx ^ "_" ^ name) all_comps ""; - in if prefix = "" then dist_thm_name else prefix ^ "." ^ dist_thm_name end; + val dist_thm_full_name = dist_thm_name; fun comps_of_thm thm = prop_of thm |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free); @@ -309,12 +318,10 @@ DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT (sort fast_string_ord all_comps)), ([]))])]; - in thy - |> Locale.add_locale "" name vars [assumes] - ||> ProofContext.theory_of - ||> interprete_parent name dist_thm_full_name parent_expr - |> #2 + |> add_locale name ([],vars) [assumes] + |> ProofContext.theory_of + |> interprete_parent name dist_thm_full_name parent_expr end; fun encode_dot x = if x= #"." then #"_" else x; @@ -378,11 +385,10 @@ val components' = map (fn (n,T) => (n,(T,full_name))) components; val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps; - fun parent_expr (_,n,rs) = Locale.Rename - (Locale.Locale (suffix namespaceN n), - map (Option.map (fn s => (s,NONE))) rs); - val parents_expr = Locale.Merge (fold (fn p => fn es => parent_expr p::es) parents []); + fun parent_expr (_,n,rs) = (suffix namespaceN n,((n,false),Expression.Positional rs)); + (* FIXME: a more specific renaming-prefix (including parameter names) may be nicer *) + val parents_expr = map parent_expr parents; fun distinct_types Ts = let val tab = fold (fn T => fn tab => Typtab.update (T,()) tab) Ts Typtab.empty; in map fst (Typtab.dest tab) end; @@ -396,30 +402,32 @@ val stateT = nameT --> valueT; fun projectT T = valueT --> T; fun injectT T = T --> valueT; - - val locs = map (fn T => Locale.Rename (Locale.Locale project_injectL, - [SOME (project_name T,NONE), - SOME (inject_name T ,NONE)])) Ts; + val locinsts = map (fn T => (project_injectL, + (("",false),Expression.Positional + [SOME (Free (project_name T,projectT T)), + SOME (Free ((inject_name T,injectT T)))]))) Ts; + val locs = flat (map (fn T => [(Binding.name (project_name T),NONE,NoSyn), + (Binding.name (inject_name T),NONE,NoSyn)]) Ts); val constrains = List.concat (map (fn T => [(project_name T,projectT T),(inject_name T,injectT T)]) Ts); - fun interprete_parent_valuetypes (Ts, pname, _) = + fun interprete_parent_valuetypes (Ts, pname, _) thy = let val {args,types,...} = the (Symtab.lookup (StateSpaceData.get (Context.Theory thy)) pname); val inst = map fst args ~~ Ts; val subst = Term.map_type_tfree (the o AList.lookup (op =) inst o fst); val pars = List.concat (map ((fn T => [project_name T,inject_name T]) o subst) types); - val expr = Locale.Rename (Locale.Locale (suffix valuetypesN name), - map (fn n => SOME (n,NONE)) pars); - in prove_interpretation_in (K all_tac) - (suffix valuetypesN name, expr) end; + + val expr = ([(suffix valuetypesN name, + (("",false),Expression.Positional (map SOME pars)))],[]); + in prove_interpretation_in (K all_tac) (suffix valuetypesN name, expr) thy end; fun interprete_parent (_, pname, rs) = let - val expr = Locale.Rename (Locale.Locale pname, map (Option.map (fn n => (n,NONE))) rs) + val expr = ([(pname, (("",false), Expression.Positional rs))],[]) in prove_interpretation_in - (fn ctxt => Locale.intro_locales_tac false ctxt []) + (fn ctxt => NewLocale.intro_locales_tac false ctxt []) (full_name, expr) end; fun declare_declinfo updates lthy phi ctxt = @@ -454,17 +462,16 @@ in thy |> namespace_definition - (suffix namespaceN name) nameT parents_expr + (suffix namespaceN name) nameT (parents_expr,[]) (map fst parent_comps) (map fst components) |> Context.theory_map (add_statespace full_name args parents components []) - |> Locale.add_locale "" (suffix valuetypesN name) (Locale.Merge locs) - [Element.Constrains constrains] - |> ProofContext.theory_of o #2 + |> add_locale (suffix valuetypesN name) (locinsts,locs) [] + |> ProofContext.theory_of |> fold interprete_parent_valuetypes parents - |> Locale.add_locale_cmd name - (Locale.Merge [Locale.Locale (suffix namespaceN full_name) - ,Locale.Locale (suffix valuetypesN full_name)]) fixestate - |> ProofContext.theory_of o #2 + |> add_locale_cmd name + ([(suffix namespaceN full_name ,(("",false),Expression.Named [])), + (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate + |> ProofContext.theory_of |> fold interprete_parent parents |> add_declaration (SOME full_name) (declare_declinfo components') end; @@ -572,7 +579,6 @@ | xs => ["Components already defined in parents: " ^ commas xs]); val errs = err_dup_args @ err_dup_components @ err_extra_frees @ err_dup_types @ err_comp_in_parent; - in if null errs then thy |> statespace_definition state_space args' name parents' parent_comps comps' else error (cat_lines errs) diff -r eddc08920f4a -r 95d3a82857e5 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Dec 16 21:11:39 2008 +0100 +++ b/src/Pure/Isar/expression.ML Thu Dec 18 11:16:48 2008 +0100 @@ -522,7 +522,8 @@ val export = Variable.export_morphism goal_ctxt context; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; - val exp_term = Drule.term_rule thy (singleton exp_fact); + val thy_ref = Theory.check_thy thy; (* FIXME!!*) + val exp_term = (fn t => Drule.term_rule (Theory.deref thy_ref) (singleton exp_fact) t); val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism {binding = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};