Up to index of Isabelle/HOL/HOL-Complex/Import
theory MakeEqual(* Title: HOL/Import/MakeEqual.thy ID: $Id: MakeEqual.thy,v 1.3 2005/06/17 14:13:07 haftmann Exp $ Author: Sebastian Skalberg (TU Muenchen) *) theory MakeEqual imports Main uses "shuffler.ML" begin setup Shuffler.setup lemma conj_norm [shuffle_rule]: "(A & B ==> PROP C) == ([| A ; B |] ==> PROP C)" proof assume "A & B ==> PROP C" A B thus "PROP C" by auto next assume "[| A; B |] ==> PROP C" "A & B" thus "PROP C" by auto qed lemma imp_norm [shuffle_rule]: "(Trueprop (A --> B)) == (A ==> B)" proof assume "A --> B" A thus B .. next assume "A ==> B" thus "A --> B" by auto qed lemma all_norm [shuffle_rule]: "(Trueprop (ALL x. P x)) == (!!x. P x)" proof fix x assume "ALL x. P x" thus "P x" .. next assume "!!x. P x" thus "ALL x. P x" .. qed lemma ex_norm [shuffle_rule]: "(EX x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)" proof fix x assume ex: "EX x. P x ==> PROP Q" assume "P x" hence "EX x. P x" .. with ex show "PROP Q" . next assume allx: "!!x. P x ==> PROP Q" assume "EX x. P x" hence p: "P (SOME x. P x)" .. from allx have "P (SOME x. P x) ==> PROP Q" . with p show "PROP Q" by auto qed lemma eq_norm [shuffle_rule]: "Trueprop (t = u) == (t == u)" proof assume "t = u" thus "t == u" by simp next assume "t == u" thus "t = u" by simp qed end
lemma conj_norm:
(A ∧ B ==> PROP C) == ([| A; B |] ==> PROP C)
lemma imp_norm:
A --> B == (A ==> B)
lemma all_norm:
∀x. P x == (!!x. P x)
lemma ex_norm:
(∃x. P x ==> PROP Q) == (!!x. P x ==> PROP Q)
lemma eq_norm:
t = u == t == u