# HG changeset patch # User wenzelm # Date 1333468096 -7200 # Node ID 610d9c212376216d33df1355799155bf11bbe400 # Parent 9d02327ede5617319dbfd1b273461ade9f8294f7# Parent c82a0b2606a128980fb8fcea43bcd4c4dabc0d22 merged diff -r 9d02327ede56 -r 610d9c212376 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Apr 03 16:45:44 2012 +0100 +++ b/src/HOL/IsaMakefile Tue Apr 03 17:48:16 2012 +0200 @@ -1041,7 +1041,8 @@ $(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ - Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ + Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \ + Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \ Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ Isar_Examples/Mutilated_Checkerboard.thy \ Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ diff -r 9d02327ede56 -r 610d9c212376 src/HOL/Isar_Examples/Group_Context.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,94 @@ +(* Title: HOL/Isar_Examples/Group_Context.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- theory context version *} + +theory Group_Context +imports Main +begin + +text {* hypothetical group axiomatization *} + +context + fixes prod :: "'a \ 'a \ 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assumes assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\x. one ** x = x" + and left_inverse: "\x. inverse x ** x = one" +begin + +text {* some consequences *} + +lemma right_inverse: "x ** inverse x = one" +proof - + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\ = one ** x ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\ = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . +qed + +lemma right_one: "x ** one = x" +proof - + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\ = x ** inverse x ** x" + by (simp only: assoc) + also have "\ = one ** x" + by (simp only: right_inverse) + also have "\ = x" + by (simp only: left_one) + finally show "x ** one = x" . +qed + +lemma one_equality: "e ** x = x \ one = e" +proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\ = (e ** x) ** inverse x" + by (simp only: eq) + also have "\ = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = e ** one" + by (simp only: right_inverse) + also have "\ = e" + by (simp only: right_one) + finally show "one = e" . +qed + +lemma inverse_equality: "x' ** x = one \ inverse x = x'" +proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\ = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\ = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = x' ** one" + by (simp only: right_inverse) + also have "\ = x'" + by (simp only: right_one) + finally show "inverse x = x'" . +qed + +end + +end diff -r 9d02327ede56 -r 610d9c212376 src/HOL/Isar_Examples/Group_Notepad.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Tue Apr 03 17:48:16 2012 +0200 @@ -0,0 +1,96 @@ +(* Title: HOL/Isar_Examples/Group_Notepad.thy + Author: Makarius +*) + +header {* Some algebraic identities derived from group axioms -- proof notepad version *} + +theory Group_Notepad +imports Main +begin + +notepad +begin + txt {* hypothetical group axiomatization *} + + fix prod :: "'a \ 'a \ 'a" (infixl "**" 70) + and one :: "'a" + and inverse :: "'a => 'a" + assume assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" + and left_one: "\x. one ** x = x" + and left_inverse: "\x. inverse x ** x = one" + + txt {* some consequences *} + + have right_inverse: "\x. x ** inverse x = one" + proof - + fix x + have "x ** inverse x = one ** (x ** inverse x)" + by (simp only: left_one) + also have "\ = one ** x ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x ** x ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (inverse x ** x) ** inverse x" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** one ** inverse x" + by (simp only: left_inverse) + also have "\ = inverse (inverse x) ** (one ** inverse x)" + by (simp only: assoc) + also have "\ = inverse (inverse x) ** inverse x" + by (simp only: left_one) + also have "\ = one" + by (simp only: left_inverse) + finally show "x ** inverse x = one" . + qed + + have right_one: "\x. x ** one = x" + proof - + fix x + have "x ** one = x ** (inverse x ** x)" + by (simp only: left_inverse) + also have "\ = x ** inverse x ** x" + by (simp only: assoc) + also have "\ = one ** x" + by (simp only: right_inverse) + also have "\ = x" + by (simp only: left_one) + finally show "x ** one = x" . + qed + + have one_equality: "\e x. e ** x = x \ one = e" + proof - + fix e x + assume eq: "e ** x = x" + have "one = x ** inverse x" + by (simp only: right_inverse) + also have "\ = (e ** x) ** inverse x" + by (simp only: eq) + also have "\ = e ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = e ** one" + by (simp only: right_inverse) + also have "\ = e" + by (simp only: right_one) + finally show "one = e" . + qed + + have inverse_equality: "\x x'. x' ** x = one \ inverse x = x'" + proof - + fix x x' + assume eq: "x' ** x = one" + have "inverse x = one ** inverse x" + by (simp only: left_one) + also have "\ = (x' ** x) ** inverse x" + by (simp only: eq) + also have "\ = x' ** (x ** inverse x)" + by (simp only: assoc) + also have "\ = x' ** one" + by (simp only: right_inverse) + also have "\ = x'" + by (simp only: right_one) + finally show "inverse x = x'" . + qed + +end + +end diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/class.ML Tue Apr 03 17:48:16 2012 +0200 @@ -486,13 +486,12 @@ ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.map_contexts (K synchronize_inst_syntax); -fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case instantiation_param lthy b of SOME c => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) else lthy |> define_overloaded (c, U) (Binding.name_of b) (b_def, rhs) - | NONE => lthy |> - Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)); + | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let @@ -553,10 +552,8 @@ |> Local_Theory.init naming {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_notes, - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => - Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.standard_declaration, + abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, + declaration = K Generic_Target.theory_declaration, pretty = pretty, exit = Local_Theory.target_of o conclude} end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/expression.ML Tue Apr 03 17:48:16 2012 +0200 @@ -43,12 +43,9 @@ (Attrib.binding * term) list -> theory -> Proof.state val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression -> (Attrib.binding * string) list -> theory -> Proof.state - val interpretation: expression_i -> (Attrib.binding * term) list -> - theory -> Proof.state - val interpretation_cmd: expression -> (Attrib.binding * string) list -> - theory -> Proof.state - val interpret: expression_i -> (Attrib.binding * term) list -> - bool -> Proof.state -> Proof.state + val interpretation: expression_i -> (Attrib.binding * term) list -> theory -> Proof.state + val interpretation_cmd: expression -> (Attrib.binding * string) list -> theory -> Proof.state + val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 17:48:16 2012 +0200 @@ -24,15 +24,23 @@ term list -> local_theory -> local_theory) -> string * bool -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val background_declaration: declaration -> local_theory -> local_theory - val standard_declaration: declaration -> local_theory -> local_theory val locale_declaration: string -> bool -> declaration -> local_theory -> local_theory + val standard_declaration: (int -> bool) -> declaration -> local_theory -> local_theory + val generic_const: bool -> Syntax.mode -> (binding * mixfix) * term -> + Context.generic -> Context.generic + val const_declaration: (int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> + local_theory -> local_theory + val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> + term list * term list -> local_theory -> (term * thm) * local_theory val theory_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory - val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory + val theory_abbrev: Syntax.mode -> (binding * mixfix) -> term * term -> term list -> + local_theory -> local_theory + val theory_declaration: declaration -> local_theory -> local_theory end structure Generic_Target: GENERIC_TARGET = @@ -52,6 +60,11 @@ else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))); NoSyn); +fun check_mixfix_global (b, no_params) mx = + if no_params orelse mx = NoSyn then mx + else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ + Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); + (* define *) @@ -61,21 +74,17 @@ val thy_ctxt = Proof_Context.init_global thy; (*term and type parameters*) - val crhs = Thm.cterm_of thy rhs; - val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of; + val ((defs, _), rhs') = Thm.cterm_of thy rhs + |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; - val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' []; + val xs = Variable.add_fixed lthy rhs' []; val T = Term.fastype_of rhs; val tfreesT = Term.add_tfreesT T (fold (Term.add_tfreesT o #2) xs []); val extra_tfrees = rev (subtract (op =) tfreesT (Term.add_tfrees rhs [])); val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; - val target_ctxt = Local_Theory.target_of lthy; - val term_params = - filter (Variable.is_fixed target_ctxt o #1) xs - |> sort (Variable.fixed_ord target_ctxt o pairself #1) - |> map Free; + val term_params = map Free (sort (Variable.fixed_ord lthy o pairself #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; @@ -184,18 +193,15 @@ fun abbrev target_abbrev prmode ((b, mx), t) lthy = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); - val target_ctxt = Local_Theory.target_of lthy; - val t' = Assumption.export_term lthy target_ctxt t; - val xs = map Free (rev (Variable.add_fixed target_ctxt t' [])); + val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t; + val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' [])); val u = fold_rev lambda xs t'; + val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; val extra_tfrees = subtract (op =) (Term.add_tfreesT (Term.fastype_of u) []) (Term.add_tfrees u []); val mx' = check_mixfix lthy (b, extra_tfrees) mx; - - val global_rhs = - singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; in lthy |> target_abbrev prmode (b, mx') (global_rhs, t') xs @@ -213,31 +219,83 @@ (Proof_Context.init_global (Proof_Context.theory_of lthy)) decl; in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; -fun standard_declaration decl = - background_declaration decl #> - (fn lthy => Local_Theory.map_contexts (fn _ => fn ctxt => - Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt) lthy); - fun locale_declaration locale syntax decl lthy = lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); +fun standard_declaration pred decl lthy = + Local_Theory.map_contexts (fn level => fn ctxt => + if pred level then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt + else ctxt) lthy; + + +(* const declaration *) + +fun generic_const same_shape prmode ((b, mx), t) context = + let + val const_alias = + if same_shape then + (case t of + Const (c, T) => + let + val thy = Context.theory_of context; + val ctxt = Context.proof_of context; + in + (case Type_Infer_Context.const_type ctxt c of + SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE + | NONE => NONE) + end + | _ => NONE) + else NONE; + in + (case const_alias of + SOME c => + context + |> Context.mapping (Sign.const_alias b c) (Proof_Context.const_alias b c) + |> Morphism.form (Proof_Context.generic_notation true prmode [(t, mx)]) + | NONE => + context + |> Proof_Context.generic_add_abbrev Print_Mode.internal (b, Term.close_schematic_term t) + |-> (fn (const as Const (c, _), _) => same_shape ? + (Proof_Context.generic_revert_abbrev (#1 prmode) c #> + Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) + end; + +fun const_declaration pred prmode ((b, mx), rhs) = + standard_declaration pred (fn phi => + let + val b' = Morphism.binding phi b; + val rhs' = Morphism.term phi rhs; + val same_shape = Term.aconv_untyped (rhs, rhs'); + in generic_const same_shape prmode ((b', mx), rhs') end); + (** primitive theory operations **) -fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let + val params = type_params @ term_params; + val mx' = check_mixfix_global (b, null params) mx; + val (const, lthy2) = lthy - |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx)); - val lhs = list_comb (const, type_params @ term_params); + |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); + val lhs = Term.list_comb (const, params); + val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def lthy2 false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); in ((lhs, def), lthy3) end; +fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = + background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) + #-> (fn (lhs, def) => fn lthy' => lthy' |> + const_declaration (fn level => level <> Local_Theory.level lthy') + Syntax.mode_default ((b, mx), lhs) + |> pair (lhs, def)); + fun theory_notes kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> (fn lthy => lthy |> Local_Theory.map_contexts (fn level => fn ctxt => @@ -246,9 +304,16 @@ ctxt |> Attrib.local_notes kind (Element.transform_facts (Local_Theory.standard_morphism lthy ctxt) local_facts) |> snd)); -fun theory_abbrev prmode ((b, mx), t) = - Local_Theory.background_theory +fun theory_abbrev prmode (b, mx) (t, _) xs = + Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, t) #-> - (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); + (fn (lhs, _) => (* FIXME type_params!? *) + Sign.notation true prmode [(lhs, check_mixfix_global (b, null xs) mx)] #> pair lhs)) + #-> (fn lhs => fn lthy' => lthy' |> + const_declaration (fn level => level <> Local_Theory.level lthy') prmode + ((b, if null xs then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, xs))); + +fun theory_declaration decl = + background_declaration decl #> standard_declaration (K true) decl; end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/local_defs.ML Tue Apr 03 17:48:16 2012 +0200 @@ -135,22 +135,22 @@ let val exp = Assumption.export false inner outer; val exp_term = Assumption.export_term inner outer; - val prems = Assumption.local_prems_of inner outer; + val asms = Assumption.local_assms_of inner outer; in fn th => let val th' = exp th; - val defs_asms = prems |> map (fn prem => - (case try (head_of_def o Thm.prop_of) prem of - NONE => (prem, false) + val defs_asms = asms |> map (Thm.assume #> (fn asm => + (case try (head_of_def o Thm.prop_of) asm of + NONE => (asm, false) | SOME x => let val t = Free x in (case try exp_term t of - NONE => (prem, false) + NONE => (asm, false) | SOME u => - if t aconv u then (prem, false) - else (Drule.abs_def prem, true)) - end)); + if t aconv u then (asm, false) + else (Drule.abs_def (Drule.gen_all asm), true)) + end))); in (pairself (map #1) (List.partition #2 defs_asms), th') end end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/local_theory.ML Tue Apr 03 17:48:16 2012 +0200 @@ -11,6 +11,7 @@ sig type operations val assert: local_theory -> local_theory + val restore: local_theory -> local_theory val level: Proof.context -> int val assert_bottom: bool -> local_theory -> local_theory val open_target: Name_Space.naming -> operations -> local_theory -> local_theory @@ -54,7 +55,6 @@ val type_alias: binding -> string -> local_theory -> local_theory val const_alias: binding -> string -> local_theory -> local_theory val init: Name_Space.naming -> operations -> Proof.context -> local_theory - val restore: local_theory -> local_theory val exit: local_theory -> Proof.context val exit_global: local_theory -> theory val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context @@ -107,6 +107,8 @@ Data.map (fn {naming, operations, target} :: parents => make_lthy (f (naming, operations, target)) :: parents); +fun restore lthy = #target (get_first_lthy lthy) |> Data.put (Data.get lthy); + (* nested structure *) @@ -126,7 +128,7 @@ |> Data.map (cons (make_lthy (naming, operations, target))); fun close_target lthy = - assert_bottom false lthy |> Data.map tl; + assert_bottom false lthy |> Data.map tl |> restore; fun map_contexts f lthy = let val n = level lthy in @@ -281,10 +283,6 @@ | _ => error "Local theory already initialized") |> checkpoint; -fun restore lthy = - let val {naming, operations, target} = get_first_lthy lthy - in init naming operations target end; - (* exit *) diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/named_target.ML Tue Apr 03 17:48:16 2012 +0200 @@ -46,12 +46,11 @@ (* consts in locale *) -fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) = +fun locale_const (Target {target, is_class, ...}) prmode ((b, mx), rhs) = Generic_Target.locale_declaration target true (fn phi => let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; - val arg = (b', Term.close_schematic_term rhs'); val same_shape = Term.aconv_untyped (rhs, rhs'); (* FIXME workaround based on educated guess *) @@ -62,31 +61,24 @@ andalso List.last prefix' = (Class.class_prefix target, false) orelse same_shape); in - not is_canonical_class ? - (Context.mapping_result - (Sign.add_abbrev Print_Mode.internal arg) - (Proof_Context.add_abbrev Print_Mode.internal arg) - #-> (fn (lhs' as Const (d, _), _) => - same_shape ? - (Context.mapping - (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #> - Morphism.form (Proof_Context.generic_notation true prmode [(lhs', mx)])))) - end); + not is_canonical_class ? Generic_Target.generic_const same_shape prmode ((b', mx), rhs') + end) #> + (fn lthy => lthy |> Generic_Target.const_declaration + (fn level => level <> 0 andalso level <> Local_Theory.level lthy) prmode ((b, mx), rhs)); (* define *) -fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) = - Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) +fun locale_foundation ta (((b, U), mx), (b_def, rhs)) params = + Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs) - #> pair (lhs, def)) + #> pair (lhs, def)); -fun class_foundation (ta as Target {target, ...}) - (((b, U), mx), (b_def, rhs)) (type_params, term_params) = - Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params) +fun class_foundation (ta as Target {target, ...}) (((b, U), mx), (b_def, rhs)) params = + Generic_Target.background_foundation (((b, U), NoSyn), (b_def, rhs)) params #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs) - #> Class.const target ((b, mx), (type_params, lhs)) - #> pair (lhs, def)) + #> Class.const target ((b, mx), (#1 params, lhs)) + #> pair (lhs, def)); fun target_foundation (ta as Target {is_locale, is_class, ...}) = if is_class then class_foundation ta @@ -106,31 +98,26 @@ fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, t)) #-> - (fn (lhs, _) => locale_const ta prmode - ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); + (fn (lhs, _) => + locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs))); -fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) - prmode (b, mx) (global_rhs, t') xs lthy = +fun target_abbrev (ta as Target {target, is_locale, is_class, ...}) prmode (b, mx) (t, t') xs lthy = if is_locale then lthy - |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), global_rhs) xs + |> locale_abbrev ta prmode ((b, if is_class then NoSyn else mx), t) xs |> is_class ? Class.abbrev target prmode ((b, mx), t') - else - lthy - |> Generic_Target.theory_abbrev prmode ((b, mx), global_rhs); + else lthy |> Generic_Target.theory_abbrev prmode (b, mx) (t, t') xs; (* declaration *) fun target_declaration (Target {target, ...}) {syntax, pervasive} decl lthy = - if target = "" then Generic_Target.standard_declaration decl lthy + if target = "" then Generic_Target.theory_declaration decl lthy else lthy |> pervasive ? Generic_Target.background_declaration decl |> Generic_Target.locale_declaration target syntax decl - |> (fn lthy' => lthy' |> Local_Theory.map_contexts (fn level => fn ctxt => - if level = 0 then ctxt - else Context.proof_map (Local_Theory.standard_form lthy' ctxt decl) ctxt)); + |> (fn lthy' => lthy' |> Generic_Target.standard_declaration (fn level => level <> 0) decl); (* pretty *) @@ -192,7 +179,7 @@ Local_Theory.assert_bottom true #> Data.get #> the #> (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target); -fun context_cmd ("-", _) thy = init I "" thy +fun context_cmd ("-", _) thy = theory_init thy | context_cmd target thy = init I (Locale.check thy target) thy; end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/overloading.ML Tue Apr 03 17:48:16 2012 +0200 @@ -158,14 +158,13 @@ ##> Local_Theory.map_contexts (K synchronize_syntax) #-> (fn (_, def) => pair (Const (c, U), def)); -fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = +fun foundation (((b, U), mx), (b_def, rhs)) params lthy = (case operation lthy b of SOME (c, (v, checked)) => if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) - | NONE => lthy - |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params)); + | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params); fun pretty lthy = let @@ -204,10 +203,8 @@ |> Local_Theory.init naming {define = Generic_Target.define foundation, notes = Generic_Target.notes Generic_Target.theory_notes, - abbrev = Generic_Target.abbrev - (fn prmode => fn (b, mx) => fn (t, _) => fn _ => - Generic_Target.theory_abbrev prmode ((b, mx), t)), - declaration = K Generic_Target.standard_declaration, + abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev, + declaration = K Generic_Target.theory_declaration, pretty = pretty, exit = Local_Theory.target_of o conclude} end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/proof_context.ML Tue Apr 03 17:48:16 2012 +0200 @@ -146,6 +146,9 @@ val add_const_constraint: string * typ option -> Proof.context -> Proof.context val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context val revert_abbrev: string -> string -> Proof.context -> Proof.context + val generic_add_abbrev: string -> binding * term -> Context.generic -> + (term * term) * Context.generic + val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic val print_syntax: Proof.context -> unit val print_abbrevs: Proof.context -> unit val print_binds: Proof.context -> unit @@ -1021,6 +1024,12 @@ fun revert_abbrev mode c = (map_consts o apfst) (Consts.revert_abbrev mode c); +fun generic_add_abbrev mode arg = + Context.mapping_result (Sign.add_abbrev mode arg) (add_abbrev mode arg); + +fun generic_revert_abbrev mode arg = + Context.mapping (Sign.revert_abbrev mode arg) (revert_abbrev mode arg); + (* fixes *) diff -r 9d02327ede56 -r 610d9c212376 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Apr 03 17:48:16 2012 +0200 @@ -109,13 +109,12 @@ val loc_init = Named_Target.context_cmd; val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; -fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy - | loc_begin NONE (Context.Proof lthy) = lthy - | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; - -fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit - | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore - | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; +fun loc_begin loc (Context.Theory thy) = + (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy) + | loc_begin NONE (Context.Proof lthy) = + (Context.Proof o Local_Theory.restore, lthy) + | loc_begin (SOME loc) (Context.Proof lthy) = + (Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy)); (* datatype node *) @@ -477,8 +476,8 @@ fun local_theory_presentation loc f = present_transaction (fn int => (fn Theory (gthy, _) => let - val finish = loc_finish loc gthy; - val lthy' = loc_begin loc gthy + val (finish, lthy) = loc_begin loc gthy; + val lthy' = lthy |> local_theory_group |> f int |> Local_Theory.reset_group; @@ -511,34 +510,37 @@ local -fun begin_proof init finish = transaction (fn int => +fun begin_proof init = transaction (fn int => (fn Theory (gthy, _) => let - val prf = init int gthy; + val (finish, prf) = init int gthy; val skip = ! skip_proofs; val (is_goal, no_skip) = (true, Proof.schematic_goal prf) handle ERROR _ => (false, true); + val _ = + if is_goal andalso skip andalso no_skip then + warning "Cannot skip proof of schematic goal statement" + else (); in - if is_goal andalso skip andalso no_skip then - warning "Cannot skip proof of schematic goal statement" - else (); if skip andalso not no_skip then - SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) - else Proof (Proof_Node.init prf, (finish gthy, gthy)) + SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy)) + else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' loc f = begin_proof - (fn int => fn gthy => f int (local_theory_group (loc_begin loc gthy))) - (fn gthy => loc_finish loc gthy o Local_Theory.reset_group); + (fn int => fn gthy => + let val (finish, lthy) = loc_begin loc gthy + in (finish o Local_Theory.reset_group, f int (local_theory_group lthy)) end); fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); fun theory_to_proof f = begin_proof - (K (fn Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF)) - (K (Context.Theory o Sign.reset_group o Proof_Context.theory_of)); + (fn _ => fn gthy => + (Context.Theory o Sign.reset_group o Proof_Context.theory_of, + (case gthy of Context.Theory thy => f (global_theory_group thy) | _ => raise UNDEF))); end; diff -r 9d02327ede56 -r 610d9c212376 src/Pure/type_infer_context.ML --- a/src/Pure/type_infer_context.ML Tue Apr 03 16:45:44 2012 +0100 +++ b/src/Pure/type_infer_context.ML Tue Apr 03 17:48:16 2012 +0200 @@ -7,6 +7,7 @@ signature TYPE_INFER_CONTEXT = sig val const_sorts: bool Config.T + val const_type: Proof.context -> string -> typ option val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list val prepare: Proof.context -> term list -> int * term list val infer_types: Proof.context -> term list -> term list