1825 code_datatype Trueprop "prop" |
1825 code_datatype Trueprop "prop" |
1826 |
1826 |
1827 text {* Code equations *} |
1827 text {* Code equations *} |
1828 |
1828 |
1829 lemma [code]: |
1829 lemma [code]: |
1830 shows "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
1830 shows "(False \<Longrightarrow> P) \<equiv> Trueprop True" |
1831 and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" |
1831 and "(True \<Longrightarrow> PROP Q) \<equiv> PROP Q" |
1832 and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" |
1832 and "(P \<Longrightarrow> False) \<equiv> Trueprop (\<not> P)" |
1833 and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule) |
1833 and "(PROP Q \<Longrightarrow> True) \<equiv> Trueprop True" by (auto intro!: equal_intr_rule) |
1834 |
1834 |
1835 lemma [code]: |
1835 lemma [code]: |
1836 shows "False \<and> x \<longleftrightarrow> False" |
1836 shows "False \<and> P \<longleftrightarrow> False" |
1837 and "True \<and> x \<longleftrightarrow> x" |
1837 and "True \<and> P \<longleftrightarrow> P" |
1838 and "x \<and> False \<longleftrightarrow> False" |
1838 and "P \<and> False \<longleftrightarrow> False" |
1839 and "x \<and> True \<longleftrightarrow> x" by simp_all |
1839 and "P \<and> True \<longleftrightarrow> P" by simp_all |
1840 |
1840 |
1841 lemma [code]: |
1841 lemma [code]: |
1842 shows "False \<or> x \<longleftrightarrow> x" |
1842 shows "False \<or> P \<longleftrightarrow> P" |
1843 and "True \<or> x \<longleftrightarrow> True" |
1843 and "True \<or> P \<longleftrightarrow> True" |
1844 and "x \<or> False \<longleftrightarrow> x" |
1844 and "P \<or> False \<longleftrightarrow> P" |
1845 and "x \<or> True \<longleftrightarrow> True" by simp_all |
1845 and "P \<or> True \<longleftrightarrow> True" by simp_all |
1846 |
1846 |
1847 declare imp_conv_disj [code, code_unfold_post] |
1847 lemma [code]: |
|
1848 shows "(False \<longrightarrow> P) \<longleftrightarrow> True" |
|
1849 and "(True \<longrightarrow> P) \<longleftrightarrow> P" |
|
1850 and "(P \<longrightarrow> False) \<longleftrightarrow> \<not> P" |
|
1851 and "(P \<longrightarrow> True) \<longleftrightarrow> True" by simp_all |
1848 |
1852 |
1849 instantiation itself :: (type) eq |
1853 instantiation itself :: (type) eq |
1850 begin |
1854 begin |
1851 |
1855 |
1852 definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where |
1856 definition eq_itself :: "'a itself \<Rightarrow> 'a itself \<Rightarrow> bool" where |