author ballarin Fri Nov 28 17:43:06 2008 +0100 (2008-11-28) changeset 28903 b3fc3a62247a parent 28902 2019bcc9d8bf child 28904 3ef9489eeef5
Intro_locales_tac to simplify goals involving locale predicates.
 src/FOL/ex/NewLocaleTest.thy file | annotate | diff | revisions src/Pure/Isar/expression.ML file | annotate | diff | revisions src/Pure/Isar/new_locale.ML file | annotate | diff | revisions
1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Fri Nov 28 12:26:14 2008 +0100
1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Fri Nov 28 17:43:06 2008 +0100
1.3 @@ -167,7 +167,7 @@
1.5  sublocale lgrp < right: rgrp
1.6  print_facts
1.7 -proof (intro rgrp.intro semi.intro rgrp_axioms.intro)
1.8 +proof new_unfold_locales
1.9    {
1.10      fix x
1.11      have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
1.12 @@ -180,7 +180,7 @@
1.13        by (simp add: linv lone rone)
1.14      then show "x ** inv(x) = one" by (simp add: assoc lcancel)
1.15    }
1.16 -qed (simp add: assoc)
1.17 +qed
1.19  (* effect on printed locale *)
1.21 @@ -196,20 +196,20 @@
1.22  (* circular interpretation *)
1.24  sublocale rgrp < left: lgrp
1.25 -  proof (intro lgrp.intro semi.intro lgrp_axioms.intro)
1.26 -    {
1.27 -      fix x
1.28 -      have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
1.29 -      then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
1.30 -    }
1.31 -    note lone = this
1.32 -    {
1.33 -      fix x
1.34 -      have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
1.35 -	by (simp add: rinv lone rone)
1.36 -      then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
1.37 -    }
1.38 -  qed (simp add: assoc)
1.39 +proof new_unfold_locales
1.40 +  {
1.41 +    fix x
1.42 +    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
1.43 +    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
1.44 +  }
1.45 +  note lone = this
1.46 +  {
1.47 +    fix x
1.48 +    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
1.49 +      by (simp add: rinv lone rone)
1.50 +    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
1.51 +  }
1.52 +qed
1.54  (* effect on printed locale *)
1.56 @@ -225,7 +225,7 @@
1.57      and trans: "[| x << y; y << z |] ==> x << z"
1.59  sublocale order < dual: order "%x y. y << x"
1.60 -  apply (rule order.intro) apply (rule refl) apply (blast intro: trans)
1.61 +  apply new_unfold_locales apply (rule refl) apply (blast intro: trans)
1.62    done
1.64  print_locale! order  (* Only two instances of order. *)
1.65 @@ -244,7 +244,7 @@
1.66  end
1.68  sublocale order_with_def < dual: order' "op >>"
1.69 -  apply (intro order'.intro)
1.70 +  apply new_unfold_locales
1.71    unfolding greater_def
1.72    apply (rule refl) apply (blast intro: trans)
1.73    done
1.74 @@ -291,14 +291,15 @@
1.75  end
1.77  sublocale trivial < x: trivial x _
1.78 -  apply (intro trivial.intro) using Q by fast
1.79 +  apply new_unfold_locales using Q by fast
1.81  print_locale! trivial
1.83  context trivial begin thm x.Q [where ?x = True] end
1.85  sublocale trivial < y: trivial Q Q
1.86 -  apply (intro trivial.intro) using Q by fast
1.87 +  by new_unfold_locales
1.88 +  (* Succeeds since previous interpretation is more general. *)
1.90  print_locale! trivial  (* No instance for y created (subsumed). *)
2.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 28 12:26:14 2008 +0100
2.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 28 17:43:06 2008 +0100
2.3 @@ -598,15 +598,17 @@
2.5  (*** Locale declarations ***)
2.7 +(* axiomsN: name of theorem set with destruct rules for locale predicates,
2.8 +     also name suffix of delta predicates and assumptions. *)
2.9 +
2.10 +val axiomsN = "axioms";
2.11 +
2.12  local
2.14  (* introN: name of theorems for introduction rules of locale and
2.15 -     delta predicates;
2.16 -   axiomsN: name of theorem set with destruct rules for locale predicates,
2.17 -     also name suffix of delta predicates. *)
2.18 +     delta predicates *)
2.20  val introN = "intro";
2.21 -val axiomsN = "axioms";
2.23  fun atomize_spec thy ts =
2.24    let
2.25 @@ -695,7 +697,8 @@
2.26              thy'
2.27              |> Sign.add_path aname
2.28              |> Sign.no_base_names
2.29 -            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
2.30 +            |> PureThy.note_thmss Thm.internalK
2.31 +              [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
2.32              ||> Sign.restore_naming thy';
2.33            in (SOME statement, SOME intro, axioms, thy'') end;
2.34      val (b_pred, b_intro, b_axioms, thy'''') =
2.35 @@ -710,7 +713,7 @@
2.36              |> Sign.add_path pname
2.37              |> Sign.no_base_names
2.38              |> PureThy.note_thmss Thm.internalK
2.39 -                 [((Name.binding introN, []), [([intro], [])]),
2.40 +                 [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
2.41                    ((Name.binding axiomsN, []),
2.42                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
2.43              ||> Sign.restore_naming thy''';
2.44 @@ -757,20 +760,25 @@
2.45        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
2.47      val satisfy = Element.satisfy_morphism b_axioms;
2.48 +
2.49      val params = fixed @
2.50        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
2.51 -    val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
2.52 -
2.53 +    val asm = if is_some b_statement then b_statement else a_statement;
2.54 +    val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
2.55      val notes = body_elems' |>
2.56        (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
2.57        fst |> map (Element.morph_ctxt satisfy) |>
2.58 -      map_filter (fn Notes notes => SOME notes | _ => NONE);
2.59 +      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
2.60 +      (if is_some asm
2.61 +        then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
2.62 +          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
2.63 +        else I);
2.65      val deps' = map (fn (l, morph) => (l, morph \$> satisfy)) deps;
2.67      val loc_ctxt = thy' |>
2.68        NewLocale.register_locale name (extraTs, params)
2.69 -        (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], [])
2.70 +        (asm, map prop_of defs) ([], [])
2.71          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
2.72        NewLocale.init name
2.73    in (name, loc_ctxt) end;
2.74 @@ -803,10 +811,10 @@
2.75      val target = intern thy raw_target;
2.76      val target_ctxt = NewLocale.init target thy;
2.78 -    val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
2.79 +    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
2.81      fun store_dep ((name, morph), thms) =
2.82 -      NewLocale.add_dependency target (name, morph \$> Element.satisfy_morphism thms \$> export');
2.83 +      NewLocale.add_dependency target (name, morph \$> Element.satisfy_morphism thms \$> export);
2.85      fun after_qed' results =
2.86        fold store_dep (deps ~~ prep_result propss results) #>
2.87 @@ -827,3 +835,4 @@
2.90  end;
2.91 +
3.1 --- a/src/Pure/Isar/new_locale.ML	Fri Nov 28 12:26:14 2008 +0100
3.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Nov 28 17:43:06 2008 +0100
3.3 @@ -37,7 +37,7 @@
3.4    val add_declaration: string -> declaration -> Proof.context -> Proof.context
3.5    val add_dependency: string -> (string * Morphism.morphism) -> Proof.context -> Proof.context
3.7 -  (* Activate locales *)
3.8 +  (* Activation *)
3.9    val activate_declarations: theory -> string * Morphism.morphism ->
3.10      identifiers * Proof.context -> identifiers * Proof.context
3.11    val activate_facts: theory -> string * Morphism.morphism ->
3.12 @@ -45,12 +45,36 @@
3.13  (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
3.14    val init: string -> theory -> Proof.context
3.16 +  (* Reasoning about locales *)
3.17 +  val witness_attrib: attribute
3.18 +  val intro_attrib: attribute
3.19 +  val unfold_attrib: attribute
3.20 +  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
3.21 +
3.22    (* Diagnostic *)
3.23    val print_locales: theory -> unit
3.24    val print_locale: theory -> bool -> bstring -> unit
3.25  end;
3.28 +(* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
3.29 +functor ThmsFun() =
3.30 +struct
3.31 +
3.32 +structure Data = GenericDataFun
3.33 +(
3.34 +  type T = thm list;
3.35 +  val empty = [];
3.36 +  val extend = I;
3.37 +  fun merge _ = Thm.merge_thms;
3.38 +);
3.39 +
3.40 +val get = Data.get o Context.Proof;
3.41 +val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
3.42 +
3.43 +end;
3.44 +
3.45 +
3.46  structure NewLocale: NEW_LOCALE =
3.47  struct
3.49 @@ -340,5 +364,34 @@
3.50      (fn (parameters, spec, decls, notes, dependencies) =>
3.51        (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies)));
3.53 +
3.54 +(*** Reasoning about locales ***)
3.55 +
3.56 +(** Storage for witnesses, intro and unfold rules **)
3.57 +
3.58 +structure Witnesses = ThmsFun();
3.59 +structure Intros = ThmsFun();
3.60 +structure Unfolds = ThmsFun();
3.61 +
3.62 +val witness_attrib = Witnesses.add;
3.63 +val intro_attrib = Intros.add;
3.64 +val unfold_attrib = Unfolds.add;
3.65 +
3.66 +(** Tactic **)
3.67 +
3.68 +fun intro_locales_tac eager ctxt facts st =
3.69 +  Method.intros_tac
3.70 +    (Witnesses.get ctxt @ Intros.get ctxt @ (if eager then Unfolds.get ctxt else [])) facts st;
3.71 +
3.72 +val _ = Context.>> (Context.map_theory