Strict prefixes in locales expressions.
authorballarin
Sun Dec 14 15:43:04 2008 +0100 (2008-12-14)
changeset 2921476c7fc5ba849
parent 29213 c3ed38de863c
child 29215 f98862eb0591
child 29231 1951b3dd1df8
Strict prefixes in locales expressions.
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/spec_parse.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 12 19:58:26 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Sun Dec 14 15:43:04 2008 +0100
     1.3 @@ -421,7 +421,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -interpretation x: logic_o "op &" "Not"
     1.8 +interpretation x!: logic_o "op &" "Not"
     1.9    where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
    1.10  proof -
    1.11    show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
    1.12 @@ -431,9 +431,12 @@
    1.13  
    1.14  thm x.lor_o_def bool_logic_o
    1.15  
    1.16 +lemma lor_triv: "z <-> z" ..
    1.17 +
    1.18  lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
    1.19  
    1.20 -thm x.lor_triv
    1.21 +thm lor_triv [where z = True] (* Check strict prefix. *)
    1.22 +  x.lor_triv
    1.23  
    1.24  
    1.25  subsection {* Interpretation in proofs *}
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 12 19:58:26 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Sun Dec 14 15:43:04 2008 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  signature EXPRESSION =
     2.5  sig
     2.6    datatype 'term map = Positional of 'term option list | Named of (string * 'term) list;
     2.7 -  type 'term expr = (string * (string * 'term map)) list;
     2.8 +  type 'term expr = (string * ((string * bool) * 'term map)) list;
     2.9    type expression = string expr * (Binding.T * string option * mixfix) list;
    2.10    type expression_i = term expr * (Binding.T * typ option * mixfix) list;
    2.11  
    2.12 @@ -47,7 +47,7 @@
    2.13    Positional of 'term option list |
    2.14    Named of (string * 'term) list;
    2.15  
    2.16 -type 'term expr = (string * (string * 'term map)) list;
    2.17 +type 'term expr = (string * ((string * bool) * 'term map)) list;
    2.18  
    2.19  type expression = string expr * (Binding.T * string option * mixfix) list;
    2.20  type expression_i = term expr * (Binding.T * typ option * mixfix) list;
    2.21 @@ -154,7 +154,7 @@
    2.22  
    2.23  (* Instantiation morphism *)
    2.24  
    2.25 -fun inst_morph (parm_names, parm_types) (prfx, insts') ctxt =
    2.26 +fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
    2.27    let
    2.28      (* parameters *)
    2.29      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    2.30 @@ -175,7 +175,7 @@
    2.31      val inst = Symtab.make insts'';
    2.32    in
    2.33      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
    2.34 -      Morphism.binding_morphism (Binding.add_prefix false prfx), ctxt')
    2.35 +      Morphism.binding_morphism (Binding.add_prefix strict prfx), ctxt')
    2.36    end;
    2.37  
    2.38  
     3.1 --- a/src/Pure/Isar/spec_parse.ML	Fri Dec 12 19:58:26 2008 +0100
     3.2 +++ b/src/Pure/Isar/spec_parse.ML	Sun Dec 14 15:43:04 2008 +0100
     3.3 @@ -104,7 +104,7 @@
     3.4  
     3.5  val rename = P.name -- Scan.option P.mixfix;
     3.6  
     3.7 -val prefix = P.name --| P.$$$ ":";
     3.8 +val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":";
     3.9  val named = P.name -- (P.$$$ "=" |-- P.term);
    3.10  val position = P.maybe P.term;
    3.11  val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
    3.12 @@ -127,7 +127,7 @@
    3.13  val locale_expression =
    3.14    let
    3.15      fun expr2 x = P.xname x;
    3.16 -    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    3.17 +    fun expr1 x = (Scan.optional prefix ("", false) -- expr2 --
    3.18        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    3.19      fun expr0 x = (plus1_unless locale_keyword expr1) x;
    3.20    in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;