# HG changeset patch # User urbanc # Date 1140724591 -3600 # Node ID ff41946e5092fd520c5326ecc5a6cdeb61ea65fd # Parent 06b6f5f8e4cb27e223bfc1ecb64b41929770ba4e added lemmas at_two: EX a b in an atom type such that a !=b at_ds10 and a "test"-lemma at_prm_eq_compose (can probably be removed) diff -r 06b6f5f8e4cb -r ff41946e5092 src/HOL/Nominal/Nominal.thy --- a/src/HOL/Nominal/Nominal.thy Thu Feb 23 13:37:46 2006 +0100 +++ b/src/HOL/Nominal/Nominal.thy Thu Feb 23 20:56:31 2006 +0100 @@ -619,16 +619,14 @@ done lemma at_ds10: - fixes pi1 :: "'x prm" - and pi2 :: "'x prm" + fixes pi :: "'x prm" and a :: "'x" and b :: "'x" assumes at: "at TYPE('x)" - and a: "b\(rev pi1)" - shows "(pi2@([(pi1\a,b)]@pi1)) \ (pi2@(pi1@[(a,b)]))" + and a: "b\(rev pi)" + shows "([(pi\a,b)]@pi) \ (pi@[(a,b)])" using a apply - -apply(rule at_prm_eq_append[OF at]) apply(rule at_prm_eq_trans) apply(rule at_ds2[OF at]) apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at]) @@ -668,6 +666,27 @@ apply simp done +lemma at_two: + assumes at: "at TYPE('x)" + shows "\(a::'x) (b::'x). a\b" +proof - + have inf1: "infinite (UNIV::'x set)" by (rule at4[OF at]) + hence "UNIV \ ({}::'x set)" by blast + hence "\(a::'x). a\UNIV" by blast + then obtain a::"'x" where mem1: "a\UNIV" by blast + from inf1 have inf2: "infinite (UNIV-{a})" by (rule infinite_remove) + have "(UNIV-{a}) \ ({}::'x set)" + proof (rule_tac ccontr, drule_tac notnotD) + assume "UNIV-{a} = ({}::'x set)" + with inf2 have "infinite ({}::'x set)" by simp + then show "False" by (auto intro: infinite_nonempty) + qed + hence "\(b::'x). b\(UNIV-{a})" by blast + then obtain b::"'x" where mem2: "b\(UNIV-{a})" by blast + from mem1 mem2 have "a\b" by blast + then show "\(a::'x) (b::'x). a\b" by blast +qed + --"the at-props imply the pt-props" lemma at_pt_inst: assumes at: "at TYPE('x)" @@ -2669,6 +2688,33 @@ by (simp add: perm_fun_def) +section {* test *} +lemma at_prm_eq_compose: + fixes pi1 :: "'x prm" + and pi2 :: "'x prm" + and pi3 :: "'x prm" + assumes at: "at TYPE('x)" + and a: "pi1 \ pi2" + shows "(pi3\pi1) \ (pi3\pi2)" +proof - + have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at]) + have pt_prm: "pt TYPE('x prm) TYPE('x)" + by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]]) + from a show ?thesis + apply - + apply(auto simp add: prm_eq_def) + apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at]) + apply(rule trans) + apply(rule pt_perm_compose[OF pt, OF at]) + apply(simp add: pt_rev_pi[OF pt_prm, OF at]) + apply(rule sym) + apply(rule trans) + apply(rule pt_perm_compose[OF pt, OF at]) + apply(simp add: pt_rev_pi[OF pt_prm, OF at]) + done +qed + + (***************************************) (* setup for the individial atom-kinds *) (* and nominal datatypes *)