equal
deleted
inserted
replaced
15 begin |
15 begin |
16 |
16 |
17 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" |
17 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" |
18 by standard simp_all |
18 by standard simp_all |
19 |
19 |
20 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
20 lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> R \<and> (P x y \<longrightarrow> Q x y)" |
21 by auto |
21 by blast |
22 |
|
23 lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" |
|
24 by auto |
|
25 |
22 |
26 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
23 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
27 by blast |
24 by blast |
28 |
25 |
29 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" |
26 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" |