--- 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 \
--- /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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
+ and one :: "'a"
+ and inverse :: "'a => 'a"
+ assumes assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
+ and left_one: "\<And>x. one ** x = x"
+ and left_inverse: "\<And>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 "\<dots> = one ** x ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = 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 "\<dots> = x ** inverse x ** x"
+ by (simp only: assoc)
+ also have "\<dots> = one ** x"
+ by (simp only: right_inverse)
+ also have "\<dots> = x"
+ by (simp only: left_one)
+ finally show "x ** one = x" .
+qed
+
+lemma one_equality: "e ** x = x \<Longrightarrow> one = e"
+proof -
+ fix e x
+ assume eq: "e ** x = x"
+ have "one = x ** inverse x"
+ by (simp only: right_inverse)
+ also have "\<dots> = (e ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = e ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = e ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = e"
+ by (simp only: right_one)
+ finally show "one = e" .
+qed
+
+lemma inverse_equality: "x' ** x = one \<Longrightarrow> 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 "\<dots> = (x' ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = x' ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = x' ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = x'"
+ by (simp only: right_one)
+ finally show "inverse x = x'" .
+qed
+
+end
+
+end
--- /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 \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70)
+ and one :: "'a"
+ and inverse :: "'a => 'a"
+ assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
+ and left_one: "\<And>x. one ** x = x"
+ and left_inverse: "\<And>x. inverse x ** x = one"
+
+ txt {* some consequences *}
+
+ have right_inverse: "\<And>x. x ** inverse x = one"
+ proof -
+ fix x
+ have "x ** inverse x = one ** (x ** inverse x)"
+ by (simp only: left_one)
+ also have "\<dots> = one ** x ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** one ** inverse x"
+ by (simp only: left_inverse)
+ also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = inverse (inverse x) ** inverse x"
+ by (simp only: left_one)
+ also have "\<dots> = one"
+ by (simp only: left_inverse)
+ finally show "x ** inverse x = one" .
+ qed
+
+ have right_one: "\<And>x. x ** one = x"
+ proof -
+ fix x
+ have "x ** one = x ** (inverse x ** x)"
+ by (simp only: left_inverse)
+ also have "\<dots> = x ** inverse x ** x"
+ by (simp only: assoc)
+ also have "\<dots> = one ** x"
+ by (simp only: right_inverse)
+ also have "\<dots> = x"
+ by (simp only: left_one)
+ finally show "x ** one = x" .
+ qed
+
+ have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
+ proof -
+ fix e x
+ assume eq: "e ** x = x"
+ have "one = x ** inverse x"
+ by (simp only: right_inverse)
+ also have "\<dots> = (e ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = e ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = e ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = e"
+ by (simp only: right_one)
+ finally show "one = e" .
+ qed
+
+ have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> 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 "\<dots> = (x' ** x) ** inverse x"
+ by (simp only: eq)
+ also have "\<dots> = x' ** (x ** inverse x)"
+ by (simp only: assoc)
+ also have "\<dots> = x' ** one"
+ by (simp only: right_inverse)
+ also have "\<dots> = x'"
+ by (simp only: right_one)
+ finally show "inverse x = x'" .
+ qed
+
+end
+
+end
--- 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;
--- 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
--- 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;
--- 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;
--- 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 *)
--- 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;
--- 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;
--- 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 *)
--- 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;
--- 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