src/HOL/Codatatype/BNF_FP.thy
changeset 49335 096967bf3940
parent 49325 340844cbf7af
child 49368 df359ce891ac
     1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 16:54:24 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Wed Sep 12 17:26:05 2012 +0200
     1.3 @@ -17,10 +17,17 @@
     1.4  lemma case_unit: "(case u of () => f) = f"
     1.5  by (cases u) (hypsubst, rule unit.cases)
     1.6  
     1.7 -(* FIXME: needed? *)
     1.8 +lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
     1.9 +by simp
    1.10 +
    1.11 +lemma prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    1.12 +by clarify
    1.13 +
    1.14 +lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    1.15 +by auto
    1.16 +
    1.17  lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
    1.18  
    1.19 -(* FIXME: needed? *)
    1.20  lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
    1.21  
    1.22  (* FIXME: needed? *)