Intro_locales_tac to simplify goals involving locale predicates.
authorballarin
Fri Nov 28 17:43:06 2008 +0100 (2008-11-28)
changeset 28903b3fc3a62247a
parent 28902 2019bcc9d8bf
child 28904 3ef9489eeef5
Intro_locales_tac to simplify goals involving locale predicates.
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/new_locale.ML
     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.4  
     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.18  
    1.19  (* effect on printed locale *)
    1.20  
    1.21 @@ -196,20 +196,20 @@
    1.22  (* circular interpretation *)
    1.23  
    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.53  
    1.54  (* effect on printed locale *)
    1.55  
    1.56 @@ -225,7 +225,7 @@
    1.57      and trans: "[| x << y; y << z |] ==> x << z"
    1.58  
    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.63  
    1.64  print_locale! order  (* Only two instances of order. *)
    1.65 @@ -244,7 +244,7 @@
    1.66  end
    1.67  
    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.76  
    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.80  
    1.81  print_locale! trivial
    1.82  
    1.83  context trivial begin thm x.Q [where ?x = True] end
    1.84  
    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.89  
    1.90  print_locale! trivial  (* No instance for y created (subsumed). *)
    1.91  
     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.4  
     2.5  (*** Locale declarations ***)
     2.6  
     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.13  
    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.19  
    2.20  val introN = "intro";
    2.21 -val axiomsN = "axioms";
    2.22  
    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.46  
    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.64  
    2.65      val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
    2.66  
    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.77  
    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.80      
    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.84  
    2.85      fun after_qed' results =
    2.86        fold store_dep (deps ~~ prep_result propss results) #>
    2.87 @@ -827,3 +835,4 @@
    2.88  
    2.89  
    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.6  
     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.15  
    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.26  
    3.27  
    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.48  
    3.49 @@ -340,5 +364,34 @@
    3.50      (fn (parameters, spec, decls, notes, dependencies) =>
    3.51        (parameters, spec, decls, notes, (dep, stamp ()) :: dependencies)));
    3.52  
    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
    3.73 +  (Method.add_methods
    3.74 +    [("new_intro_locales",
    3.75 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac false ctxt)),
    3.76 +      "back-chain introduction rules of locales without unfolding predicates"),
    3.77 +     ("new_unfold_locales",
    3.78 +      Method.ctxt_args (fn ctxt => Method.METHOD (intro_locales_tac true ctxt)),
    3.79 +      "back-chain all introduction rules of locales")]));
    3.80 +
    3.81 +
    3.82  end;
    3.83