equal
deleted
inserted
replaced
18 |
18 |
19 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
19 lemma eq_sym_Unity_conv: "(x = (() = ())) = x" |
20 by blast |
20 by blast |
21 |
21 |
22 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" |
22 lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f" |
23 by (cases u) (hypsubst, rule unit.cases) |
23 by (cases u) (hypsubst, rule unit.case) |
24 |
24 |
25 lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" |
25 lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" |
26 by simp |
26 by simp |
27 |
27 |
28 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
28 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |