1.1 --- a/src/HOL/Nominal/Nominal.thy	Wed Aug 27 01:27:33 2008 +0200
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed Aug 27 04:47:30 2008 +0200
     1.3 @@ -1882,6 +1882,31 @@
     1.4  apply(simp add: pt_rev_pi[OF pt, OF at])
     1.5  done
     1.6  
     1.7 +lemma pt_ex1_eqvt:
     1.8 +  fixes  pi :: "'x prm"
     1.9 +  and     x :: "'a"
    1.10 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.11 +  and     at: "at TYPE('x)"
    1.12 +  shows  "(pi\<bullet>(\<exists>!x. P (x::'a))) = (\<exists>!x. pi\<bullet>(P (rev pi\<bullet>x)))"
    1.13 +unfolding Ex1_def
    1.14 +by (simp add: pt_ex_eqvt[OF pt at] conj_eqvt pt_all_eqvt[OF pt at] 
    1.15 +              imp_eqvt pt_eq_eqvt[OF pt at] pt_pi_rev[OF pt at])
    1.16 +
    1.17 +lemma pt_the_eqvt:
    1.18 +  fixes  pi :: "'x prm"
    1.19 +  assumes pt: "pt TYPE('a) TYPE('x)"
    1.20 +  and     at: "at TYPE('x)"
    1.21 +  and     unique: "\<exists>!x. P x"
    1.22 +  shows "pi\<bullet>(THE(x::'a). P x) = (THE(x::'a). pi\<bullet>(P ((rev pi)\<bullet>x)))"
    1.23 +  apply(rule the1_equality [symmetric])
    1.24 +  apply(simp add: pt_ex1_eqvt[OF pt at,symmetric])
    1.25 +  apply(simp add: perm_bool unique)
    1.26 +  apply(simp add: perm_bool pt_rev_pi [OF pt at])
    1.27 +  apply(rule theI'[OF unique])
    1.28 +  done
    1.29 +
    1.30 +
    1.31 +
    1.32  section {* facts about supports *}
    1.33  (*==============================*)
    1.34  

     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 01:27:33 2008 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Aug 27 04:47:30 2008 +0200
     2.3 @@ -750,6 +750,8 @@
     2.4         val eq_eqvt             = @{thm "Nominal.pt_eq_eqvt"};
     2.5         val all_eqvt            = @{thm "Nominal.pt_all_eqvt"};
     2.6         val ex_eqvt             = @{thm "Nominal.pt_ex_eqvt"};
     2.7 +       val ex1_eqvt            = @{thm "Nominal.pt_ex1_eqvt"};
     2.8 +       val the_eqvt            = @{thm "Nominal.pt_the_eqvt"};
     2.9         val pt_pi_rev           = @{thm "Nominal.pt_pi_rev"};
    2.10         val pt_rev_pi           = @{thm "Nominal.pt_rev_pi"};
    2.11         val at_exists_fresh     = @{thm "Nominal.at_exists_fresh"};
    2.12 @@ -864,6 +866,8 @@
    2.13                  [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
    2.14                end
    2.15              ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
    2.16 +            ||>> PureThy.add_thmss [(("ex1_eqvt", inst_pt_at [ex1_eqvt]),[NominalThmDecls.eqvt_force_add])]
    2.17 +            ||>> PureThy.add_thmss [(("the_eqvt", inst_pt_at [the_eqvt]),[NominalThmDecls.eqvt_force_add])]
    2.18              ||>> PureThy.add_thmss 
    2.19                let val thms1 = inst_at [at_fresh]
    2.20                    val thms2 = inst_dj [at_fresh_ineq]