added eqvt-flag to subseteq-lemma
authorurbanc
Mon Feb 18 03:12:08 2008 +0100 (2008-02-18)
changeset 26090ec111fa4f8c5
parent 26089 373221497340
child 26091 f31d4fe763aa
added eqvt-flag to subseteq-lemma
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_atoms.ML
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Mon Feb 18 02:10:55 2008 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Mon Feb 18 03:12:08 2008 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    by (simp add: perm_set_def)
     1.5  
     1.6  lemma union_eqvt:
     1.7 -  shows "pi \<bullet> (X \<union> Y) = (pi \<bullet> X) \<union> (pi \<bullet> Y)"
     1.8 +  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
     1.9    by (auto simp add: perm_set_def)
    1.10  
    1.11  lemma insert_eqvt:
    1.12 @@ -47,7 +47,7 @@
    1.13  
    1.14  (* permutation on units and products *)
    1.15  primrec (unchecked perm_unit)
    1.16 -  "pi\<bullet>()    = ()"
    1.17 +  "pi\<bullet>() = ()"
    1.18    
    1.19  primrec (unchecked perm_prod)
    1.20    "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
    1.21 @@ -82,7 +82,7 @@
    1.22    fixes pi :: "'x prm"
    1.23    and   xs :: "'a list"
    1.24    shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
    1.25 -by (induct xs, auto simp add: empty_eqvt insert_eqvt)
    1.26 +by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
    1.27  
    1.28  (* permutation on functions *)
    1.29  defs (unchecked overloaded)
    1.30 @@ -1308,20 +1308,8 @@
    1.31    and   X  :: "'a set"
    1.32    assumes pt: "pt TYPE('a) TYPE('x)"
    1.33    and     at: "at TYPE('x)"
    1.34 -  shows "((pi\<bullet>X)\<subseteq>(pi\<bullet>Y)) = (X\<subseteq>Y)"
    1.35 -proof (auto)
    1.36 -  fix x::"'a"
    1.37 -  assume a: "(pi\<bullet>X)\<subseteq>(pi\<bullet>Y)"
    1.38 -  and    "x\<in>X"
    1.39 -  hence  "(pi\<bullet>x)\<in>(pi\<bullet>X)" by (simp add: pt_set_bij[OF pt, OF at])
    1.40 -  with a have "(pi\<bullet>x)\<in>(pi\<bullet>Y)" by force
    1.41 -  thus "x\<in>Y" by (simp add: pt_set_bij[OF pt, OF at])
    1.42 -next
    1.43 -  fix x::"'a"
    1.44 -  assume a: "X\<subseteq>Y"
    1.45 -  and    "x\<in>(pi\<bullet>X)"
    1.46 -  thus "x\<in>(pi\<bullet>Y)" by (force simp add: pt_set_bij1a[OF pt, OF at])
    1.47 -qed
    1.48 +  shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
    1.49 +by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
    1.50  
    1.51  lemma pt_set_diff_eqvt:
    1.52    fixes X::"'a set"
    1.53 @@ -3270,7 +3258,7 @@
    1.54    plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
    1.55    
    1.56    (* sets *)
    1.57 -  union_eqvt empty_eqvt insert_eqvt set_eqvt
    1.58 +  union_eqvt empty_eqvt insert_eqvt set_eqvt 
    1.59    
    1.60   
    1.61  (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
     2.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 02:10:55 2008 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Feb 18 03:12:08 2008 +0100
     2.3 @@ -775,6 +775,7 @@
     2.4         val fresh_aux           = @{thm "Nominal.pt_fresh_aux"};  
     2.5         val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
     2.6         val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
     2.7 +       val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
     2.8  
     2.9         (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
    2.10         (* types; this allows for example to use abs_perm (which is a      *)
    2.11 @@ -922,6 +923,9 @@
    2.12  	      let val thms1 = inst_pt_at [set_diff_eqvt]
    2.13  	      in [(("set_diff_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    2.14              ||>> PureThy.add_thmss
    2.15 +	      let val thms1 = inst_pt_at [subseteq_eqvt]
    2.16 +	      in [(("subseteq_eqvt", thms1),[NominalThmDecls.eqvt_add])] end
    2.17 +            ||>> PureThy.add_thmss
    2.18  	      let val thms1 = inst_pt_at [fresh_aux]
    2.19  		  and thms2 = inst_pt_pt_at_cp_dj [fresh_perm_app_ineq] 
    2.20  	      in  [(("fresh_aux", thms1 @ thms2),[])] end