1.1 --- a/NEWS Wed Nov 19 18:15:31 2008 +0100
1.2 +++ b/NEWS Thu Nov 20 00:03:47 2008 +0100
1.3 @@ -47,6 +47,11 @@
1.4
1.5 *** Pure ***
1.6
1.7 +* Slightly more coherent Pure syntax, with updated documentation in
1.8 +isar-ref manual. Removed locales meta_term_syntax and
1.9 +meta_conjunction_syntax: TERM and &&& (formerly &&) are now permanent,
1.10 +INCOMPATIBILITY in rare situations.
1.11 +
1.12 * Goal-directed proof now enforces strict proof irrelevance wrt. sort
1.13 hypotheses. Sorts required in the course of reasoning need to be
1.14 covered by the constraints in the initial statement, completed by the
2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Wed Nov 19 18:15:31 2008 +0100
2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Nov 20 00:03:47 2008 +0100
2.3 @@ -485,6 +485,7 @@
2.4 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=?="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
2.5 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "=="} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
2.6 & @{text "|"} & @{text "any\<^sup>(\<^sup>3\<^sup>)"} @{text "\<equiv>"} @{text "any\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
2.7 + & @{text "|"} & @{text "prop\<^sup>(\<^sup>3\<^sup>)"} @{verbatim "&&&"} @{text "prop\<^sup>(\<^sup>2\<^sup>)"} & @{text "(2)"} \\
2.8 & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
2.9 & @{text "|"} & @{text "prop\<^sup>(\<^sup>2\<^sup>)"} @{text "\<Longrightarrow>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
2.10 & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\<dots>"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\
2.11 @@ -493,18 +494,21 @@
2.12 & @{text "|"} & @{text "\<And>"} @{text idts} @{verbatim "."} @{text prop} & @{text "(0)"} \\
2.13 & @{text "|"} & @{verbatim OFCLASS} @{verbatim "("} @{text type} @{verbatim ","} @{text logic} @{verbatim ")"} \\
2.14 & @{text "|"} & @{verbatim SORT_CONSTRAINT} @{verbatim "("} @{text type} @{verbatim ")"} \\
2.15 + & @{text "|"} & @{verbatim TERM} @{text logic} \\
2.16 & @{text "|"} & @{verbatim PROP} @{text aprop} \\\\
2.17
2.18 - @{syntax_def (inner) aprop} & = & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
2.19 + @{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
2.20 + & @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
2.21 + & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
2.22 & @{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)"} \\\\
2.23
2.24 @{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
2.25 & @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
2.26 & @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
2.27 + & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
2.28 & @{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)"} \\
2.29 & @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
2.30 & @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
2.31 - & @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
2.32 & @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
2.33
2.34 @{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\
2.35 @@ -847,7 +851,7 @@
2.36 Priority information attached to chain productions is ignored; only
2.37 the dummy value @{text "-1"} is displayed.
2.38
2.39 - \item @{text "print_modes"} lists the alternative print modes
2.40 + \item @{text "print modes"} lists the alternative print modes
2.41 provided by this grammar; see \secref{sec:print-modes}.
2.42
2.43 \item @{text "parse_rules"} and @{text "print_rules"} relate to
3.1 --- a/doc-src/IsarRef/Thy/Proof.thy Wed Nov 19 18:15:31 2008 +0100
3.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Thu Nov 20 00:03:47 2008 +0100
3.3 @@ -381,7 +381,7 @@
3.4
3.5 Goals may consist of multiple statements, resulting in a list of
3.6 facts eventually. A pending multi-goal is internally represented as
3.7 - a meta-level conjunction (printed as @{text "&&"}), which is usually
3.8 + a meta-level conjunction (@{text "&&&"}), which is usually
3.9 split into the corresponding number of sub-goals prior to an initial
3.10 method application, via @{command_ref "proof"}
3.11 (\secref{sec:proof-steps}) or @{command_ref "apply"}
4.1 --- a/src/FOL/FOL.thy Wed Nov 19 18:15:31 2008 +0100
4.2 +++ b/src/FOL/FOL.thy Thu Nov 20 00:03:47 2008 +0100
4.3 @@ -346,9 +346,7 @@
4.4 lemma induct_equal_eq: "(x == y) == Trueprop(induct_equal(x, y))"
4.5 unfolding atomize_eq induct_equal_def .
4.6
4.7 -lemma induct_conj_eq:
4.8 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
4.9 - shows "(A && B) == Trueprop(induct_conj(A, B))"
4.10 +lemma induct_conj_eq: "(A &&& B) == Trueprop(induct_conj(A, B))"
4.11 unfolding atomize_conj induct_conj_def .
4.12
4.13 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
5.1 --- a/src/FOL/IFOL.thy Wed Nov 19 18:15:31 2008 +0100
5.2 +++ b/src/FOL/IFOL.thy Thu Nov 20 00:03:47 2008 +0100
5.3 @@ -698,11 +698,9 @@
5.4 then show "A == B" by (rule iff_reflection)
5.5 qed
5.6
5.7 -lemma atomize_conj [atomize]:
5.8 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
5.9 - shows "(A && B) == Trueprop (A & B)"
5.10 +lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
5.11 proof
5.12 - assume conj: "A && B"
5.13 + assume conj: "A &&& B"
5.14 show "A & B"
5.15 proof (rule conjI)
5.16 from conj show A by (rule conjunctionD1)
5.17 @@ -710,7 +708,7 @@
5.18 qed
5.19 next
5.20 assume conj: "A & B"
5.21 - show "A && B"
5.22 + show "A &&& B"
5.23 proof -
5.24 from conj show A ..
5.25 from conj show B ..
6.1 --- a/src/HOL/Code_Setup.thy Wed Nov 19 18:15:31 2008 +0100
6.2 +++ b/src/HOL/Code_Setup.thy Thu Nov 20 00:03:47 2008 +0100
6.3 @@ -78,9 +78,8 @@
6.4 using assms by simp_all
6.5
6.6 lemma If_case_cert:
6.7 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
6.8 assumes "CASE \<equiv> (\<lambda>b. If b f g)"
6.9 - shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
6.10 + shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
6.11 using assms by simp_all
6.12
6.13 setup {*
7.1 --- a/src/HOL/Groebner_Basis.thy Wed Nov 19 18:15:31 2008 +0100
7.2 +++ b/src/HOL/Groebner_Basis.thy Thu Nov 20 00:03:47 2008 +0100
7.3 @@ -64,10 +64,8 @@
7.4 subsubsection {* Declaring the abstract theory *}
7.5
7.6 lemma semiring_ops:
7.7 - fixes meta_term :: "'a => prop" ("TERM _")
7.8 shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)"
7.9 - and "TERM r0" and "TERM r1"
7.10 - by rule+
7.11 + and "TERM r0" and "TERM r1" .
7.12
7.13 lemma semiring_rules:
7.14 "add (mul a m) (mul b m) = mul (add a b) m"
7.15 @@ -226,9 +224,7 @@
7.16 and sub_add: "sub x y = add x (neg y)"
7.17 begin
7.18
7.19 -lemma ring_ops:
7.20 - fixes meta_term :: "'a => prop" ("TERM _")
7.21 - shows "TERM (sub x y)" and "TERM (neg x)" .
7.22 +lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" .
7.23
7.24 lemmas ring_rules = neg_mul sub_add
7.25
8.1 --- a/src/HOL/HOL.thy Wed Nov 19 18:15:31 2008 +0100
8.2 +++ b/src/HOL/HOL.thy Thu Nov 20 00:03:47 2008 +0100
8.3 @@ -845,11 +845,9 @@
8.4 then show "x == y" by (rule eq_reflection)
8.5 qed
8.6
8.7 -lemma atomize_conj [atomize]:
8.8 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
8.9 - shows "(A && B) == Trueprop (A & B)"
8.10 +lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
8.11 proof
8.12 - assume conj: "A && B"
8.13 + assume conj: "A &&& B"
8.14 show "A & B"
8.15 proof (rule conjI)
8.16 from conj show A by (rule conjunctionD1)
8.17 @@ -857,7 +855,7 @@
8.18 qed
8.19 next
8.20 assume conj: "A & B"
8.21 - show "A && B"
8.22 + show "A &&& B"
8.23 proof -
8.24 from conj show A ..
8.25 from conj show B ..
8.26 @@ -1511,9 +1509,7 @@
8.27 lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
8.28 by (unfold atomize_eq induct_equal_def)
8.29
8.30 -lemma induct_conj_eq:
8.31 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
8.32 - shows "(A && B) == Trueprop (induct_conj A B)"
8.33 +lemma induct_conj_eq: "(A &&& B) == Trueprop (induct_conj A B)"
8.34 by (unfold atomize_conj induct_conj_def)
8.35
8.36 lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
9.1 --- a/src/HOL/Library/Coinductive_List.thy Wed Nov 19 18:15:31 2008 +0100
9.2 +++ b/src/HOL/Library/Coinductive_List.thy Thu Nov 20 00:03:47 2008 +0100
9.3 @@ -216,9 +216,8 @@
9.4 CONS_type Abs_llist_inverse Rep_llist Rep_llist_inverse inj_Leaf)
9.5
9.6 lemma llist_case_cert:
9.7 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
9.8 assumes "CASE \<equiv> llist_case c d"
9.9 - shows "(CASE LNil \<equiv> c) && (CASE (LCons M N) \<equiv> d M N)"
9.10 + shows "(CASE LNil \<equiv> c) &&& (CASE (LCons M N) \<equiv> d M N)"
9.11 using assms by simp_all
9.12
9.13 setup {*
10.1 --- a/src/HOL/Library/Dense_Linear_Order.thy Wed Nov 19 18:15:31 2008 +0100
10.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy Thu Nov 20 00:03:47 2008 +0100
10.3 @@ -268,7 +268,6 @@
10.4
10.5 lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
10.6 lemma atoms:
10.7 - fixes meta_term :: "'a => prop" ("TERM _")
10.8 shows "TERM (less :: 'a \<Rightarrow> _)"
10.9 and "TERM (less_eq :: 'a \<Rightarrow> _)"
10.10 and "TERM (op = :: 'a \<Rightarrow> _)" .
10.11 @@ -505,7 +504,6 @@
10.12 lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
10.13 by (rule constr_dense_linear_order_axioms)
10.14 lemma atoms:
10.15 - fixes meta_term :: "'a => prop" ("TERM _")
10.16 shows "TERM (less :: 'a \<Rightarrow> _)"
10.17 and "TERM (less_eq :: 'a \<Rightarrow> _)"
10.18 and "TERM (op = :: 'a \<Rightarrow> _)" .
11.1 --- a/src/Pure/Isar/proof_context.ML Wed Nov 19 18:15:31 2008 +0100
11.2 +++ b/src/Pure/Isar/proof_context.ML Thu Nov 20 00:03:47 2008 +0100
11.3 @@ -1060,10 +1060,14 @@
11.4
11.5 val _ = Context.>> (Context.map_theory
11.6 (Sign.add_syntax
11.7 - [("_context_const", "id => 'a", Delimfix "CONST _"),
11.8 - ("_context_const", "longid => 'a", Delimfix "CONST _"),
11.9 - ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
11.10 - ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
11.11 + [("_context_const", "id => logic", Delimfix "CONST _"),
11.12 + ("_context_const", "id => aprop", Delimfix "CONST _"),
11.13 + ("_context_const", "longid => logic", Delimfix "CONST _"),
11.14 + ("_context_const", "longid => aprop", Delimfix "CONST _"),
11.15 + ("_context_xconst", "id => logic", Delimfix "XCONST _"),
11.16 + ("_context_xconst", "id => aprop", Delimfix "XCONST _"),
11.17 + ("_context_xconst", "longid => logic", Delimfix "XCONST _"),
11.18 + ("_context_xconst", "longid => aprop", Delimfix "XCONST _")] #>
11.19 Sign.add_advanced_trfuns
11.20 ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
11.21
12.1 --- a/src/Pure/Pure.thy Wed Nov 19 18:15:31 2008 +0100
12.2 +++ b/src/Pure/Pure.thy Thu Nov 20 00:03:47 2008 +0100
12.3 @@ -24,34 +24,22 @@
12.4 "(!!x y. PROP P x y) == (!!y x. PROP P x y)" ..
12.5
12.6
12.7 -subsection {* Embedded terms *}
12.8 -
12.9 -locale meta_term_syntax =
12.10 - fixes meta_term :: "'a => prop" ("TERM _")
12.11 -
12.12 -lemmas [intro?] = termI
12.13 -
12.14 -
12.15 subsection {* Meta-level conjunction *}
12.16
12.17 -locale meta_conjunction_syntax =
12.18 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
12.19 -
12.20 lemma all_conjunction:
12.21 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
12.22 - shows "(!!x. PROP A x && PROP B x) == ((!!x. PROP A x) && (!!x. PROP B x))"
12.23 + "(!!x. PROP A x &&& PROP B x) == ((!!x. PROP A x) &&& (!!x. PROP B x))"
12.24 proof
12.25 - assume conj: "!!x. PROP A x && PROP B x"
12.26 - show "(!!x. PROP A x) && (!!x. PROP B x)"
12.27 + assume conj: "!!x. PROP A x &&& PROP B x"
12.28 + show "(!!x. PROP A x) &&& (!!x. PROP B x)"
12.29 proof -
12.30 fix x
12.31 from conj show "PROP A x" by (rule conjunctionD1)
12.32 from conj show "PROP B x" by (rule conjunctionD2)
12.33 qed
12.34 next
12.35 - assume conj: "(!!x. PROP A x) && (!!x. PROP B x)"
12.36 + assume conj: "(!!x. PROP A x) &&& (!!x. PROP B x)"
12.37 fix x
12.38 - show "PROP A x && PROP B x"
12.39 + show "PROP A x &&& PROP B x"
12.40 proof -
12.41 show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format])
12.42 show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format])
12.43 @@ -59,20 +47,19 @@
12.44 qed
12.45
12.46 lemma imp_conjunction:
12.47 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
12.48 - shows "(PROP A ==> PROP B && PROP C) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
12.49 + "(PROP A ==> PROP B &&& PROP C) == (PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
12.50 proof
12.51 - assume conj: "PROP A ==> PROP B && PROP C"
12.52 - show "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
12.53 + assume conj: "PROP A ==> PROP B &&& PROP C"
12.54 + show "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
12.55 proof -
12.56 assume "PROP A"
12.57 from conj [OF `PROP A`] show "PROP B" by (rule conjunctionD1)
12.58 from conj [OF `PROP A`] show "PROP C" by (rule conjunctionD2)
12.59 qed
12.60 next
12.61 - assume conj: "(PROP A ==> PROP B) && (PROP A ==> PROP C)"
12.62 + assume conj: "(PROP A ==> PROP B) &&& (PROP A ==> PROP C)"
12.63 assume "PROP A"
12.64 - show "PROP B && PROP C"
12.65 + show "PROP B &&& PROP C"
12.66 proof -
12.67 from `PROP A` show "PROP B" by (rule conj [THEN conjunctionD1])
12.68 from `PROP A` show "PROP C" by (rule conj [THEN conjunctionD2])
12.69 @@ -80,18 +67,17 @@
12.70 qed
12.71
12.72 lemma conjunction_imp:
12.73 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
12.74 - shows "(PROP A && PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
12.75 + "(PROP A &&& PROP B ==> PROP C) == (PROP A ==> PROP B ==> PROP C)"
12.76 proof
12.77 - assume r: "PROP A && PROP B ==> PROP C"
12.78 + assume r: "PROP A &&& PROP B ==> PROP C"
12.79 assume ab: "PROP A" "PROP B"
12.80 show "PROP C"
12.81 proof (rule r)
12.82 - from ab show "PROP A && PROP B" .
12.83 + from ab show "PROP A &&& PROP B" .
12.84 qed
12.85 next
12.86 assume r: "PROP A ==> PROP B ==> PROP C"
12.87 - assume conj: "PROP A && PROP B"
12.88 + assume conj: "PROP A &&& PROP B"
12.89 show "PROP C"
12.90 proof (rule r)
12.91 from conj show "PROP A" by (rule conjunctionD1)
13.1 --- a/src/Pure/Syntax/simple_syntax.ML Wed Nov 19 18:15:31 2008 +0100
13.2 +++ b/src/Pure/Syntax/simple_syntax.ML Thu Nov 20 00:03:47 2008 +0100
13.3 @@ -18,7 +18,7 @@
13.4 (* scanning tokens *)
13.5
13.6 val lexicon = Scan.make_lexicon
13.7 - (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&", "CONST"]);
13.8 + (map Symbol.explode ["!!", "%", "(", ")", ".", "::", "==", "==>", "=?=", "=>", "&&&", "CONST"]);
13.9
13.10 fun read scan s =
13.11 (case
13.12 @@ -81,7 +81,7 @@
13.13 | term2
13.14 term2 = term3 == term2
13.15 | term3 =?= term2
13.16 - | term3 && term2
13.17 + | term3 &&& term2
13.18 | term3
13.19 term3 = ident :: typ
13.20 | var :: typ
13.21 @@ -111,7 +111,7 @@
13.22 term2 env T) x
13.23 and term2 env T x =
13.24 (equal env "==" || equal env "=?=" ||
13.25 - term3 env propT -- ($$ "&&" |-- term2 env propT) >> Logic.mk_conjunction ||
13.26 + term3 env propT -- ($$ "&&&" |-- term2 env propT) >> Logic.mk_conjunction ||
13.27 term3 env T) x
13.28 and equal env eq x =
13.29 (term3 env dummyT -- ($$ eq |-- term2 env dummyT) >> (fn (t, u) =>
14.1 --- a/src/Pure/Syntax/syn_ext.ML Wed Nov 19 18:15:31 2008 +0100
14.2 +++ b/src/Pure/Syntax/syn_ext.ML Thu Nov 20 00:03:47 2008 +0100
14.3 @@ -10,6 +10,7 @@
14.4 val dddot_indexname: indexname
14.5 val constrainC: string
14.6 val typeT: typ
14.7 + val spropT: typ
14.8 val max_pri: int
14.9 val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
14.10 val mk_trfun: string * 'a -> string * ('a * stamp)
15.1 --- a/src/Pure/Syntax/syn_trans.ML Wed Nov 19 18:15:31 2008 +0100
15.2 +++ b/src/Pure/Syntax/syn_trans.ML Thu Nov 20 00:03:47 2008 +0100
15.3 @@ -473,9 +473,8 @@
15.4 ("_bigimpl", bigimpl_ast_tr), ("_indexdefault", indexdefault_ast_tr),
15.5 ("_indexnum", indexnum_ast_tr), ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
15.6 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
15.7 - ("_sort_constraint", sort_constraint_tr), ("\\<^fixed>meta_conjunction", conjunction_tr),
15.8 - ("_TYPE", type_tr), ("\\<^fixed>meta_term", term_tr), ("_DDDOT", dddot_tr),
15.9 - ("_index", index_tr)],
15.10 + ("_sort_constraint", sort_constraint_tr), ("_TYPE", type_tr),
15.11 + ("_DDDOT", dddot_tr), ("_index", index_tr)],
15.12 ([]: (string * (term list -> term)) list),
15.13 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
15.14 ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
16.1 --- a/src/Pure/conjunction.ML Wed Nov 19 18:15:31 2008 +0100
16.2 +++ b/src/Pure/conjunction.ML Thu Nov 20 00:03:47 2008 +0100
16.3 @@ -67,7 +67,7 @@
16.4 val B = read_prop "B" and vB = read_prop "?B";
16.5 val C = read_prop "C";
16.6 val ABC = read_prop "A ==> B ==> C";
16.7 -val A_B = read_prop "A && B";
16.8 +val A_B = read_prop "A &&& B";
16.9
16.10 val conjunction_def =
16.11 Thm.unvarify (Thm.axiom (Context.the_theory (Context.the_thread_data ())) "Pure.conjunction_def");
16.12 @@ -135,7 +135,7 @@
16.13 in
16.14
16.15 (*
16.16 - A1 && ... && An ==> B
16.17 + A1 &&& ... &&& An ==> B
16.18 -----------------------
16.19 A1 ==> ... ==> An ==> B
16.20 *)
16.21 @@ -155,7 +155,7 @@
16.22 (*
16.23 A1 ==> ... ==> An ==> B
16.24 -----------------------
16.25 - A1 && ... && An ==> B
16.26 + A1 &&& ... &&& An ==> B
16.27 *)
16.28 fun uncurry_balanced n th =
16.29 if n < 2 then th
17.1 --- a/src/Pure/logic.ML Wed Nov 19 18:15:31 2008 +0100
17.2 +++ b/src/Pure/logic.ML Thu Nov 20 00:03:47 2008 +0100
17.3 @@ -162,33 +162,33 @@
17.4 val conjunction = Const ("Pure.conjunction", propT --> propT --> propT);
17.5
17.6
17.7 -(*A && B*)
17.8 +(*A &&& B*)
17.9 fun mk_conjunction (A, B) = conjunction $ A $ B;
17.10
17.11 -(*A && B && C -- improper*)
17.12 +(*A &&& B &&& C -- improper*)
17.13 fun mk_conjunction_list [] = true_prop
17.14 | mk_conjunction_list ts = foldr1 mk_conjunction ts;
17.15
17.16 -(*(A && B) && (C && D) -- balanced*)
17.17 +(*(A &&& B) &&& (C &&& D) -- balanced*)
17.18 fun mk_conjunction_balanced [] = true_prop
17.19 | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
17.20
17.21
17.22 -(*A && B*)
17.23 +(*A &&& B*)
17.24 fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B)
17.25 | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
17.26
17.27 -(*A && B && C -- improper*)
17.28 +(*A &&& B &&& C -- improper*)
17.29 fun dest_conjunction_list t =
17.30 (case try dest_conjunction t of
17.31 NONE => [t]
17.32 | SOME (A, B) => A :: dest_conjunction_list B);
17.33
17.34 -(*(A && B) && (C && D) -- balanced*)
17.35 +(*(A &&& B) &&& (C &&& D) -- balanced*)
17.36 fun dest_conjunction_balanced 0 _ = []
17.37 | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
17.38
17.39 -(*((A && B) && C) && D && E -- flat*)
17.40 +(*((A &&& B) &&& C) &&& D &&& E -- flat*)
17.41 fun dest_conjunctions t =
17.42 (case try dest_conjunction t of
17.43 NONE => [t]
18.1 --- a/src/Pure/pure_thy.ML Wed Nov 19 18:15:31 2008 +0100
18.2 +++ b/src/Pure/pure_thy.ML Thu Nov 20 00:03:47 2008 +0100
18.3 @@ -244,6 +244,9 @@
18.4 val term = SimpleSyntax.read_term;
18.5 val prop = SimpleSyntax.read_prop;
18.6
18.7 +val typeT = Syntax.typeT;
18.8 +val spropT = Syntax.spropT;
18.9 +
18.10
18.11 (* application syntax variants *)
18.12
18.13 @@ -301,6 +304,7 @@
18.14 ("", typ "idt => pttrn", Delimfix "_"),
18.15 ("", typ "pttrn => pttrns", Delimfix "_"),
18.16 ("_pttrns", typ "pttrn => pttrns => pttrns", Mixfix ("_/ _", [1, 0], 0)),
18.17 + ("", typ "aprop => aprop", Delimfix "'(_')"),
18.18 ("", typ "id => aprop", Delimfix "_"),
18.19 ("", typ "longid => aprop", Delimfix "_"),
18.20 ("", typ "var => aprop", Delimfix "_"),
18.21 @@ -324,13 +328,16 @@
18.22 ("_struct", typ "index => logic", Mixfix ("\\<struct>_", [1000], 1000)),
18.23 ("==>", typ "prop => prop => prop", Delimfix "op ==>"),
18.24 (Term.dummy_patternN, typ "aprop", Delimfix "'_"),
18.25 - ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))")]
18.26 + ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
18.27 + ("Pure.term", typ "logic => prop", Delimfix "TERM _"),
18.28 + ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&&", 2))]
18.29 #> Sign.add_syntax_i applC_syntax
18.30 #> Sign.add_modesyntax_i (Symbol.xsymbolsN, true)
18.31 [("fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
18.32 ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
18.33 ("_ofsort", typ "tid => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
18.34 - ("_constrain", typ "'a => type => 'a", Mixfix ("_\\<Colon>_", [4, 0], 3)),
18.35 + ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
18.36 + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\<Colon>_", [4, 0], 3)),
18.37 ("_idtyp", typ "id => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
18.38 ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
18.39 ("_type_constraint_", typ "'a", NoSyn),
18.40 @@ -342,9 +349,7 @@
18.41 ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
18.42 ("_DDDOT", typ "logic", Delimfix "\\<dots>")]
18.43 #> Sign.add_modesyntax_i ("", false)
18.44 - [("prop", typ "prop => prop", Mixfix ("_", [0], 0)),
18.45 - ("Pure.term", typ "'a => prop", Delimfix "TERM _"),
18.46 - ("Pure.conjunction", typ "prop => prop => prop", InfixrName ("&&", 2))]
18.47 + [("prop", typ "prop => prop", Mixfix ("_", [0], 0))]
18.48 #> Sign.add_modesyntax_i ("HTML", false)
18.49 [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
18.50 #> Sign.add_consts_i
18.51 @@ -372,7 +377,7 @@
18.52 ("sort_constraint_def",
18.53 prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
18.54 \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
18.55 - ("conjunction_def", prop "(A && B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
18.56 + ("conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
18.57 #> Sign.hide_const false "Pure.term"
18.58 #> Sign.hide_const false "Pure.sort_constraint"
18.59 #> Sign.hide_const false "Pure.conjunction"