equal
deleted
inserted
replaced
12 imports BNF_Comp BNF_Wrap |
12 imports BNF_Comp BNF_Wrap |
13 keywords |
13 keywords |
14 "defaults" |
14 "defaults" |
15 begin |
15 begin |
16 |
16 |
17 lemma case_unit: "(case u of () => f) = f" |
17 lemma unit_case_Unity: "(case u of () => f) = f" |
18 by (cases u) (hypsubst, rule unit.cases) |
18 by (cases u) (hypsubst, rule unit.cases) |
|
19 |
|
20 lemma prod_case_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p" |
|
21 by simp |
19 |
22 |
20 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
23 lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
21 by simp |
24 by simp |
22 |
25 |
23 lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |
26 lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x" |