# HG changeset patch # User wenzelm # Date 1140643119 -3600 # Node ID 59b26248547b80cb46bc66cf5e3dab32731eba35 # Parent d9ac560a7bc80032ff49353dbfa864e6f84e3553 simplified Pure conjunction, based on actual const; diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/logic.ML --- a/src/Pure/logic.ML Wed Feb 22 22:18:38 2006 +0100 +++ b/src/Pure/logic.ML Wed Feb 22 22:18:39 2006 +0100 @@ -22,6 +22,7 @@ val strip_prems: int * term list * term -> term list * term val count_prems: term * int -> int val nth_prem: int * term -> term + val conjunction: term val mk_conjunction: term * term -> term val mk_conjunction_list: term list -> term val mk_conjunction_list2: term list list -> term @@ -144,10 +145,10 @@ (** conjunction **) +val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT); + (*A && B*) -fun mk_conjunction (t, u) = - Term.list_all ([("X", propT)], - mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0)); +fun mk_conjunction (A, B) = conjunction $ A $ B; (*A && B && C -- improper*) fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) @@ -158,12 +159,7 @@ mk_conjunction_list (map mk_conjunction_list (filter_out null tss)); (*A && B*) -fun dest_conjunction - (t as Const ("all", _) $ Abs (_, _, - Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) = - if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0) - then raise TERM ("dest_conjunction", [t]) - else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B) +fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B) | dest_conjunction t = raise TERM ("dest_conjunction", [t]); (*((A && B) && C) && D && E -- flat*) diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Wed Feb 22 22:18:38 2006 +0100 +++ b/src/Pure/pure_thy.ML Wed Feb 22 22:18:39 2006 +0100 @@ -23,6 +23,7 @@ sig val thy: theory val prop_def: thm + val conjunction_def: thm end end; @@ -609,7 +610,7 @@ ("_DDDOT", "logic", Delimfix "\\")] |> Theory.add_modesyntax ("", false) [("prop", "prop => prop", Mixfix ("_", [0], 0)), - ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))] + ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))] |> Theory.add_modesyntax ("HTML", false) [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] |> Theory.add_consts @@ -628,8 +629,13 @@ |> Theory.add_trfuns Syntax.pure_trfuns |> Theory.add_trfunsT Syntax.pure_trfunsT |> Sign.local_path - |> (add_defs_i false o map Thm.no_attributes) - [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd + |> Theory.add_consts + [("conjunction", "prop => prop => prop", NoSyn)] + |> (add_defs false o map Thm.no_attributes) + [("prop_def", "prop(A) == A"), + ("conjunction_def", + "conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] |> snd + |> Sign.hide_consts false ["conjunction"] |> add_thmss [(("nothing", []), [])] |> snd |> Theory.add_axioms_i Proofterm.equality_axms |> Theory.end_theory; @@ -638,6 +644,7 @@ struct val thy = proto_pure; val prop_def = get_axiom thy "prop_def"; + val conjunction_def = get_axiom thy "conjunction_def"; end; end; diff -r d9ac560a7bc8 -r 59b26248547b src/Pure/tactic.ML --- a/src/Pure/tactic.ML Wed Feb 22 22:18:38 2006 +0100 +++ b/src/Pure/tactic.ML Wed Feb 22 22:18:39 2006 +0100 @@ -642,8 +642,7 @@ (* meta-level conjunction *) val conj_tac = SUBGOAL (fn (goal, i) => - if can Logic.dest_conjunction goal then - (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st) + if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i else no_tac); val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;