Quelle Preorder.thy Sprache: Isabelle

(* Author: Florian Haftmann, TU Muenchen *)

section \<open>Preorders with explicit equivalence relation\<close>

theory Preorder
imports Main
begin

class preorder_equiv = preorder
begin

definition equiv :: "'a \ 'a \ bool"
  where "equiv x y \ x \ y \ y \ x"

notation
  equiv (\<open>'(\<approx>')\<close>) and
  equiv (\<open>(\<open>notation=\<open>infix \<approx>\<close>\<close>_/ \<approx> _)\<close>  [51, 51] 50)

lemma equivD1: "x \ y" if "x \ y"
  using that by (simp add: equiv_def)

lemma equivD2: "y \ x" if "x \ y"
  using that by (simp add: equiv_def)

lemma equiv_refl [iff]: "x \ x"
  by (simp add: equiv_def)

lemma equiv_sym: "x \ y \ y \ x"
  by (auto simp add: equiv_def)

lemma equiv_trans: "x \ y \ y \ z \ x \ z"
  by (auto simp: equiv_def intro: order_trans)

lemma equiv_antisym: "x \ y \ y \ x \ x \ y"
  by (simp only: equiv_def)

lemma less_le: "x < y \ x \ y \ \ x \ y"
  by (auto simp add: equiv_def less_le_not_le)

lemma le_less: "x \ y \ x < y \ x \ y"
  by (auto simp add: equiv_def less_le)

lemma le_imp_less_or_equiv: "x \ y \ x < y \ x \ y"
  by (simp add: less_le)

lemma less_imp_not_equiv: "x < y \ \ x \ y"
  by (simp add: less_le)

lemma not_equiv_le_trans: "\ a \ b \ a \ b \ a < b"
  by (simp add: less_le)

lemma le_not_equiv_trans: "a \ b \ \ a \ b \ a < b"
  by (rule not_equiv_le_trans)

lemma antisym_conv: "y \ x \ x \ y \ x \ y"
  by (simp add: equiv_def)

end

ML_file \<open>~~/src/Provers/preorder.ML\<close>

ML \<open>
structure Quasi = Quasi_Tac(
struct

val le_trans = @{thm order_trans};
val le_refl = @{thm order_refl};
val eqD1 = @{thm equivD1};
val eqD2 = @{thm equivD2};
val less_reflE = @{thm less_irrefl};
val less_imp_le = @{thm less_imp_le};
val le_neq_trans = @{thm le_not_equiv_trans};
val neq_le_trans = @{thm not_equiv_le_trans};
val less_imp_neq = @{thm less_imp_not_equiv};

fun decomp_quasi thy (Const (@{const_name less_eq}, _) $ t1 $ t2) = SOME (t1, "<=", t2)
  | decomp_quasi thy (Const (@{const_name less}, _) $ t1 $ t2) = SOME (t1, "<", t2)
  | decomp_quasi thy (Const (@{const_name equiv}, _) $ t1 $ t2) = SOME (t1, "=", t2)
  | decomp_quasi thy (Const (@{const_name Not}, _) $ (Const (@{const_name equiv}, _) $ t1 $ t2)) = SOME (t1, "~=", t2)
  | decomp_quasi thy _ = NONE;

fun decomp_trans thy t = case decomp_quasi thy t of
    x as SOME (t1, "<=", t2) => x
  | _ => NONE;

end
);
\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.