# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308097919 -32400
# Node ID f8eb6cd9f56015e7e9e8e2c766258b15343ac78f
# Parent  31c338d562fd00c91b02df2c956df73bff918b2a# Parent  354a930ef18fdfbedae6db666149162197a4a854
merge

diff -r 354a930ef18f -r f8eb6cd9f560 Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Wed Jun 15 09:25:36 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Wed Jun 15 09:31:59 2011 +0900
@@ -1697,12 +1697,10 @@
 subsection {* helper functions for nominal_functions *}
 
 lemma THE_defaultI2:
-  assumes "P a" "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
+  assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   shows "Q (THE_default d P)"
 by (iprover intro: assms THE_defaultI')
 
-thm THE_default1_equality
-
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
   shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))"
@@ -1728,22 +1726,16 @@
   apply(rule THE_default1_equality [symmetric])
   apply(rule_tac p="-p" in permute_boolE)
   apply(perm_simp add: permute_minus_cancel)
-  using eqvt
-  unfolding eqvt_def
+  using eqvt[simplified eqvt_def]
   apply(simp)
   apply(rule ex1)
-  apply(rule_tac p="-p" in permute_boolE)
-  apply(subst permute_fun_app_eq)
-  back
-  apply(subst the_default_eqvt)
+  apply(rule THE_defaultI2) 
   apply(rule_tac p="-p" in permute_boolE)
   apply(perm_simp add: permute_minus_cancel)
   apply(rule ex1)
-  apply(perm_simp add: permute_minus_cancel)
-  using eqvt
-  unfolding eqvt_def
+  apply(perm_simp)
+  using eqvt[simplified eqvt_def]
   apply(simp)
-  apply(rule THE_defaultI'[OF ex1])
   done
 
 lemma fundef_ex1_eqvt_at:
@@ -1756,7 +1748,6 @@
   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 x) (G x))"
@@ -1767,7 +1758,6 @@
   using ex1
   apply(erule_tac ex1E)
   apply(rule THE_defaultI2)
-  apply(assumption)
   apply(blast)
   apply(rule P_all)
   apply(assumption)