equal
deleted
inserted
replaced
13 theory BNF_Fixpoint_Base |
13 theory BNF_Fixpoint_Base |
14 imports BNF_Composition Basic_BNFs |
14 imports BNF_Composition Basic_BNFs |
15 begin |
15 begin |
16 |
16 |
17 lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True" |
17 lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True" |
18 by default simp_all |
18 by standard simp_all |
19 |
19 |
20 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" |
20 lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)" |
21 by default simp_all |
21 by standard simp_all |
22 |
22 |
23 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
23 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q" |
24 by auto |
24 by auto |
25 |
25 |
26 lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" |
26 lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y" |