Merged.
--- a/NEWS Wed Apr 07 20:40:42 2010 +0200
+++ b/NEWS Wed Apr 07 22:22:49 2010 +0200
@@ -83,6 +83,9 @@
* Code generator: details of internal data cache have no impact on
the user space functionality any longer.
+* Methods unfold_locales and intro_locales ignore non-locale subgoals. This
+is more appropriate for interpretations with 'where'. INCOMPATIBILITY.
+
* Discontinued unnamed infix syntax (legacy feature for many years) --
need to specify constant name and syntax separately. Internal ML
datatype constructors have been renamed from InfixName to Infix etc.
--- a/src/FOL/ex/LocaleTest.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/FOL/ex/LocaleTest.thy Wed Apr 07 22:22:49 2010 +0200
@@ -572,40 +572,132 @@
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le.less_thm2)
+text {* Mixin does not leak to a side branch. *}
+
+locale mixin3 = reflexive
+begin
+lemmas less_thm3 = less_def
+end
+
+interpretation le: mixin3 gle
+ by unfold_locales
+
+thm le.less_thm3 (* mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
+
text {* Mixin only available in original context *}
-(* This section is not finished. *)
+locale mixin4_base = reflexive
+
+locale mixin4_mixin = mixin4_base
-locale mixin3 = mixin le' for le' :: "'a => 'a => o" (infix "\<sqsubseteq>''" 50)
+interpretation le: mixin4_mixin gle
+ where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+ show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
+ note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
+ show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+locale mixin4_copy = mixin4_base
+begin
+lemmas less_thm4 = less_def
+end
-lemma (in mixin2) before:
- "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
+begin
+lemmas less_thm4' = less_def
+end
+
+interpretation le4: mixin4_combined gle' gle
+ by unfold_locales (rule grefl')
+
+thm le4.less_thm4' (* mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+ by (rule le4.less_thm4')
+
+text {* Inherited mixin applied to new theorem *}
+
+locale mixin5_base = reflexive
+
+locale mixin5_inherited = mixin5_base
+
+interpretation le5: mixin5_base gle
+ where "reflexive.less(gle, x, y) <-> gless(x, y)"
proof -
- have "reflexive(gle)" by unfold_locales (rule grefl)
- note th = reflexive.less_def[OF this]
- then show ?thesis by (simp add: th)
+ show "mixin5_base(gle)" by unfold_locales
+ note reflexive = this[unfolded mixin5_base_def mixin_def]
+ show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-interpretation le': mixin2 gle'
- apply unfold_locales apply (rule grefl') done
+interpretation le5: mixin5_inherited gle
+ by unfold_locales
+
+lemmas (in mixin5_inherited) less_thm5 = less_def
+
+thm le5.less_thm5 (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+ by (rule le5.less_thm5)
+
+text {* Mixin pushed down to existing inherited locale *}
+
+locale mixin6_base = reflexive
-lemma (in mixin2) after:
- "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+locale mixin6_inherited = mixin5_base
+
+interpretation le6: mixin6_base gle
+ by unfold_locales
+interpretation le6: mixin6_inherited gle
+ by unfold_locales
+interpretation le6: mixin6_base gle
+ where "reflexive.less(gle, x, y) <-> gless(x, y)"
proof -
- have "reflexive(gle)" by unfold_locales (rule grefl)
- note th = reflexive.less_def[OF this]
- then show ?thesis by (simp add: th)
+ show "mixin6_base(gle)" by unfold_locales
+ note reflexive = this[unfolded mixin6_base_def mixin_def]
+ show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-thm le'.less_def le'.less_thm le'.less_thm2 le'.before le'.after
+lemmas (in mixin6_inherited) less_thm6 = less_def
+
+thm le6.less_thm6 (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+ by (rule le6.less_thm6)
-locale combined = le: reflexive le + le': mixin le'
- for le :: "'a => 'a => o" (infixl "\<sqsubseteq>" 50) and le' :: "'a => 'a => o" (infixl "\<sqsubseteq>''" 50)
+text {* Existing mixin inherited through sublocale relation *}
+
+locale mixin7_base = reflexive
+
+locale mixin7_inherited = reflexive
-interpretation combined gle gle'
- apply unfold_locales done
+interpretation le7: mixin7_base gle
+ where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+ show "mixin7_base(gle)" by unfold_locales
+ note reflexive = this[unfolded mixin7_base_def mixin_def]
+ show "reflexive.less(gle, x, y) <-> gless(x, y)"
+ by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+interpretation le7: mixin7_inherited gle
+ by unfold_locales
-thm le.less_def le.less_thm le'.less_def le'.less_thm
+lemmas (in mixin7_inherited) less_thm7 = less_def
+
+thm le7.less_thm7 (* before, mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+ by (rule le7.less_thm7)
+
+sublocale mixin7_inherited < mixin7_base
+ by unfold_locales
+
+lemmas (in mixin7_inherited) less_thm7b = less_def
+
+thm le7.less_thm7b (* after, mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+ by (rule le7.less_thm7b)
subsection {* Interpretation in proofs *}
--- a/src/HOL/Algebra/UnivPoly.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Wed Apr 07 22:22:49 2010 +0200
@@ -1343,14 +1343,8 @@
text {* Interpretation of ring homomorphism lemmas. *}
sublocale UP_univ_prop < ring_hom_cring P S Eval
- apply (unfold Eval_def)
- apply intro_locales
- apply (rule ring_hom_cring.axioms)
- apply (rule ring_hom_cring.intro)
- apply unfold_locales
- apply (rule eval_ring_hom)
- apply rule
- done
+ unfolding Eval_def
+ by unfold_locales (fast intro: eval_ring_hom)
lemma (in UP_cring) monom_pow:
assumes R: "a \<in> carrier R"
@@ -1437,10 +1431,7 @@
lemma ring_homD:
assumes Phi: "Phi \<in> ring_hom P S"
shows "ring_hom_cring P S Phi"
-proof (rule ring_hom_cring.intro)
- show "ring_hom_cring_axioms P S Phi"
- by (rule ring_hom_cring_axioms.intro) (rule Phi)
-qed unfold_locales
+ by unfold_locales (rule Phi)
theorem UP_universal_property:
assumes S: "s \<in> carrier S"
@@ -1761,9 +1752,9 @@
shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
(is "eval R R id a ?g = _")
proof -
- interpret UP_pre_univ_prop R R id proof qed simp
+ interpret UP_pre_univ_prop R R id by unfold_locales simp
have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
- interpret ring_hom_cring P R "eval R R id a" proof qed (simp add: eval_ring_hom)
+ interpret ring_hom_cring P R "eval R R id a" by unfold_locales (rule eval_ring_hom)
have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
and mon0_closed: "monom P a 0 \<in> carrier P"
and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
--- a/src/HOL/Lattices.thy Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/Lattices.thy Wed Apr 07 22:22:49 2010 +0200
@@ -370,8 +370,7 @@
lemma dual_bounded_lattice:
"bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
- by (rule bounded_lattice.intro, rule dual_lattice)
- (unfold_locales, auto simp add: less_le_not_le)
+ by unfold_locales (auto simp add: less_le_not_le)
lemma inf_bot_left [simp]:
"\<bottom> \<sqinter> x = \<bottom>"
--- a/src/Pure/Isar/locale.ML Wed Apr 07 20:40:42 2010 +0200
+++ b/src/Pure/Isar/locale.ML Wed Apr 07 22:22:49 2010 +0200
@@ -95,11 +95,17 @@
intros: thm option * thm option,
axioms: thm list,
(** dynamic part **)
- syntax_decls: (declaration * stamp) list,
+(* <<<<<<< local
+ decls: (declaration * serial) list * (declaration * serial) list,
+ (* type and term syntax declarations *)
+ notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
+======= *)
+ syntax_decls: (declaration * serial) list,
(* syntax declarations *)
- notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
+ notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
+(* >>>>>>> other *)
(* theorem declarations *)
- dependencies: ((string * morphism) * stamp) list
+ dependencies: ((string * morphism) * serial) list
(* locale dependencies (sublocale relation) *)
};
@@ -142,8 +148,13 @@
thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
(binding,
mk_locale ((parameters, spec, intros, axioms),
- ((map (fn decl => (decl, stamp ())) syntax_decls, map (fn n => (n, stamp ())) notes),
- map (fn d => (d, stamp ())) dependencies))) #> snd);
+(* <<<<<<< local
+ ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
+ map (fn d => (d, serial ())) dependencies))) #> snd);
+======= *)
+ ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
+ map (fn d => (d, serial ())) dependencies))) #> snd);
+(* >>>>>>> other *)
fun change_locale name =
Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
@@ -329,10 +340,13 @@
structure Registrations = Theory_Data
(
- type T = ((string * (morphism * morphism)) * stamp) list *
- (* registrations, in reverse order of declaration *)
- (stamp * ((morphism * bool) * stamp) list) list;
- (* alist of mixin lists, per list mixins in reverse order of declaration *)
+ type T = ((string * (morphism * morphism)) * serial) list *
+ (* registrations, in reverse order of declaration;
+ serial points to mixin list *)
+ (serial * ((morphism * bool) * serial) list) list;
+ (* alist of mixin lists, per list mixins in reverse order of declaration;
+ lists indexed by registration serial,
+ entries for empty lists may be omitted *)
val empty = ([], []);
val extend = I;
fun merge ((r1, m1), (r2, m2)) : T =
@@ -344,19 +358,12 @@
(* Primitive operations *)
-fun compose_mixins mixins =
- fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
-
-fun reg_morph mixins ((name, (base, export)), stamp) =
- let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
- in (name, base $> mix $> export) end;
+fun add_reg export (dep, morph) =
+ Registrations.map (apfst (cons ((dep, (morph, export)), serial ())));
-fun these_registrations thy name = Registrations.get thy
- |>> filter (curry (op =) name o fst o fst)
- |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
-
-fun all_registrations thy = Registrations.get thy
- |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
+fun add_mixin serial' mixin =
+ (* registration to be amended identified by its serial id *)
+ Registrations.map (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ()))));
fun get_mixins thy (name, morph) =
let
@@ -365,13 +372,31 @@
case find_first (fn ((name', (morph', export')), _) => ident_eq thy
((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
NONE => []
- | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
+ | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
end;
fun collect_mixins thy (name, morph) =
roundup thy (fn dep => fn mixins =>
merge (eq_snd op =) (mixins, get_mixins thy dep)) Morphism.identity (name, morph) ([], [])
|> snd |> filter (snd o fst); (* only inheritable mixins *)
+ (* FIXME refactor usage *)
+
+fun compose_mixins mixins =
+ fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
+
+fun reg_morph mixins ((name, (base, export)), serial) =
+ let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
+ in (name, base $> mix $> export) end;
+
+fun these_registrations thy name = Registrations.get thy
+ |>> filter (curry (op =) name o fst o fst)
+ (* with inherited mixins *)
+ |-> (fn regs => fn _ => map (fn ((name, (base, export)) ,_) =>
+ (name, base $> (collect_mixins thy (name, base $> export) |> compose_mixins) $> export)) regs);
+
+fun all_registrations thy = Registrations.get thy
+ |-> (fn regs => fn mixins => map (reg_morph mixins) regs);
+ (* without inherited mixins *)
fun activate_notes' activ_elem transfer thy export (name, morph) input =
let
@@ -440,9 +465,7 @@
quote (extern thy name) ^ " and\nparameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
" available")
- | SOME (_, stamp') => Registrations.map
- (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
- (* FIXME deal with inheritance: propagate to existing children *)
+ | SOME (_, serial') => add_mixin serial' mixin thy
end;
(* Note that a registration that would be subsumed by an existing one will not be
@@ -455,37 +478,31 @@
if member (ident_eq thy) (get_idents (Context.Theory thy)) (name, base)
then thy
else
- let
- fun add_reg (dep', morph') =
- let
- val mixins = collect_mixins thy (dep', morph' $> export);
- val stamp = stamp ();
- in
- Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
- #> apsnd (cons (stamp, mixins)))
- end
- in
- (get_idents (Context.Theory thy), thy)
- (* add new registrations with inherited mixins *)
- |> roundup thy add_reg export (name, base_morph)
- |> snd
- (* add mixin *)
- |> (case mixin of NONE => I
- | SOME mixin => amend_registration (name, base_morph) mixin export)
- (* activate import hierarchy as far as not already active *)
- |> Context.theory_map (activate_facts' export (name, base_morph))
- end
+ (get_idents (Context.Theory thy), thy)
+ (* add new registrations with inherited mixins *)
+ |> roundup thy (add_reg export) export (name, base_morph)
+ |> snd
+ (* add mixin *)
+ |> (case mixin of NONE => I
+ | SOME mixin => amend_registration (name, base_morph) mixin export)
+ (* activate import hierarchy as far as not already active *)
+ |> Context.theory_map (activate_facts' export (name, base_morph))
end;
(*** Dependencies ***)
+fun add_reg_activate_facts export (dep, morph) thy =
+ (get_idents (Context.Theory thy), thy)
+ |> roundup thy (add_reg export) export (dep, morph)
+ |> snd
+ |> Context.theory_map (activate_facts' export (dep, morph));
+
fun add_dependency loc (dep, morph) export thy =
thy
- |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
- |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
+ |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
+ |> (fn thy => fold_rev (add_reg_activate_facts export)
(all_registrations thy) thy);
- (* FIXME deal with inheritance: propagate mixins to new children *)
(*** Storing results ***)
@@ -496,7 +513,7 @@
let
val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
val ctxt'' = ctxt' |> ProofContext.theory (
- (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
+ (change_locale loc o apfst o apsnd) (cons (args', serial ()))
#>
(* Registrations *)
(fn thy => fold_rev (fn (_, morph) =>
@@ -510,14 +527,23 @@
(* Declarations *)
+(* <<<<<<< local
+local
+
+fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
+
+fun add_decls add loc decl =
+ ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
+======= *)
fun add_declaration loc decl =
+(* >>>>>>> other *)
add_thmss loc ""
[((Binding.conceal Binding.empty,
[Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
[([Drule.dummy_thm], [])])];
fun add_syntax_declaration loc decl =
- ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, stamp ())))
+ ProofContext.theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
#> add_declaration loc decl;
@@ -550,15 +576,17 @@
(* Tactic *)
-fun intro_locales_tac eager ctxt =
- Method.intros_tac
+fun gen_intro_locales_tac intros_tac eager ctxt =
+ intros_tac
(get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
+val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
+val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
+
val _ = Context.>> (Context.map_theory
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
+ (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
"back-chain introduction rules of locales without unfolding predicates" #>
- Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
+ Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
"back-chain all introduction rules of locales"));
end;
-
--- a/src/Pure/Isar/method.ML Wed Apr 07 20:40:42 2010 +0200
+++ b/src/Pure/Isar/method.ML Wed Apr 07 22:22:49 2010 +0200
@@ -46,6 +46,7 @@
val rule_tac: thm list -> thm list -> int -> tactic
val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
val intros_tac: thm list -> thm list -> tactic
+ val try_intros_tac: thm list -> thm list -> tactic
val rule: thm list -> method
val erule: int -> thm list -> method
val drule: int -> thm list -> method
@@ -262,11 +263,13 @@
(* intros_tac -- pervasive search spanned by intro rules *)
-fun intros_tac intros facts =
- ALLGOALS (insert_tac facts THEN'
+fun gen_intros_tac goals intros facts =
+ goals (insert_tac facts THEN'
REPEAT_ALL_NEW (resolve_tac intros))
THEN Tactic.distinct_subgoals_tac;
+val intros_tac = gen_intros_tac ALLGOALS;
+val try_intros_tac = gen_intros_tac TRYALL;
(* ML tactics *)