# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307289498 -3600
# Node ID 8fe80e9f796dbfe7ba89159296197b755b236c06
# Parent  2f5ce0ecbf312c4b7a93c38984e89766e0352e15
added a more general lemma fro fundef_ex1

diff -r 2f5ce0ecbf31 -r 8fe80e9f796d Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Sat Jun 04 14:50:57 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Sun Jun 05 16:58:18 2011 +0100
@@ -1696,6 +1696,11 @@
 
 subsection {* helper functions for nominal_functions *}
 
+lemma THE_defaultI2:
+  assumes "P a" "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
+  shows "Q (THE_default d P)"
+by (iprover intro: assms THE_defaultI')
+
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))"
@@ -1733,6 +1738,23 @@
   using assms
   by (auto intro: fundef_ex1_eqvt)
 
+(* fixme: polish *)
+lemma fundef_ex1_prop:
+  fixes x::"'a::pt"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes P_all: "\<And>y. G x y \<Longrightarrow> P y"
+  assumes ex1: "\<exists>!y. G x y"
+  shows "P (f x)"
+  unfolding f_def
+  using ex1
+  apply(erule_tac ex1E)
+  apply(rule THE_defaultI2)
+  apply(assumption)
+  apply(blast)
+  apply(rule P_all)
+  apply(assumption)
+  done
+
 
 section {* Support of Finite Sets of Finitely Supported Elements *}