equal
deleted
inserted
replaced
739 by (auto split: split_if_asm elim: botE) |
739 by (auto split: split_if_asm elim: botE) |
740 lemma "f () = False \<or> f () = True" |
740 lemma "f () = False \<or> f () = True" |
741 by simp |
741 by simp |
742 |
742 |
743 lemma closure_of_bool_cases [no_atp]: |
743 lemma closure_of_bool_cases [no_atp]: |
744 assumes "(f :: unit \<Rightarrow> bool) = (%u. False) \<Longrightarrow> P f" |
744 fixes f :: "unit \<Rightarrow> bool" |
745 assumes "f = (%u. True) \<Longrightarrow> P f" |
745 assumes "f = (\<lambda>u. False) \<Longrightarrow> P f" |
746 shows "P f" |
746 assumes "f = (\<lambda>u. True) \<Longrightarrow> P f" |
|
747 shows "P f" |
747 proof - |
748 proof - |
748 have "f = (%u. False) \<or> f = (%u. True)" |
749 have "f = (\<lambda>u. False) \<or> f = (\<lambda>u. True)" |
749 apply (cases "f ()") |
750 apply (cases "f ()") |
750 apply (rule disjI2) |
751 apply (rule disjI2) |
751 apply (rule ext) |
752 apply (rule ext) |
752 apply (simp add: unit_eq) |
753 apply (simp add: unit_eq) |
753 apply (rule disjI1) |
754 apply (rule disjI1) |
756 done |
757 done |
757 from this assms show ?thesis by blast |
758 from this assms show ?thesis by blast |
758 qed |
759 qed |
759 |
760 |
760 lemma unit_pred_cases: |
761 lemma unit_pred_cases: |
761 assumes "P \<bottom>" |
762 assumes "P \<bottom>" |
762 assumes "P (single ())" |
763 assumes "P (single ())" |
763 shows "P Q" |
764 shows "P Q" |
764 using assms |
765 using assms unfolding bot_pred_def Collect_def empty_def single_def proof (cases Q) |
765 unfolding bot_pred_def Collect_def empty_def single_def |
766 fix f |
766 apply (cases Q) |
767 assume "P (Pred (\<lambda>u. False))" "P (Pred (\<lambda>u. () = u))" |
767 apply simp |
768 then have "P (Pred f)" |
768 apply (rule_tac f="fun" in closure_of_bool_cases) |
769 by (cases _ f rule: closure_of_bool_cases) simp_all |
769 apply auto |
770 moreover assume "Q = Pred f" |
770 apply (subgoal_tac "(%x. () = x) = (%x. True)") |
771 ultimately show "P Q" by simp |
771 apply auto |
772 qed |
772 done |
773 |
773 |
|
774 lemma holds_if_pred: |
774 lemma holds_if_pred: |
775 "holds (if_pred b) = b" |
775 "holds (if_pred b) = b" |
776 unfolding if_pred_eq holds_eq |
776 unfolding if_pred_eq holds_eq |
777 by (cases b) (auto intro: singleI elim: botE) |
777 by (cases b) (auto intro: singleI elim: botE) |
778 |
778 |