author urbanc Mon Feb 18 03:12:08 2008 +0100 (2008-02-18) changeset 26090 ec111fa4f8c5 parent 26089 373221497340 child 26091 f31d4fe763aa
 src/HOL/Nominal/Nominal.thy file | annotate | diff | revisions src/HOL/Nominal/nominal_atoms.ML file | annotate | diff | revisions
```     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.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.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]