library theories for debugging and parallel computing using code generation towards Isabelle/ML
1 (* Author: Florian Haftmann, TU Muenchen *)
3 header {* Preorders with explicit equivalence relation *}
9 class preorder_equiv = preorder
12 definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
13 "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
17 equiv ("(_/ ~~ _)" [51, 51] 50)
20 equiv ("op \<approx>") and
21 equiv ("(_/ \<approx> _)" [51, 51] 50)
23 notation (HTML output)
24 equiv ("op \<approx>") and
25 equiv ("(_/ \<approx> _)" [51, 51] 50)
29 unfolding equiv_def by simp
32 "x \<approx> y \<Longrightarrow> y \<approx> z \<Longrightarrow> x \<approx> z"
33 unfolding equiv_def by (auto intro: order_trans)
36 "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x \<approx> y"
37 unfolding equiv_def ..
39 lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> x \<approx> y"
40 by (auto simp add: equiv_def less_le_not_le)
42 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x \<approx> y"
43 by (auto simp add: equiv_def less_le)
45 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x \<approx> y"
46 by (simp add: less_le)
48 lemma less_imp_not_eq: "x < y \<Longrightarrow> x \<approx> y \<longleftrightarrow> False"
49 by (simp add: less_le)
51 lemma less_imp_not_eq2: "x < y \<Longrightarrow> y \<approx> x \<longleftrightarrow> False"
52 by (simp add: equiv_def less_le)
54 lemma neq_le_trans: "\<not> a \<approx> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
55 by (simp add: less_le)
57 lemma le_neq_trans: "a \<le> b \<Longrightarrow> \<not> a \<approx> b \<Longrightarrow> a < b"
58 by (simp add: less_le)
60 lemma antisym_conv: "y \<le> x \<Longrightarrow> x \<le> y \<longleftrightarrow> x \<approx> y"
61 by (simp add: equiv_def)