--- a/NEWS Wed Nov 19 18:15:31 2008 +0100
+++ b/NEWS Thu Nov 20 00:03:47 2008 +0100
@@ -47,6 +47,11 @@
*** Pure ***
+* Slightly more coherent Pure syntax, with updated documentation in
+isar-ref manual. Removed locales meta_term_syntax and
+meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
+INCOMPATIBILITY in rare situations.
+
* Goal-directed proof now enforces strict proof irrelevance wrt. sort
hypotheses. Sorts required in the course of reasoning need to be
covered by the constraints in the initial statement, completed by the
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 20 00:03:47 2008 +0100
@@ -485,6 +485,7 @@
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
& @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
+ & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
& @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
& @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
& @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
@@ -493,18 +494,21 @@
& @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
& @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
& @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
+ & @{text "|"} & @{verbatim TERM} @{text logic} \\
& @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
- @{syntax_def (inner) aprop} & = & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
+ @{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
+ & @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
+ & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
@{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
& @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
+ & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
& @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
& @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
- & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
& @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\
@@ -847,7 +851,7 @@
Priority information attached to chain productions is ignored; only
the dummy value @{text "-1"} is displayed.
- \item @{text "print_modes"} lists the alternative print modes
+ \item @{text "print modes"} lists the alternative print modes
provided by this grammar; see \secref{sec:print-modes}.
\item @{text "parse_rules"} and @{text "print_rules"} relate to
--- a/doc-src/IsarRef/Thy/Proof.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 20 00:03:47 2008 +0100
@@ -381,7 +381,7 @@
Goals may consist of multiple statements, resulting in a list of
facts eventually. A pending multi-goal is internally represented as
- a meta-level conjunction (printed as @{text "&&"}), which is usually
+ a meta-level conjunction (@{text "&&&"}), which is usually
split into the corresponding number of sub-goals prior to an initial
method application, via @{command_ref "proof"}
(\secref{sec:proof-steps}) or @{command_ref "apply"}
--- a/src/FOL/FOL.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/FOL/FOL.thy Thu Nov 20 00:03:47 2008 +0100
@@ -346,9 +346,7 @@
lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
unfolding atomize_eq induct_equal_def .
-lemma induct_conj_eq:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(A && B) == Trueprop(induct_conj(A, B))"
+lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))"
unfolding atomize_conj induct_conj_def .
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
--- a/src/FOL/IFOL.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/FOL/IFOL.thy Thu Nov 20 00:03:47 2008 +0100
@@ -698,11 +698,9 @@
then show "A == B" by (rule iff_reflection)
qed
-lemma atomize_conj [atomize]:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(A && B) == Trueprop (A & B)"
+lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
proof
- assume conj: "A && B"
+ assume conj: "A &&& B"
show "A & B"
proof (rule conjI)
from conj show A by (rule conjunctionD1)
@@ -710,7 +708,7 @@
qed
next
assume conj: "A & B"
- show "A && B"
+ show "A &&& B"
proof -
from conj show A ..
from conj show B ..
--- a/src/HOL/Code_Setup.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Code_Setup.thy Thu Nov 20 00:03:47 2008 +0100
@@ -78,9 +78,8 @@
using assms by simp_all
lemma If_case_cert:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
assumes "CASE \<equiv> (\<lambda>b. If b f g)"
- shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
+ shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
using assms by simp_all
setup {*
--- a/src/HOL/Groebner_Basis.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Nov 20 00:03:47 2008 +0100
@@ -64,10 +64,8 @@
subsubsection {* Declaring the abstract theory *}
lemma semiring_ops:
- fixes meta_term :: "'a => prop" ("TERM _")
shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
- and "TERM r0" and "TERM r1"
- by rule+
+ and "TERM r0" and "TERM r1" .
lemma semiring_rules:
"add (mul a m) (mul b m) = mul (add a b) m"
@@ -226,9 +224,7 @@
and sub_add: "sub x y = add x (neg y)"
begin
-lemma ring_ops:
- fixes meta_term :: "'a => prop" ("TERM _")
- shows "TERM (sub x y)" and "TERM (neg x)" .
+lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
lemmas ring_rules = neg_mul sub_add
--- a/src/HOL/HOL.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/HOL.thy Thu Nov 20 00:03:47 2008 +0100
@@ -845,11 +845,9 @@
then show "x == y" by (rule eq_reflection)
qed
-lemma atomize_conj [atomize]:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(A && B) == Trueprop (A & B)"
+lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
proof
- assume conj: "A && B"
+ assume conj: "A &&& B"
show "A & B"
proof (rule conjI)
from conj show A by (rule conjunctionD1)
@@ -857,7 +855,7 @@
qed
next
assume conj: "A & B"
- show "A && B"
+ show "A &&& B"
proof -
from conj show A ..
from conj show B ..
@@ -1511,9 +1509,7 @@
lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
by (unfold atomize_eq induct_equal_def)
-lemma induct_conj_eq:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(A && B) == Trueprop (induct_conj A B)"
+lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
by (unfold atomize_conj induct_conj_def)
lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
--- a/src/HOL/Library/Coinductive_List.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Thu Nov 20 00:03:47 2008 +0100
@@ -216,9 +216,8 @@
CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
lemma llist_case_cert:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
assumes "CASE \<equiv> llist_case c d"
- shows "(CASE LNil \<equiv> c) && (CASE (LCons M N) \<equiv> d M N)"
+ shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
using assms by simp_all
setup {*
--- a/src/HOL/Library/Dense_Linear_Order.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy Thu Nov 20 00:03:47 2008 +0100
@@ -268,7 +268,6 @@
lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
lemma atoms:
- fixes meta_term :: "'a => prop" ("TERM _")
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
and "TERM (op = :: 'a \<Rightarrow> _)" .
@@ -505,7 +504,6 @@
lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
by (rule constr_dense_linear_order_axioms)
lemma atoms:
- fixes meta_term :: "'a => prop" ("TERM _")
shows "TERM (less :: 'a \<Rightarrow> _)"
and "TERM (less_eq :: 'a \<Rightarrow> _)"
and "TERM (op = :: 'a \<Rightarrow> _)" .
--- a/src/Pure/Isar/proof_context.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Nov 20 00:03:47 2008 +0100
@@ -1060,10 +1060,14 @@
val _ = Context.>> (Context.map_theory
(Sign.add_syntax
- [("_context_const", "id => 'a", Delimfix "CONST _"),
- ("_context_const", "longid => 'a", Delimfix "CONST _"),
- ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
- ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
+ [("_context_const", "id => logic", Delimfix "CONST _"),
+ ("_context_const", "id => aprop", Delimfix "CONST _"),
+ ("_context_const", "longid => logic", Delimfix "CONST _"),
+ ("_context_const", "longid => aprop", Delimfix "CONST _"),
+ ("_context_xconst", "id => logic", Delimfix "XCONST _"),
+ ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
+ ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
+ ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
Sign.add_advanced_trfuns
([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
--- a/src/Pure/Pure.thy Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Pure.thy Thu Nov 20 00:03:47 2008 +0100
@@ -24,34 +24,22 @@
"(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
-subsection {* Embedded terms *}
-
-locale meta_term_syntax =
- fixes meta_term :: "'a => prop" ("TERM _")
-
-lemmas [intro?] = termI
-
-
subsection {* Meta-level conjunction *}
-locale meta_conjunction_syntax =
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
-
lemma all_conjunction:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
+ "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
proof
- assume conj: "!!x. PROP A x && PROP B x"
- show "(!!x. PROP A x) && (!!x. PROP B x)"
+ assume conj: "!!x. PROP A x &&& PROP B x"
+ show "(!!x. PROP A x) &&& (!!x. PROP B x)"
proof -
fix x
from conj show "PROP A x" by (rule conjunctionD1)
from conj show "PROP B x" by (rule conjunctionD2)
qed
next
- assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
+ assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
fix x
- show "PROP A x && PROP B x"
+ show "PROP A x &&& PROP B x"
proof -
show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
@@ -59,20 +47,19 @@
qed
lemma imp_conjunction:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
+ "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
proof
- assume conj: "PROP A ==> PROP B && PROP C"
- show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
+ assume conj: "PROP A ==> PROP B &&& PROP C"
+ show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
proof -
assume "PROP A"
from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
qed
next
- assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
+ assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
assume "PROP A"
- show "PROP B && PROP C"
+ show "PROP B &&& PROP C"
proof -
from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
@@ -80,18 +67,17 @@
qed
lemma conjunction_imp:
- fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
- shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
+ "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
proof
- assume r: "PROP A && PROP B ==> PROP C"
+ assume r: "PROP A &&& PROP B ==> PROP C"
assume ab: "PROP A" "PROP B"
show "PROP C"
proof (rule r)
- from ab show "PROP A && PROP B" .
+ from ab show "PROP A &&& PROP B" .
qed
next
assume r: "PROP A ==> PROP B ==> PROP C"
- assume conj: "PROP A && PROP B"
+ assume conj: "PROP A &&& PROP B"
show "PROP C"
proof (rule r)
from conj show "PROP A" by (rule conjunctionD1)
--- a/src/Pure/Syntax/simple_syntax.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Syntax/simple_syntax.ML Thu Nov 20 00:03:47 2008 +0100
@@ -18,7 +18,7 @@
(* scanning tokens *)
val lexicon = Scan.make_lexicon
- (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]);
+ (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&&", "CONST"]);
fun read scan s =
(case
@@ -81,7 +81,7 @@
| term2
term2 = term3 == term2
| term3 =?= term2
- | term3 && term2
+ | term3 &&& term2
| term3
term3 = ident :: typ
| var :: typ
@@ -111,7 +111,7 @@
term2 env T) x
and term2 env T x =
(equal env "==" || equal env "=?=" ||
- term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction ||
+ term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
term3 env T) x
and equal env eq x =
(term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
--- a/src/Pure/Syntax/syn_ext.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Thu Nov 20 00:03:47 2008 +0100
@@ -10,6 +10,7 @@
val dddot_indexname: indexname
val constrainC: string
val typeT: typ
+ val spropT: typ
val max_pri: int
val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
val mk_trfun: string * 'a -> string * ('a * stamp)
--- a/src/Pure/Syntax/syn_trans.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/Syntax/syn_trans.ML Thu Nov 20 00:03:47 2008 +0100
@@ -473,9 +473,8 @@
("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
[("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
- ("_sort_constraint", sort_constraint_tr), ("\\<^fixed>meta_conjunction", conjunction_tr),
- ("_TYPE", type_tr), ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr),
- ("_index", index_tr)],
+ ("_sort_constraint", sort_constraint_tr), ("_TYPE", type_tr),
+ ("_DDDOT", dddot_tr), ("_index", index_tr)],
([]: (string * (term list -> term)) list),
[("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
--- a/src/Pure/conjunction.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/conjunction.ML Thu Nov 20 00:03:47 2008 +0100
@@ -67,7 +67,7 @@
val B = read_prop "B" and vB = read_prop "?B";
val C = read_prop "C";
val ABC = read_prop "A ==> B ==> C";
-val A_B = read_prop "A && B";
+val A_B = read_prop "A &&& B";
val conjunction_def =
Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
@@ -135,7 +135,7 @@
in
(*
- A1 && ... && An ==> B
+ A1 &&& ... &&& An ==> B
-----------------------
A1 ==> ... ==> An ==> B
*)
@@ -155,7 +155,7 @@
(*
A1 ==> ... ==> An ==> B
-----------------------
- A1 && ... && An ==> B
+ A1 &&& ... &&& An ==> B
*)
fun uncurry_balanced n th =
if n < 2 then th
--- a/src/Pure/logic.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/logic.ML Thu Nov 20 00:03:47 2008 +0100
@@ -162,33 +162,33 @@
val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
-(*A && B*)
+(*A &&& B*)
fun mk_conjunction (A, B) = conjunction $ A $ B;
-(*A && B && C -- improper*)
+(*A &&& B &&& C -- improper*)
fun mk_conjunction_list [] = true_prop
| mk_conjunction_list ts = foldr1 mk_conjunction ts;
-(*(A && B) && (C && D) -- balanced*)
+(*(A &&& B) &&& (C &&& D) -- balanced*)
fun mk_conjunction_balanced [] = true_prop
| mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
-(*A && B*)
+(*A &&& B*)
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
| dest_conjunction t = raise TERM ("dest_conjunction", [t]);
-(*A && B && C -- improper*)
+(*A &&& B &&& C -- improper*)
fun dest_conjunction_list t =
(case try dest_conjunction t of
NONE => [t]
| SOME (A, B) => A :: dest_conjunction_list B);
-(*(A && B) && (C && D) -- balanced*)
+(*(A &&& B) &&& (C &&& D) -- balanced*)
fun dest_conjunction_balanced 0 _ = []
| dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
-(*((A && B) && C) && D && E -- flat*)
+(*((A &&& B) &&& C) &&& D &&& E -- flat*)
fun dest_conjunctions t =
(case try dest_conjunction t of
NONE => [t]
--- a/src/Pure/pure_thy.ML Wed Nov 19 18:15:31 2008 +0100
+++ b/src/Pure/pure_thy.ML Thu Nov 20 00:03:47 2008 +0100
@@ -244,6 +244,9 @@
val term = SimpleSyntax.read_term;
val prop = SimpleSyntax.read_prop;
+val typeT = Syntax.typeT;
+val spropT = Syntax.spropT;
+
(* application syntax variants *)
@@ -301,6 +304,7 @@
("", typ "idt => pttrn", Delimfix "_"),
("", typ "pttrn => pttrns", Delimfix "_"),
("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
+ ("", typ "aprop => aprop", Delimfix "'(_')"),
("", typ "id => aprop", Delimfix "_"),
("", typ "longid => aprop", Delimfix "_"),
("", typ "var => aprop", Delimfix "_"),
@@ -324,13 +328,16 @@
("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
("==>", typ "prop => prop => prop", Delimfix "op ==>"),
(Term.dummy_patternN, typ "aprop", Delimfix "'_"),
- ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))")]
+ ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
+ ("Pure.term", typ "logic => prop", Delimfix "TERM _"),
+ ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&&", 2))]
#> Sign.add_syntax_i applC_syntax
#> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
[("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "'a => type => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_type_constraint_", typ "'a", NoSyn),
@@ -342,9 +349,7 @@
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
#> Sign.add_modesyntax_i ("", false)
- [("prop", typ "prop => prop", Mixfix ("_", [0], 0)),
- ("Pure.term", typ "'a => prop", Delimfix "TERM _"),
- ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))]
+ [("prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_modesyntax_i ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts_i
@@ -372,7 +377,7 @@
("sort_constraint_def",
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
- ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+ ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
#> Sign.hide_const false "Pure.term"
#> Sign.hide_const false "Pure.sort_constraint"
#> Sign.hide_const false "Pure.conjunction"