simplified Pure conjunction, based on actual const;
authorwenzelm
Wed Feb 22 22:18:39 2006 +0100 (2006-02-22)
changeset 1912559b26248547b
parent 19124 d9ac560a7bc8
child 19126 a3cf88213ea5
simplified Pure conjunction, based on actual const;
src/Pure/logic.ML
src/Pure/pure_thy.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/logic.ML	Wed Feb 22 22:18:38 2006 +0100
     1.2 +++ b/src/Pure/logic.ML	Wed Feb 22 22:18:39 2006 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    val strip_prems: int * term list * term -> term list * term
     1.5    val count_prems: term * int -> int
     1.6    val nth_prem: int * term -> term
     1.7 +  val conjunction: term
     1.8    val mk_conjunction: term * term -> term
     1.9    val mk_conjunction_list: term list -> term
    1.10    val mk_conjunction_list2: term list list -> term
    1.11 @@ -144,10 +145,10 @@
    1.12  
    1.13  (** conjunction **)
    1.14  
    1.15 +val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
    1.16 +
    1.17  (*A && B*)
    1.18 -fun mk_conjunction (t, u) =
    1.19 -  Term.list_all ([("X", propT)],
    1.20 -    mk_implies (list_implies (map (Term.incr_boundvars 1) [t, u], Bound 0), Bound 0));
    1.21 +fun mk_conjunction (A, B) = conjunction $ A $ B;
    1.22  
    1.23  (*A && B && C -- improper*)
    1.24  fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
    1.25 @@ -158,12 +159,7 @@
    1.26    mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
    1.27  
    1.28  (*A && B*)
    1.29 -fun dest_conjunction
    1.30 -      (t as Const ("all", _) $ Abs (_, _,
    1.31 -        Const ("==>", _) $ (Const ("==>", _) $ A $ (Const ("==>", _) $ B $ Bound 0)) $ Bound 0)) =
    1.32 -      if Term.loose_bvar1 (A, 0) orelse Term.loose_bvar1 (B, 0)
    1.33 -      then raise TERM ("dest_conjunction", [t])
    1.34 -      else (Term.incr_boundvars ~1 A, Term.incr_boundvars ~1 B)
    1.35 +fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
    1.36    | dest_conjunction t = raise TERM ("dest_conjunction", [t]);
    1.37  
    1.38  (*((A && B) && C) && D && E -- flat*)
     2.1 --- a/src/Pure/pure_thy.ML	Wed Feb 22 22:18:38 2006 +0100
     2.2 +++ b/src/Pure/pure_thy.ML	Wed Feb 22 22:18:39 2006 +0100
     2.3 @@ -23,6 +23,7 @@
     2.4      sig
     2.5        val thy: theory
     2.6        val prop_def: thm
     2.7 +      val conjunction_def: thm
     2.8      end
     2.9  end;
    2.10  
    2.11 @@ -609,7 +610,7 @@
    2.12      ("_DDDOT",   "logic",                 Delimfix "\\<dots>")]
    2.13    |> Theory.add_modesyntax ("", false)
    2.14     [("prop", "prop => prop", Mixfix ("_", [0], 0)),
    2.15 -    ("_meta_conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
    2.16 +    ("ProtoPure.conjunction", "prop => prop => prop", InfixrName ("&&", 2))]
    2.17    |> Theory.add_modesyntax ("HTML", false)
    2.18     [("_lambda",  "[pttrns, 'a] => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
    2.19    |> Theory.add_consts
    2.20 @@ -628,8 +629,13 @@
    2.21    |> Theory.add_trfuns Syntax.pure_trfuns
    2.22    |> Theory.add_trfunsT Syntax.pure_trfunsT
    2.23    |> Sign.local_path
    2.24 -  |> (add_defs_i false o map Thm.no_attributes)
    2.25 -       [("prop_def", Logic.mk_equals (Logic.protect A, A))] |> snd
    2.26 +  |> Theory.add_consts
    2.27 +   [("conjunction", "prop => prop => prop", NoSyn)]
    2.28 +  |> (add_defs false o map Thm.no_attributes)
    2.29 +   [("prop_def", "prop(A) == A"),
    2.30 +    ("conjunction_def",
    2.31 +      "conjunction(A, B) == (!!C. (PROP A ==> PROP B ==> PROP C) ==> PROP C)")] |> snd
    2.32 +  |> Sign.hide_consts false ["conjunction"]
    2.33    |> add_thmss [(("nothing", []), [])] |> snd
    2.34    |> Theory.add_axioms_i Proofterm.equality_axms
    2.35    |> Theory.end_theory;
    2.36 @@ -638,6 +644,7 @@
    2.37  struct
    2.38    val thy = proto_pure;
    2.39    val prop_def = get_axiom thy "prop_def";
    2.40 +  val conjunction_def = get_axiom thy "conjunction_def";
    2.41  end;
    2.42  
    2.43  end;
     3.1 --- a/src/Pure/tactic.ML	Wed Feb 22 22:18:38 2006 +0100
     3.2 +++ b/src/Pure/tactic.ML	Wed Feb 22 22:18:39 2006 +0100
     3.3 @@ -642,8 +642,7 @@
     3.4  (* meta-level conjunction *)
     3.5  
     3.6  val conj_tac = SUBGOAL (fn (goal, i) =>
     3.7 -  if can Logic.dest_conjunction goal then
     3.8 -    (fn st => compose_tac (false, Drule.incr_indexes st Drule.conj_intr_thm, 2) i st)
     3.9 +  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
    3.10    else no_tac);
    3.11  
    3.12  val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;