treatment of type constructor `set`
authorhaftmann
Sat Dec 24 15:53:08 2011 +0100 (2011-12-24)
changeset 459615cefe17916a6
parent 45960 e1b09bfb52f1
child 45962 fc77947a7db4
treatment of type constructor `set`
src/HOL/Nominal/Nominal.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Dec 24 15:53:07 2011 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Dec 24 15:53:08 2011 +0100
     1.3 @@ -38,6 +38,7 @@
     1.4  overloading
     1.5    perm_fun    \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<Rightarrow>'b) \<Rightarrow> ('a\<Rightarrow>'b)"   (unchecked)
     1.6    perm_bool   \<equiv> "perm :: 'x prm \<Rightarrow> bool \<Rightarrow> bool"           (unchecked)
     1.7 +  perm_set    \<equiv> "perm :: 'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set"           (unchecked)
     1.8    perm_unit   \<equiv> "perm :: 'x prm \<Rightarrow> unit \<Rightarrow> unit"           (unchecked)
     1.9    perm_prod   \<equiv> "perm :: 'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)"    (unchecked)
    1.10    perm_list   \<equiv> "perm :: 'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list"     (unchecked)
    1.11 @@ -56,6 +57,9 @@
    1.12  definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where
    1.13    "perm_bool pi b = b"
    1.14  
    1.15 +definition perm_set :: "'x prm \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    1.16 +  "perm_set pi A = {x. rev pi \<bullet> x \<in> A}"
    1.17 +
    1.18  primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit"  where 
    1.19    "perm_unit pi () = ()"
    1.20    
    1.21 @@ -131,10 +135,6 @@
    1.22    by (simp add: perm_bool)
    1.23  
    1.24  (* permutation on sets *)
    1.25 -lemma perm_set_def:
    1.26 -  "pi \<bullet> A = {x. rev pi \<bullet> x \<in> A}"
    1.27 -  by (simp add: perm_fun_def perm_bool_def Collect_def mem_def)
    1.28 -
    1.29  lemma empty_eqvt:
    1.30    shows "pi\<bullet>{} = {}"
    1.31    by (simp add: perm_set_def fun_eq_iff)
    1.32 @@ -963,7 +963,7 @@
    1.33    and   x ::"'x set"
    1.34    assumes dj: "disjoint TYPE('x) TYPE('y)"
    1.35    shows "pi\<bullet>x=x" 
    1.36 -  using dj by (simp_all add: perm_fun_def disjoint_def perm_bool)
    1.37 +  using dj by (simp_all add: perm_set_def disjoint_def)
    1.38  
    1.39  lemma dj_perm_perm_forget:
    1.40    fixes pi1::"'x prm"
    1.41 @@ -1022,9 +1022,11 @@
    1.42    and     at:  "at TYPE('x)"
    1.43    shows "pt TYPE('a set) TYPE('x)"
    1.44  proof -
    1.45 +  have *: "\<And>pi A. pi \<bullet> A = {x. (pi \<bullet> (\<lambda>x. x \<in> A)) x}"
    1.46 +    by (simp add: perm_fun_def perm_bool_def perm_set_def)
    1.47    from pta pt_bool_inst at
    1.48      have "pt TYPE('a \<Rightarrow> bool) TYPE('x)" by (rule pt_fun_inst)
    1.49 -  then show ?thesis by (simp add: pt_def perm_set_def)
    1.50 +  then show ?thesis by (simp add: pt_def *)
    1.51  qed
    1.52  
    1.53  lemma pt_unit_inst:
    1.54 @@ -1247,7 +1249,7 @@
    1.55    assumes pt: "pt TYPE('a) TYPE('x)"
    1.56    and at: "at TYPE('x)" 
    1.57    shows "(pi::'x prm)\<bullet>(X::'a set) = {pi\<bullet>x | x. x\<in>X}"
    1.58 -  apply (auto simp add: perm_fun_def perm_bool mem_def)
    1.59 +  apply (auto simp add: perm_fun_def perm_bool perm_set_def)
    1.60    apply (rule_tac x="rev pi \<bullet> x" in exI)
    1.61    apply (simp add: pt_pi_rev [OF pt at])
    1.62    apply (simp add: pt_rev_pi [OF pt at])
    1.63 @@ -2262,7 +2264,7 @@
    1.64    and     at: "at TYPE('x)"
    1.65    shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
    1.66    apply(simp add: X_to_Un_supp_def)
    1.67 -  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
    1.68 +  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
    1.69    apply(simp add: pt_perm_supp[OF pt, OF at])
    1.70    apply(simp add: pt_pi_rev[OF pt, OF at])
    1.71    done
    1.72 @@ -2307,9 +2309,9 @@
    1.73  proof -
    1.74    have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
    1.75      apply(rule pt_empty_supp_fun_subset)
    1.76 -    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
    1.77 +    apply(force intro: pt_set_inst at_pt_inst pt at)+
    1.78      apply(rule pt_eqvt_fun2b)
    1.79 -    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
    1.80 +    apply(force intro: pt_set_inst at_pt_inst pt at)+
    1.81      apply(rule allI)+
    1.82      apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
    1.83      done
    1.84 @@ -2638,7 +2640,7 @@
    1.85      have "set ([]::'a prm) \<subseteq> {} \<times> {}" by simp
    1.86      moreover
    1.87      have "([]::'a prm)\<bullet>{} = ({}::'a set)" 
    1.88 -      by (rule pt1[OF pt_fun_inst, OF at_pt_inst[OF at] pt_bool_inst at])
    1.89 +      by (rule pt1 [OF pt_set_inst, OF at_pt_inst [OF at] at])
    1.90      ultimately show ?case by simp
    1.91    next
    1.92      case (insert x Xs)
    1.93 @@ -2653,7 +2655,7 @@
    1.94      obtain y::"'a" where fr: "y\<sharp>(c,pi\<bullet>Xs,As)" 
    1.95        apply(rule_tac at_exists_fresh[OF at, where x="(c,pi\<bullet>Xs,As)"])
    1.96        apply(auto simp add: supp_prod at_supp[OF at] at_fin_set_supp[OF at]
    1.97 -        pt_supp_finite_pi[OF pt_fun_inst[OF at_pt_inst[OF at] pt_bool_inst at] at])
    1.98 +        pt_supp_finite_pi[OF pt_set_inst[OF at_pt_inst[OF at] at] at])
    1.99        done
   1.100      have "({y}\<union>(pi\<bullet>Xs))\<sharp>*c" using a1 fr by (simp add: fresh_star_def)
   1.101      moreover
   1.102 @@ -2669,18 +2671,18 @@
   1.103        have eq: "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
   1.104        proof -
   1.105          have "(pi\<bullet>x)\<sharp>(pi\<bullet>Xs)" using b d2 
   1.106 -          by(simp add: pt_fresh_bij[OF pt_fun_inst, OF at_pt_inst[OF at], 
   1.107 -            OF pt_bool_inst, OF at, OF at]
   1.108 -            at_fin_set_fresh[OF at])
   1.109 +          by (simp add: pt_fresh_bij [OF pt_set_inst, OF at_pt_inst [OF at], 
   1.110 +            OF at, OF at]
   1.111 +            at_fin_set_fresh [OF at])
   1.112          moreover
   1.113          have "y\<sharp>(pi\<bullet>Xs)" using fr by simp
   1.114          ultimately show "[(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs) = (pi\<bullet>Xs)" 
   1.115 -          by (simp add: pt_fresh_fresh[OF pt_fun_inst, 
   1.116 -            OF at_pt_inst[OF at], OF pt_bool_inst, OF at, OF at])
   1.117 +          by (simp add: pt_fresh_fresh[OF pt_set_inst, 
   1.118 +            OF at_pt_inst[OF at], OF at, OF at])
   1.119        qed
   1.120        have "(((pi\<bullet>x,y)#pi)\<bullet>({x}\<union>Xs)) = ([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>({x}\<union>Xs)))"
   1.121 -        by (simp add: pt2[symmetric, OF pt_fun_inst, OF at_pt_inst[OF at], 
   1.122 -          OF pt_bool_inst, OF at])
   1.123 +        by (simp add: pt2[symmetric, OF pt_set_inst, OF at_pt_inst[OF at], 
   1.124 +          OF at])
   1.125        also have "\<dots> = {y}\<union>([(pi\<bullet>x,y)]\<bullet>(pi\<bullet>Xs))" 
   1.126          by (simp only: union_eqvt perm_set_eq[OF at_pt_inst[OF at], OF at] at_calc[OF at])(auto)
   1.127        finally show "(((pi\<bullet>x,y)#pi)\<bullet>({x} \<union> Xs)) = {y}\<union>(pi\<bullet>Xs)" using eq by simp
     2.1 --- a/src/HOL/Quotient.thy	Sat Dec 24 15:53:07 2011 +0100
     2.2 +++ b/src/HOL/Quotient.thy	Sat Dec 24 15:53:08 2011 +0100
     2.3 @@ -15,6 +15,13 @@
     2.4  begin
     2.5  
     2.6  text {*
     2.7 +  An aside: contravariant functorial structure of sets.
     2.8 +*}
     2.9 +
    2.10 +enriched_type vimage
    2.11 +  by (simp_all add: fun_eq_iff vimage_compose)
    2.12 +
    2.13 +text {*
    2.14    Basic definition for equivalence relations
    2.15    that are represented by predicates.
    2.16  *}