# HG changeset patch # User Christian Urban <urbanc@in.tum.de> # Date 1308075104 -3600 # Node ID 31c338d562fd00c91b02df2c956df73bff918b2a # Parent da7e6655cd4c0fa675908ccbdea2300766684e2a tuned some proofs diff -r da7e6655cd4c -r 31c338d562fd Nominal/Nominal2_Base.thy --- a/Nominal/Nominal2_Base.thy Tue Jun 14 14:07:07 2011 +0100 +++ b/Nominal/Nominal2_Base.thy Tue Jun 14 19:11:44 2011 +0100 @@ -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)