# HG changeset patch # User urbanc # Date 1133775157 -3600 # Node ID 6bab9cef50cf78cb7e9423b4407f18388ef04e57 # Parent 66cda85ea3ab5a4bc47ebac3ee9addafac09f704 ISAR-fied two proofs diff -r 66cda85ea3ab -r 6bab9cef50cf src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Mon Dec 05 00:39:18 2005 +0100 +++ b/src/HOL/Nominal/Nominal.thy Mon Dec 05 10:32:37 2005 +0100 @@ -1683,26 +1683,35 @@ proof - have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at) show ?thesis - apply(auto simp add: perm_set_def) - apply(rule_tac x="pi\xa" in exI) - apply(rule conjI) - apply(rule_tac x="xa" in exI) - apply(simp) - apply(subgoal_tac "(pi\f) (pi\xa) = pi\(f xa)")(*A*) - apply(simp) - apply(rule pt_set_bij2[OF pt_x, OF at]) - apply(assumption) - apply(rule sym) - apply(rule pt_fun_app_eq[OF pt, OF at]) - apply(rule_tac x="(rev pi)\x" in exI) - apply(rule conjI) - apply(rule sym) - apply(rule pt_pi_rev[OF pt_x, OF at]) - apply(rule_tac x="a" in bexI) - apply(simp add: pt_set_bij1[OF pt_x, OF at]) - apply(simp add: pt_fun_app_eq[OF pt, OF at]) - apply(assumption) - done + proof (rule equalityI) + case goal1 + show "pi\(\x\X. f x) \ (\x\(pi\X). (pi\f) x)" + apply(auto simp add: perm_set_def) + apply(rule_tac x="pi\xa" in exI) + apply(rule conjI) + apply(rule_tac x="xa" in exI) + apply(simp) + apply(subgoal_tac "(pi\f) (pi\xa) = pi\(f xa)")(*A*) + apply(simp) + apply(rule pt_set_bij2[OF pt_x, OF at]) + apply(assumption) + (*A*) + apply(rule sym) + apply(rule pt_fun_app_eq[OF pt, OF at]) + done + next + case goal2 + show "(\x\(pi\X). (pi\f) x) \ pi\(\x\X. f x)" + apply(auto simp add: perm_set_def) + apply(rule_tac x="(rev pi)\x" in exI) + apply(rule conjI) + apply(simp add: pt_pi_rev[OF pt_x, OF at]) + apply(rule_tac x="a" in bexI) + apply(simp add: pt_set_bij1[OF pt_x, OF at]) + apply(simp add: pt_fun_app_eq[OF pt, OF at]) + apply(assumption) + done + qed qed lemma X_to_Un_supp_eqvt: @@ -1760,8 +1769,7 @@ apply(force intro: pt_set_inst at_pt_inst pt at)+ apply(rule pt_eqvt_fun2b) apply(force intro: pt_set_inst at_pt_inst pt at)+ - apply(rule allI) - apply(rule allI) + apply(rule allI)+ apply(rule X_to_Un_supp_eqvt[OF pt, OF at]) done hence "supp (\x\X. ((supp x)::'x set)) \ ((supp X)::'x set)" by (simp add: X_to_Un_supp_def) @@ -1780,7 +1788,7 @@ and fs: "fs TYPE('a) TYPE('x)" and fi: "finite X" shows "(supp X) = (\x\X. ((supp x)::'x set))" -apply(rule subset_antisym) +apply(rule equalityI) apply(rule supp_is_subset) apply(rule Union_supports_set[OF pt, OF at]) apply(rule Union_of_fin_supp_sets[OF fs, OF fi]) @@ -2242,38 +2250,6 @@ and at: "at TYPE('x)" and a1: "a\b" and a2: "[a].x = [b].y" - shows "x=[(a,b)]\y\a\y" -proof - - from a2 have a3: - "\c::'x. (if c=a then nSome(x) else (if c\x then nSome([(a,c)]\x) else nNone)) - = (if c=b then nSome(y) else (if c\y then nSome([(b,c)]\y) else nNone))" - (is "\c::'x. ?P c = ?Q c") - by (force simp add: abs_fun_def expand_fun_eq) - from a3 have "?P a = ?Q a" by (blast) - hence a4: "nSome(x) = ?Q a" by simp - show ?thesis using a4 (*a5*) - proof (cases "a\y") - assume a6: "a\y" - hence a7: "x = [(b,a)]\y" using a4 a1 by simp - have "[(a,b)]\y = [(b,a)]\y" by (rule pt3[OF pt], rule at_ds5[OF at]) - thus ?thesis using a6 a7 by simp - next - assume "\a\y" - hence "nSome(x) = nNone" using a1 a4 by simp - hence False by force - thus ?thesis by force - qed -qed - -lemma abs_fun_eq2: - fixes x :: "'a" - and y :: "'a" - and a :: "'x" - and b :: "'x" - assumes pt: "pt TYPE('a) TYPE('x)" - and at: "at TYPE('x)" - and a1: "a\b" - and a2: "[a].x = [b].y" shows "x=[(a,b)]\y \ a\y" proof - from a2 have "\c::'x. ([a].x) c = ([b].y) c" by (force simp add: expand_fun_eq)