# HG changeset patch # User wenzelm # Date 1227135827 -3600 # Node ID 5e009a80fe6d423cb48177bd81e6a40247d9496b # Parent 5d21a3e7303cde2fc5272021e37eae22faa913aa Pure syntax: more coherent treatment of aprop, permanent TERM and &&&; diff -r 5d21a3e7303c -r 5e009a80fe6d NEWS --- 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 diff -r 5d21a3e7303c -r 5e009a80fe6d doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 "\"} @{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 "\"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ & @{text "|"} & @{verbatim "[|"} @{text prop} @{verbatim ";"} @{text "\"} @{verbatim ";"} @{text prop} @{verbatim "|]"} @{verbatim "==>"} @{text "prop\<^sup>(\<^sup>1\<^sup>)"} & @{text "(1)"} \\ @@ -493,18 +494,21 @@ & @{text "|"} & @{text "\"} @{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>) \ 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>) \ 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 \} @{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 diff -r 5d21a3e7303c -r 5e009a80fe6d doc-src/IsarRef/Thy/Proof.thy --- 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"} diff -r 5d21a3e7303c -r 5e009a80fe6d src/FOL/FOL.thy --- 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 diff -r 5d21a3e7303c -r 5e009a80fe6d src/FOL/IFOL.thy --- 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 .. diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/Code_Setup.thy --- 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 \ (\b. If b f g)" - shows "(CASE True \ f) && (CASE False \ g)" + shows "(CASE True \ f) &&& (CASE False \ g)" using assms by simp_all setup {* diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/Groebner_Basis.thy --- 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 diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/HOL.thy --- 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 diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/Library/Coinductive_List.thy --- 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 \ llist_case c d" - shows "(CASE LNil \ c) && (CASE (LCons M N) \ d M N)" + shows "(CASE LNil \ c) &&& (CASE (LCons M N) \ d M N)" using assms by simp_all setup {* diff -r 5d21a3e7303c -r 5e009a80fe6d src/HOL/Library/Dense_Linear_Order.thy --- 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 \) (op <)" by (rule dense_linear_order_axioms) lemma atoms: - fixes meta_term :: "'a => prop" ("TERM _") shows "TERM (less :: 'a \ _)" and "TERM (less_eq :: 'a \ _)" and "TERM (op = :: 'a \ _)" . @@ -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 \ _)" and "TERM (less_eq :: 'a \ _)" and "TERM (op = :: 'a \ _)" . diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Isar/proof_context.ML --- 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)], [], [], []))); diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Pure.thy --- 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) diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Syntax/simple_syntax.ML --- 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) => diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Syntax/syn_ext.ML --- 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) diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/Syntax/syn_trans.ML --- 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'), diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/conjunction.ML --- 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 diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/logic.ML --- 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] diff -r 5d21a3e7303c -r 5e009a80fe6d src/Pure/pure_thy.ML --- 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 ("\\_", [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 ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), - ("_constrain", typ "'a => type => 'a", Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), ("_idtyp", typ "id => type => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_type_constraint_", typ "'a", NoSyn), @@ -342,9 +349,7 @@ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] #> 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\\_./ _)", [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"