<commit_before>(*  Title:      HOL/simpdata.ML
    ID:         $Id$
    Author:     <NAME>
    Copyright   1991  University of Cambridge

Instantiation of the generic simplifier for HOL.
*)

section "Simplifier";

val [prem] = goal (the_context ()) "x==y ==> x=y";
by (rewtac prem);
by (rtac refl 1);
qed "meta_eq_to_obj_eq";

Goal "(%s. f s) = f";
br refl 1;
qed "eta_contract_eq";

local

  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);

in

(*Make meta-equalities.  The operator below is Trueprop*)

fun mk_meta_eq r = r RS eq_reflection;
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;

val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);

fun mk_eq th = case concl_of th of
        Const("==",_)$_$_       => th
    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    |   _                       => th RS Eq_TrueI;
(* last 2 lines requires all formulae to be of the from Trueprop(.) *)

fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);

(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong rl =
  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
  handle THM _ =>
  error("Premises and conclusion of congruence rules must be =-equalities");

val not_not = prover "(~ ~ P) = P";

val simp_thms = [not_not] @ map prover
 [ "(x=x) = True",
   "(~True) = False", "(~False) = True",
   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
   "(True --> P) = P", "(False --> P) = True",
   "(P --> True) = True", "(P --> P) = True",
   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
   "(P & True) = P", "(True & P) = P",
   "(P & False) = False", "(False & P) = False",
   "(P & P) = P", "(P & (P & Q)) = (P & Q)",
   "(P & ~P) = False",    "(~P & P) = False",
   "(P | True) = True", "(True | P) = True",
   "(P | False) = P", "(False | P) = P",
   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
   "(P | ~P) = True",    "(~P | P) = True",
   "((~P) = (~Q)) = (P=Q)",
   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
(*two needed for the one-point-rule quantifier simplification procs*)
   "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
   "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)

val imp_cong = impI RSN
    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
        (fn _=> [(Blast_tac 1)]) RS mp RS mp);

(*Miniscoping: pushing in existential quantifiers*)
val ex_simps = map prover
                ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
                 "(EX x. P & Q x)   = (P & (EX x. Q x))",
                 "(EX x. P x | Q)   = ((EX x. P x) | Q)",
                 "(EX x. P | Q x)   = (P | (EX x. Q x))",
                 "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
                 "(EX x. P --> Q x) = (P --> (EX x. Q x))"];

(*Miniscoping: pushing in universal quantifiers*)
val all_simps = map prover
                ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
                 "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
                 "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
                 "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
                 "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
                 "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];


(* elimination of existential quantifiers in assumptions *)

val ex_all_equiv =
  let val lemma1 = prove_goal (the_context ())
        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
        (fn prems => [resolve_tac prems 1, etac exI 1]);
      val lemma2 = prove_goalw (the_context ()) [Ex_def]
        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
        (fn prems => [(REPEAT(resolve_tac prems 1))])
  in equal_intr lemma1 lemma2 end;

end;

bind_thms ("ex_simps", ex_simps);
bind_thms ("all_simps", all_simps);
bind_thm ("not_not", not_not);

(* Elimination of True from asumptions: *)

val True_implies_equals = prove_goal (the_context ())<commit_msg>imp_cong bound at thm level.<commit_after>(*  Title:      HOL/simpdata.ML
    ID:         $Id$
    Author:     <NAME>
    Copyright   1991  University of Cambridge

Instantiation of the generic simplifier for HOL.
*)

section "Simplifier";

val [prem] = goal (the_context ()) "x==y ==> x=y";
by (rewtac prem);
by (rtac refl 1);
qed "meta_eq_to_obj_eq";

Goal "(%s. f s) = f";
br refl 1;
qed "eta_contract_eq";

local

  fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);

in

(*Make meta-equalities.  The operator below is Trueprop*)

fun mk_meta_eq r = r RS eq_reflection;
fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;

val Eq_TrueI  = mk_meta_eq(prover  "P --> (P = True)"  RS mp);
val Eq_FalseI = mk_meta_eq(prover "~P --> (P = False)" RS mp);

fun mk_eq th = case concl_of th of
        Const("==",_)$_$_       => th
    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
    |   _                       => th RS Eq_TrueI;
(* last 2 lines requires all formulae to be of the from Trueprop(.) *)

fun mk_eq_True r = Some(r RS meta_eq_to_obj_eq RS Eq_TrueI);

(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong rl =
  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
  handle THM _ =>
  error("Premises and conclusion of congruence rules must be =-equalities");

val not_not = prover "(~ ~ P) = P";

val simp_thms = [not_not] @ map prover
 [ "(x=x) = True",
   "(~True) = False", "(~False) = True",
   "(~P) ~= P", "P ~= (~P)", "(P ~= Q) = (P = (~Q))",
   "(True=P) = P", "(P=True) = P", "(False=P) = (~P)", "(P=False) = (~P)",
   "(True --> P) = P", "(False --> P) = True",
   "(P --> True) = True", "(P --> P) = True",
   "(P --> False) = (~P)", "(P --> ~P) = (~P)",
   "(P & True) = P", "(True & P) = P",
   "(P & False) = False", "(False & P) = False",
   "(P & P) = P", "(P & (P & Q)) = (P & Q)",
   "(P & ~P) = False",    "(~P & P) = False",
   "(P | True) = True", "(True | P) = True",
   "(P | False) = P", "(False | P) = P",
   "(P | P) = P", "(P | (P | Q)) = (P | Q)",
   "(P | ~P) = True",    "(~P | P) = True",
   "((~P) = (~Q)) = (P=Q)",
   "(!x. P) = P", "(? x. P) = P", "? x. x=t", "? x. t=x",
(*two needed for the one-point-rule quantifier simplification procs*)
   "(? x. x=t & P(x)) = P(t)",          (*essential for termination!!*)
   "(! x. t=x --> P(x)) = P(t)" ];      (*covers a stray case*)

val imp_cong = standard(impI RSN
    (2, prove_goal (the_context ()) "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"
        (fn _=> [(Blast_tac 1)]) RS mp RS mp));

(*Miniscoping: pushing in existential quantifiers*)
val ex_simps = map prover
                ["(EX x. P x & Q)   = ((EX x. P x) & Q)",
                 "(EX x. P & Q x)   = (P & (EX x. Q x))",
                 "(EX x. P x | Q)   = ((EX x. P x) | Q)",
                 "(EX x. P | Q x)   = (P | (EX x. Q x))",
                 "(EX x. P x --> Q) = ((ALL x. P x) --> Q)",
                 "(EX x. P --> Q x) = (P --> (EX x. Q x))"];

(*Miniscoping: pushing in universal quantifiers*)
val all_simps = map prover
                ["(ALL x. P x & Q)   = ((ALL x. P x) & Q)",
                 "(ALL x. P & Q x)   = (P & (ALL x. Q x))",
                 "(ALL x. P x | Q)   = ((ALL x. P x) | Q)",
                 "(ALL x. P | Q x)   = (P | (ALL x. Q x))",
                 "(ALL x. P x --> Q) = ((EX x. P x) --> Q)",
                 "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"];


(* elimination of existential quantifiers in assumptions *)

val ex_all_equiv =
  let val lemma1 = prove_goal (the_context ())
        "(? x. P(x) ==> PROP Q) ==> (!!x. P(x) ==> PROP Q)"
        (fn prems => [resolve_tac prems 1, etac exI 1]);
      val lemma2 = prove_goalw (the_context ()) [Ex_def]
        "(!!x. P(x) ==> PROP Q) ==> (? x. P(x) ==> PROP Q)"
        (fn prems => [(REPEAT(resolve_tac prems 1))])
  in equal_intr lemma1 lemma2 end;

end;

bind_thms ("ex_simps", ex_simps);
bind_thms ("all_simps", all_simps);
bind_thm ("not_not", not_not);
bind_thm ("imp_cong", imp_cong);

(* Elimination of True from asumptions: *)

val True_implies_equals = prove_goal (the_context ())
{'fraction_non_alphanumeric': 0.2267230955259976, 'fraction_numerical': 0.004111245465538089, 'mean_word_length': 2.2524577270939834, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 83, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '191499', 'n_tokens_mistral': 3429, 'n_tokens_neox': 3344, 'n_words': 1055}