Adapted to encoding of sets as predicates
authorberghofe
Wed May 07 10:57:19 2008 +0200 (2008-05-07)
changeset 2680640b411ec05aa
parent 26805 27941d7d9a11
child 26807 4cd176ea28dc
Adapted to encoding of sets as predicates
doc-src/TutorialI/Sets/Relations.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Complex/ex/BigO_Complex.thy
src/HOL/Hyperreal/NatStar.thy
src/HOL/Hyperreal/StarDef.thy
src/HOL/IOA/IOA.thy
src/HOL/Induct/Com.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Library/Order_Relation.thy
src/HOL/Library/RType.thy
src/HOL/Library/Zorn.thy
src/HOL/MetisExamples/Tarski.thy
src/HOL/MetisExamples/set.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/Nominal/Examples/Class.thy
src/HOL/Nominal/Examples/SOS.thy
src/HOL/Nominal/Examples/Support.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Real/PReal.thy
src/HOL/Subst/Unify.thy
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Transformers.thy
src/HOLCF/CompactBasis.thy
src/HOLCF/ConvexPD.thy
src/HOLCF/IOA/meta_theory/Automata.thy
src/HOLCF/LowerPD.thy
src/HOLCF/UpperPD.thy
     1.1 --- a/doc-src/TutorialI/Sets/Relations.thy	Wed May 07 10:56:58 2008 +0200
     1.2 +++ b/doc-src/TutorialI/Sets/Relations.thy	Wed May 07 10:57:19 2008 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  text{*Pow, Inter too little used*}
     1.5  
     1.6  lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
     1.7 -apply (simp add: psubset_def)
     1.8 +apply (simp add: psubset_eq)
     1.9  done
    1.10  
    1.11  end
     2.1 --- a/src/HOL/Algebra/Sylow.thy	Wed May 07 10:56:58 2008 +0200
     2.2 +++ b/src/HOL/Algebra/Sylow.thy	Wed May 07 10:57:19 2008 +0200
     2.3 @@ -262,7 +262,7 @@
     2.4  apply (rule coset_join1 [THEN in_H_imp_eq])
     2.5  apply (rule_tac [3] H_is_subgroup)
     2.6  prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
     2.7 -apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
     2.8 +apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
     2.9  done
    2.10  
    2.11  
     3.1 --- a/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:56:58 2008 +0200
     3.2 +++ b/src/HOL/Complex/ex/BigO_Complex.thy	Wed May 07 10:57:19 2008 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4    apply (drule set_plus_imp_minus)
     3.5    apply (drule bigo_LIMSEQ1)
     3.6    apply assumption
     3.7 -  apply (simp only: func_diff)
     3.8 +  apply (simp only: fun_diff_def)
     3.9    apply (erule LIMSEQ_diff_approach_zero2)
    3.10    apply assumption
    3.11  done
     4.1 --- a/src/HOL/Hyperreal/NatStar.thy	Wed May 07 10:56:58 2008 +0200
     4.2 +++ b/src/HOL/Hyperreal/NatStar.thy	Wed May 07 10:57:19 2008 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4  by (auto simp add: InternalSets_def starset_n_Int [symmetric])
     4.5  
     4.6  lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
     4.7 -apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_def)
     4.8 +apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
     4.9  apply (rule_tac x=whn in spec, transfer, simp)
    4.10  done
    4.11  
    4.12 @@ -44,7 +44,7 @@
    4.13  by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
    4.14  
    4.15  lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
    4.16 -apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_def)
    4.17 +apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
    4.18  apply (rule_tac x=whn in spec, transfer, simp)
    4.19  done
    4.20  
     5.1 --- a/src/HOL/Hyperreal/StarDef.thy	Wed May 07 10:56:58 2008 +0200
     5.2 +++ b/src/HOL/Hyperreal/StarDef.thy	Wed May 07 10:57:19 2008 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4  
     5.5  lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
     5.6  apply (unfold FreeUltrafilterNat_def)
     5.7 -apply (rule someI_ex)
     5.8 +apply (rule someI_ex [where P=freeultrafilter])
     5.9  apply (rule freeultrafilter_Ex)
    5.10  apply (rule nat_infinite)
    5.11  done
    5.12 @@ -401,10 +401,10 @@
    5.13  by (transfer Int_def, rule refl)
    5.14  
    5.15  lemma starset_Compl: "*s* -A = -( *s* A)"
    5.16 -by (transfer Compl_def, rule refl)
    5.17 +by (transfer Compl_eq, rule refl)
    5.18  
    5.19  lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
    5.20 -by (transfer set_diff_def, rule refl)
    5.21 +by (transfer set_diff_eq, rule refl)
    5.22  
    5.23  lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
    5.24  by (transfer image_def, rule refl)
    5.25 @@ -413,7 +413,7 @@
    5.26  by (transfer vimage_def, rule refl)
    5.27  
    5.28  lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
    5.29 -by (transfer subset_def, rule refl)
    5.30 +by (transfer subset_eq, rule refl)
    5.31  
    5.32  lemma starset_eq: "( *s* A = *s* B) = (A = B)"
    5.33  by (transfer, rule refl)
     6.1 --- a/src/HOL/IOA/IOA.thy	Wed May 07 10:56:58 2008 +0200
     6.2 +++ b/src/HOL/IOA/IOA.thy	Wed May 07 10:57:19 2008 +0200
     6.3 @@ -337,7 +337,7 @@
     6.4  lemma externals_of_par: "externals(asig_of(A1||A2)) =
     6.5     (externals(asig_of(A1)) Un externals(asig_of(A2)))"
     6.6    apply (simp add: externals_def asig_of_par asig_comp_def
     6.7 -    asig_inputs_def asig_outputs_def Un_def set_diff_def)
     6.8 +    asig_inputs_def asig_outputs_def Un_def set_diff_eq)
     6.9    apply blast
    6.10    done
    6.11  
     7.1 --- a/src/HOL/Induct/Com.thy	Wed May 07 10:56:58 2008 +0200
     7.2 +++ b/src/HOL/Induct/Com.thy	Wed May 07 10:57:19 2008 +0200
     7.3 @@ -85,11 +85,11 @@
     7.4  
     7.5  lemma [pred_set_conv]:
     7.6    "((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
     7.7 -  by (auto simp add: le_fun_def le_bool_def)
     7.8 +  by (auto simp add: le_fun_def le_bool_def mem_def)
     7.9  
    7.10  lemma [pred_set_conv]:
    7.11    "((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
    7.12 -  by (auto simp add: le_fun_def le_bool_def)
    7.13 +  by (auto simp add: le_fun_def le_bool_def mem_def)
    7.14  
    7.15  declare [[unify_trace_bound = 30, unify_search_bound = 60]]
    7.16  
     8.1 --- a/src/HOL/Lambda/InductTermi.thy	Wed May 07 10:56:58 2008 +0200
     8.2 +++ b/src/HOL/Lambda/InductTermi.thy	Wed May 07 10:57:19 2008 +0200
     8.3 @@ -34,7 +34,6 @@
     8.4    apply clarify
     8.5    apply (rule accp.accI)
     8.6    apply (safe elim!: apps_betasE)
     8.7 -     apply assumption
     8.8      apply (blast intro: subst_preserves_beta apps_preserves_beta)
     8.9     apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
    8.10       dest: accp_downwards)  (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
    8.11 @@ -44,7 +43,7 @@
    8.12  lemma IT_implies_termi: "IT t ==> termip beta t"
    8.13    apply (induct set: IT)
    8.14      apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
    8.15 -    apply fast
    8.16 +    apply (fast intro!: predicate1I)
    8.17      apply (drule lists_accD)
    8.18      apply (erule accp_induct)
    8.19      apply (rule accp.accI)
     9.1 --- a/src/HOL/Library/Order_Relation.thy	Wed May 07 10:56:58 2008 +0200
     9.2 +++ b/src/HOL/Library/Order_Relation.thy	Wed May 07 10:57:19 2008 +0200
     9.3 @@ -103,7 +103,7 @@
     9.4  lemma subset_Image_Image_iff:
     9.5    "\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
     9.6     r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
     9.7 -apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
     9.8 +apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
     9.9  apply metis
    9.10  by(metis trans_def)
    9.11  
    10.1 --- a/src/HOL/Library/RType.thy	Wed May 07 10:56:58 2008 +0200
    10.2 +++ b/src/HOL/Library/RType.thy	Wed May 07 10:57:19 2008 +0200
    10.3 @@ -87,7 +87,6 @@
    10.4    #> RType.add_def @{type_name fun}
    10.5    #> RType.add_def @{type_name itself}
    10.6    #> RType.add_def @{type_name bool}
    10.7 -  #> RType.add_def @{type_name set}
    10.8    #> TypedefPackage.interpretation RType.perhaps_add_def
    10.9  *}
   10.10  
    11.1 --- a/src/HOL/Library/Zorn.thy	Wed May 07 10:56:58 2008 +0200
    11.2 +++ b/src/HOL/Library/Zorn.thy	Wed May 07 10:57:19 2008 +0200
    11.3 @@ -44,7 +44,6 @@
    11.4    where
    11.5      succI:        "x \<in> TFin S ==> succ S x \<in> TFin S"
    11.6    | Pow_UnionI:   "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
    11.7 -  monos          Pow_mono
    11.8  
    11.9  
   11.10  subsection{*Mathematical Preamble*}
   11.11 @@ -57,22 +56,20 @@
   11.12  text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
   11.13  
   11.14  lemma Abrial_axiom1: "x \<subseteq> succ S x"
   11.15 -  apply (unfold succ_def)
   11.16 -  apply (rule split_if [THEN iffD2])
   11.17 -  apply (auto simp add: super_def maxchain_def psubset_def)
   11.18 +  apply (auto simp add: succ_def super_def maxchain_def)
   11.19    apply (rule contrapos_np, assumption)
   11.20 -  apply (rule someI2, blast+)
   11.21 +  apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
   11.22    done
   11.23  
   11.24  lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
   11.25  
   11.26  lemma TFin_induct:
   11.27 -          "[| n \<in> TFin S;
   11.28 -             !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
   11.29 -             !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
   11.30 -          ==> P(n)"
   11.31 -  apply (induct set: TFin)
   11.32 -   apply blast+
   11.33 +  assumes H: "n \<in> TFin S"
   11.34 +  and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
   11.35 +    "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
   11.36 +  shows "P n" using H
   11.37 +  apply (induct rule: TFin.induct [where P=P])
   11.38 +   apply (blast intro: I)+
   11.39    done
   11.40  
   11.41  lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
   11.42 @@ -163,14 +160,14 @@
   11.43  lemma select_super:
   11.44       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
   11.45    apply (erule mem_super_Ex [THEN exE])
   11.46 -  apply (rule someI2, auto)
   11.47 +  apply (rule someI2 [where Q="%X. X : super S c"], auto)
   11.48    done
   11.49  
   11.50  lemma select_not_equals:
   11.51       "c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
   11.52    apply (rule notI)
   11.53    apply (drule select_super)
   11.54 -  apply (simp add: super_def psubset_def)
   11.55 +  apply (simp add: super_def less_le)
   11.56    done
   11.57  
   11.58  lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
   11.59 @@ -189,7 +186,7 @@
   11.60    apply (rule CollectI, safe)
   11.61     apply (drule bspec, assumption)
   11.62     apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
   11.63 -     blast+)
   11.64 +     best+)
   11.65    done
   11.66  
   11.67  theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
   11.68 @@ -223,7 +220,7 @@
   11.69  apply (erule conjE)
   11.70  apply (subgoal_tac "({u} Un c) \<in> super S c")
   11.71   apply simp
   11.72 -apply (unfold super_def psubset_def)
   11.73 +apply (unfold super_def less_le)
   11.74  apply (blast intro: chain_extend dest: chain_Union_upper)
   11.75  done
   11.76  
   11.77 @@ -253,7 +250,7 @@
   11.78  apply (rule ccontr)
   11.79  apply (frule_tac z = x in chain_extend)
   11.80    apply (assumption, blast)
   11.81 -apply (unfold maxchain_def super_def psubset_def)
   11.82 +apply (unfold maxchain_def super_def less_le)
   11.83  apply (blast elim!: equalityCE)
   11.84  done
   11.85  
    12.1 --- a/src/HOL/MetisExamples/Tarski.thy	Wed May 07 10:56:58 2008 +0200
    12.2 +++ b/src/HOL/MetisExamples/Tarski.thy	Wed May 07 10:57:19 2008 +0200
    12.3 @@ -672,7 +672,7 @@
    12.4    declare (in CLF) rel_imp_elem[intro] 
    12.5    declare interval_def [simp]
    12.6  lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
    12.7 -by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
    12.8 +by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_eq)
    12.9    declare (in CLF) rel_imp_elem[rule del] 
   12.10    declare interval_def [simp del]
   12.11  
   12.12 @@ -1013,7 +1013,7 @@
   12.13  ML_command{*ResAtp.problem_name:="Tarski__fz_in_int_rel"*}  (*ALL THEOREMS*)
   12.14  lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
   12.15        ==> ((%x: intY1. f x) z, z) \<in> induced intY1 r" 
   12.16 -apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_def z_in_interval)
   12.17 +apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
   12.18  done
   12.19  
   12.20  (*never proved, 2007-01-22*)
    13.1 --- a/src/HOL/MetisExamples/set.thy	Wed May 07 10:56:58 2008 +0200
    13.2 +++ b/src/HOL/MetisExamples/set.thy	Wed May 07 10:57:19 2008 +0200
    13.3 @@ -238,7 +238,7 @@
    13.4  
    13.5  lemma (*singleton_example_2:*)
    13.6       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    13.7 -by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
    13.8 +by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
    13.9  
   13.10  lemma singleton_example_2:
   13.11       "\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
    14.1 --- a/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:56:58 2008 +0200
    14.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Wed May 07 10:57:19 2008 +0200
    14.3 @@ -330,7 +330,7 @@
    14.4   apply (rename_tac m n)
    14.5   apply (case_tac "m=n")
    14.6    apply simp
    14.7 - apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
    14.8 + apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
    14.9  apply clarify
   14.10  apply (rename_tac n)
   14.11  apply (induct_tac n)
    15.1 --- a/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:56:58 2008 +0200
    15.2 +++ b/src/HOL/Nominal/Examples/Class.thy	Wed May 07 10:57:19 2008 +0200
    15.3 @@ -10317,7 +10317,7 @@
    15.4  lemma NOTRIGHT_eqvt_name:
    15.5    fixes pi::"name prm"
    15.6    shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
    15.7 -apply(auto simp add: perm_set_def)
    15.8 +apply(auto simp add: perm_set_eq)
    15.9  apply(rule_tac x="pi\<bullet>a" in exI) 
   15.10  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.11  apply(rule_tac x="pi\<bullet>M" in exI)
   15.12 @@ -10343,7 +10343,7 @@
   15.13  lemma NOTRIGHT_eqvt_coname:
   15.14    fixes pi::"coname prm"
   15.15    shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
   15.16 -apply(auto simp add: perm_set_def)
   15.17 +apply(auto simp add: perm_set_eq)
   15.18  apply(rule_tac x="pi\<bullet>a" in exI) 
   15.19  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.20  apply(rule_tac x="pi\<bullet>M" in exI)
   15.21 @@ -10377,7 +10377,7 @@
   15.22  lemma NOTLEFT_eqvt_name:
   15.23    fixes pi::"name prm"
   15.24    shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
   15.25 -apply(auto simp add: perm_set_def)
   15.26 +apply(auto simp add: perm_set_eq)
   15.27  apply(rule_tac x="pi\<bullet>a" in exI) 
   15.28  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.29  apply(rule_tac x="pi\<bullet>M" in exI)
   15.30 @@ -10403,7 +10403,7 @@
   15.31  lemma NOTLEFT_eqvt_coname:
   15.32    fixes pi::"coname prm"
   15.33    shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
   15.34 -apply(auto simp add: perm_set_def)
   15.35 +apply(auto simp add: perm_set_eq)
   15.36  apply(rule_tac x="pi\<bullet>a" in exI) 
   15.37  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.38  apply(rule_tac x="pi\<bullet>M" in exI)
   15.39 @@ -10438,7 +10438,7 @@
   15.40  lemma ANDRIGHT_eqvt_name:
   15.41    fixes pi::"name prm"
   15.42    shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
   15.43 -apply(auto simp add: perm_set_def)
   15.44 +apply(auto simp add: perm_set_eq)
   15.45  apply(rule_tac x="pi\<bullet>c" in exI)
   15.46  apply(rule_tac x="pi\<bullet>a" in exI)
   15.47  apply(rule_tac x="pi\<bullet>b" in exI)
   15.48 @@ -10473,7 +10473,7 @@
   15.49  lemma ANDRIGHT_eqvt_coname:
   15.50    fixes pi::"coname prm"
   15.51    shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
   15.52 -apply(auto simp add: perm_set_def)
   15.53 +apply(auto simp add: perm_set_eq)
   15.54  apply(rule_tac x="pi\<bullet>c" in exI)
   15.55  apply(rule_tac x="pi\<bullet>a" in exI)
   15.56  apply(rule_tac x="pi\<bullet>b" in exI)
   15.57 @@ -10516,7 +10516,7 @@
   15.58  lemma ANDLEFT1_eqvt_name:
   15.59    fixes pi::"name prm"
   15.60    shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
   15.61 -apply(auto simp add: perm_set_def)
   15.62 +apply(auto simp add: perm_set_eq)
   15.63  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.64  apply(rule_tac x="pi\<bullet>y" in exI) 
   15.65  apply(rule_tac x="pi\<bullet>M" in exI)
   15.66 @@ -10542,7 +10542,7 @@
   15.67  lemma ANDLEFT1_eqvt_coname:
   15.68    fixes pi::"coname prm"
   15.69    shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
   15.70 -apply(auto simp add: perm_set_def)
   15.71 +apply(auto simp add: perm_set_eq)
   15.72  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.73  apply(rule_tac x="pi\<bullet>y" in exI) 
   15.74  apply(rule_tac x="pi\<bullet>M" in exI)
   15.75 @@ -10576,7 +10576,7 @@
   15.76  lemma ANDLEFT2_eqvt_name:
   15.77    fixes pi::"name prm"
   15.78    shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
   15.79 -apply(auto simp add: perm_set_def)
   15.80 +apply(auto simp add: perm_set_eq)
   15.81  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.82  apply(rule_tac x="pi\<bullet>y" in exI) 
   15.83  apply(rule_tac x="pi\<bullet>M" in exI)
   15.84 @@ -10602,7 +10602,7 @@
   15.85  lemma ANDLEFT2_eqvt_coname:
   15.86    fixes pi::"coname prm"
   15.87    shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
   15.88 -apply(auto simp add: perm_set_def)
   15.89 +apply(auto simp add: perm_set_eq)
   15.90  apply(rule_tac x="pi\<bullet>xb" in exI) 
   15.91  apply(rule_tac x="pi\<bullet>y" in exI) 
   15.92  apply(rule_tac x="pi\<bullet>M" in exI)
   15.93 @@ -10637,7 +10637,7 @@
   15.94  lemma ORLEFT_eqvt_name:
   15.95    fixes pi::"name prm"
   15.96    shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
   15.97 -apply(auto simp add: perm_set_def)
   15.98 +apply(auto simp add: perm_set_eq)
   15.99  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.100  apply(rule_tac x="pi\<bullet>y" in exI)
  15.101  apply(rule_tac x="pi\<bullet>z" in exI)
  15.102 @@ -10672,7 +10672,7 @@
  15.103  lemma ORLEFT_eqvt_coname:
  15.104    fixes pi::"coname prm"
  15.105    shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
  15.106 -apply(auto simp add: perm_set_def)
  15.107 +apply(auto simp add: perm_set_eq)
  15.108  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.109  apply(rule_tac x="pi\<bullet>y" in exI)
  15.110  apply(rule_tac x="pi\<bullet>z" in exI)
  15.111 @@ -10715,7 +10715,7 @@
  15.112  lemma ORRIGHT1_eqvt_name:
  15.113    fixes pi::"name prm"
  15.114    shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
  15.115 -apply(auto simp add: perm_set_def)
  15.116 +apply(auto simp add: perm_set_eq)
  15.117  apply(rule_tac x="pi\<bullet>a" in exI) 
  15.118  apply(rule_tac x="pi\<bullet>b" in exI) 
  15.119  apply(rule_tac x="pi\<bullet>M" in exI)
  15.120 @@ -10741,7 +10741,7 @@
  15.121  lemma ORRIGHT1_eqvt_coname:
  15.122    fixes pi::"coname prm"
  15.123    shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
  15.124 -apply(auto simp add: perm_set_def)
  15.125 +apply(auto simp add: perm_set_eq)
  15.126  apply(rule_tac x="pi\<bullet>a" in exI) 
  15.127  apply(rule_tac x="pi\<bullet>b" in exI) 
  15.128  apply(rule_tac x="pi\<bullet>M" in exI)
  15.129 @@ -10775,7 +10775,7 @@
  15.130  lemma ORRIGHT2_eqvt_name:
  15.131    fixes pi::"name prm"
  15.132    shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
  15.133 -apply(auto simp add: perm_set_def)
  15.134 +apply(auto simp add: perm_set_eq)
  15.135  apply(rule_tac x="pi\<bullet>a" in exI) 
  15.136  apply(rule_tac x="pi\<bullet>b" in exI) 
  15.137  apply(rule_tac x="pi\<bullet>M" in exI)
  15.138 @@ -10801,7 +10801,7 @@
  15.139  lemma ORRIGHT2_eqvt_coname:
  15.140    fixes pi::"coname prm"
  15.141    shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
  15.142 -apply(auto simp add: perm_set_def)
  15.143 +apply(auto simp add: perm_set_eq)
  15.144  apply(rule_tac x="pi\<bullet>a" in exI) 
  15.145  apply(rule_tac x="pi\<bullet>b" in exI) 
  15.146  apply(rule_tac x="pi\<bullet>M" in exI)
  15.147 @@ -10838,7 +10838,7 @@
  15.148  lemma IMPRIGHT_eqvt_name:
  15.149    fixes pi::"name prm"
  15.150    shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
  15.151 -apply(auto simp add: perm_set_def)
  15.152 +apply(auto simp add: perm_set_eq)
  15.153  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.154  apply(rule_tac x="pi\<bullet>a" in exI)
  15.155  apply(rule_tac x="pi\<bullet>b" in exI)
  15.156 @@ -10898,7 +10898,7 @@
  15.157  lemma IMPRIGHT_eqvt_coname:
  15.158    fixes pi::"coname prm"
  15.159    shows "(pi\<bullet>(IMPRIGHT (A IMP B) X Y Z U)) = IMPRIGHT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y) (pi\<bullet>Z) (pi\<bullet>U)"
  15.160 -apply(auto simp add: perm_set_def)
  15.161 +apply(auto simp add: perm_set_eq)
  15.162  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.163  apply(rule_tac x="pi\<bullet>a" in exI)
  15.164  apply(rule_tac x="pi\<bullet>b" in exI)
  15.165 @@ -10966,7 +10966,7 @@
  15.166  lemma IMPLEFT_eqvt_name:
  15.167    fixes pi::"name prm"
  15.168    shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
  15.169 -apply(auto simp add: perm_set_def)
  15.170 +apply(auto simp add: perm_set_eq)
  15.171  apply(rule_tac x="pi\<bullet>xb" in exI) 
  15.172  apply(rule_tac x="pi\<bullet>a" in exI)
  15.173  apply(rule_tac x="pi\<bullet>y" in exI) 
  15.174 @@ -11001,7 +11001,7 @@
  15.175  lemma IMPLEFT_eqvt_coname:
  15.176    fixes pi::"coname prm"
  15.177    shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
  15.178 -apply(auto simp add: perm_set_def)
  15.179 +apply(auto simp add: perm_set_eq)
  15.180  apply(rule_tac x="pi\<bullet>xb" in exI) 
  15.181  apply(rule_tac x="pi\<bullet>a" in exI)
  15.182  apply(rule_tac x="pi\<bullet>y" in exI) 
  15.183 @@ -11098,16 +11098,6 @@
  15.184    shows "x\<in>(X\<inter>Y) = (x\<in>X \<and> x\<in>Y)"
  15.185  by blast
  15.186  
  15.187 -lemma pt_Collect_eqvt:
  15.188 -  fixes pi::"'x prm"
  15.189 -  assumes pt: "pt TYPE('a) TYPE('x)"
  15.190 -  and     at: "at TYPE('x)"
  15.191 -  shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
  15.192 -apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
  15.193 -apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  15.194 -apply(simp add: pt_pi_rev[OF pt, OF at])
  15.195 -done
  15.196 -
  15.197  lemma big_inter_eqvt:
  15.198    fixes pi1::"name prm"
  15.199    and   X::"('a::pt_name) set set"
  15.200 @@ -11115,7 +11105,7 @@
  15.201    and   Y::"('b::pt_coname) set set"
  15.202    shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
  15.203    and   "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
  15.204 -apply(auto simp add: perm_set_def)
  15.205 +apply(auto simp add: perm_set_eq)
  15.206  apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
  15.207  apply(perm_simp)
  15.208  apply(rule ballI)
  15.209 @@ -11150,7 +11140,7 @@
  15.210    shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
  15.211    and   "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
  15.212  apply(simp add: lfp_def)
  15.213 -apply(simp add: Inf_set_def)
  15.214 +apply(simp add: Inf_set_eq)
  15.215  apply(simp add: big_inter_eqvt)
  15.216  apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
  15.217  apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
  15.218 @@ -11162,7 +11152,7 @@
  15.219  apply(drule subseteq_eqvt(1)[THEN iffD2])
  15.220  apply(simp add: perm_bool)
  15.221  apply(simp add: lfp_def)
  15.222 -apply(simp add: Inf_set_def)
  15.223 +apply(simp add: Inf_set_eq)
  15.224  apply(simp add: big_inter_eqvt)
  15.225  apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
  15.226  apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
  15.227 @@ -11345,7 +11335,7 @@
  15.228    fixes pi::"name prm"
  15.229    shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
  15.230    and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
  15.231 -apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
  15.232 +apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
  15.233  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.234  apply(rule_tac x="pi\<bullet>M" in exI)
  15.235  apply(simp)
  15.236 @@ -11400,7 +11390,7 @@
  15.237    fixes pi::"coname prm"
  15.238    shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)" 
  15.239    and   "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)" 
  15.240 -apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
  15.241 +apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
  15.242  apply(rule_tac x="pi\<bullet>xb" in exI)
  15.243  apply(rule_tac x="pi\<bullet>M" in exI)
  15.244  apply(simp)
  15.245 @@ -11460,7 +11450,7 @@
  15.246    { case 1 show ?case 
  15.247        apply -
  15.248        apply(simp add: lfp_eqvt)
  15.249 -      apply(simp add: perm_fun_def)
  15.250 +      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.251        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
  15.252        apply(perm_simp)
  15.253      done
  15.254 @@ -11471,7 +11461,7 @@
  15.255        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
  15.256        apply(simp add: lfp_eqvt)
  15.257        apply(simp add: comp_def)
  15.258 -      apply(simp add: perm_fun_def)
  15.259 +      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.260        apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
  15.261        apply(perm_simp)
  15.262        done
  15.263 @@ -11484,7 +11474,7 @@
  15.264      apply -
  15.265      apply(simp only: lfp_eqvt)
  15.266      apply(simp only: comp_def)
  15.267 -    apply(simp only: perm_fun_def)
  15.268 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.269      apply(simp only: NEGc.simps NEGn.simps)
  15.270      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
  15.271      apply(perm_simp add: ih1 ih2)
  15.272 @@ -11504,7 +11494,7 @@
  15.273      apply -
  15.274      apply(simp only: lfp_eqvt)
  15.275      apply(simp only: comp_def)
  15.276 -    apply(simp only: perm_fun_def)
  15.277 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.278      apply(simp only: NEGc.simps NEGn.simps)
  15.279      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name 
  15.280                       ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
  15.281 @@ -11526,7 +11516,7 @@
  15.282      apply -
  15.283      apply(simp only: lfp_eqvt)
  15.284      apply(simp only: comp_def)
  15.285 -    apply(simp only: perm_fun_def)
  15.286 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.287      apply(simp only: NEGc.simps NEGn.simps)
  15.288      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name 
  15.289                       ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
  15.290 @@ -11548,7 +11538,7 @@
  15.291      apply -
  15.292      apply(simp only: lfp_eqvt)
  15.293      apply(simp only: comp_def)
  15.294 -    apply(simp only: perm_fun_def)
  15.295 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.296      apply(simp only: NEGc.simps NEGn.simps)
  15.297      apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
  15.298      apply(perm_simp add: ih1 ih2 ih3 ih4)
  15.299 @@ -11570,7 +11560,7 @@
  15.300    { case 1 show ?case 
  15.301        apply -
  15.302        apply(simp add: lfp_eqvt)
  15.303 -      apply(simp add: perm_fun_def)
  15.304 +      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.305        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
  15.306        apply(perm_simp)
  15.307      done
  15.308 @@ -11581,7 +11571,7 @@
  15.309        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
  15.310        apply(simp add: lfp_eqvt)
  15.311        apply(simp add: comp_def)
  15.312 -      apply(simp add: perm_fun_def)
  15.313 +      apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.314        apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
  15.315        apply(perm_simp)
  15.316        done
  15.317 @@ -11594,7 +11584,7 @@
  15.318      apply -
  15.319      apply(simp only: lfp_eqvt)
  15.320      apply(simp only: comp_def)
  15.321 -    apply(simp only: perm_fun_def)
  15.322 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.323      apply(simp only: NEGc.simps NEGn.simps)
  15.324      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname 
  15.325              NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
  15.326 @@ -11616,7 +11606,7 @@
  15.327      apply -
  15.328      apply(simp only: lfp_eqvt)
  15.329      apply(simp only: comp_def)
  15.330 -    apply(simp only: perm_fun_def)
  15.331 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.332      apply(simp only: NEGc.simps NEGn.simps)
  15.333      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname 
  15.334                       ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
  15.335 @@ -11638,7 +11628,7 @@
  15.336      apply -
  15.337      apply(simp only: lfp_eqvt)
  15.338      apply(simp only: comp_def)
  15.339 -    apply(simp only: perm_fun_def)
  15.340 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.341      apply(simp only: NEGc.simps NEGn.simps)
  15.342      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname 
  15.343                       ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
  15.344 @@ -11660,7 +11650,7 @@
  15.345      apply -
  15.346      apply(simp only: lfp_eqvt)
  15.347      apply(simp only: comp_def)
  15.348 -    apply(simp only: perm_fun_def)
  15.349 +    apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
  15.350      apply(simp only: NEGc.simps NEGn.simps)
  15.351      apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname 
  15.352           IMPLEFT_eqvt_coname)
    16.1 --- a/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:56:58 2008 +0200
    16.2 +++ b/src/HOL/Nominal/Examples/SOS.thy	Wed May 07 10:57:19 2008 +0200
    16.3 @@ -422,7 +422,7 @@
    16.4    shows "(pi\<bullet>x)\<in>V T"
    16.5  using a
    16.6  apply(nominal_induct T arbitrary: pi x rule: ty.induct)
    16.7 -apply(auto simp add: trm.inject perm_set_def)
    16.8 +apply(auto simp add: trm.inject)
    16.9  apply(simp add: eqvts)
   16.10  apply(rule_tac x="pi\<bullet>xa" in exI)
   16.11  apply(rule_tac x="pi\<bullet>e" in exI)
    17.1 --- a/src/HOL/Nominal/Examples/Support.thy	Wed May 07 10:56:58 2008 +0200
    17.2 +++ b/src/HOL/Nominal/Examples/Support.thy	Wed May 07 10:57:19 2008 +0200
    17.3 @@ -100,14 +100,14 @@
    17.4      proof (cases "x\<in>S")
    17.5        case True
    17.6        have "x\<in>S" by fact
    17.7 -      hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
    17.8 +      hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
    17.9        with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
   17.10        hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
   17.11        then show "x\<in>(supp S)" by (simp add: supp_def)
   17.12      next
   17.13        case False
   17.14        have "x\<notin>S" by fact
   17.15 -      hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
   17.16 +      hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
   17.17        with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
   17.18        hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
   17.19        then show "x\<in>(supp S)" by (simp add: supp_def)
   17.20 @@ -131,7 +131,7 @@
   17.21    shows "supp (UNIV::atom set) = ({}::atom set)"
   17.22  proof -
   17.23    have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
   17.24 -    by (auto simp add: perm_set_def calc_atm)
   17.25 +    by (auto simp add: perm_set_eq calc_atm)
   17.26    then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
   17.27  qed
   17.28  
    18.1 --- a/src/HOL/Nominal/Nominal.thy	Wed May 07 10:56:58 2008 +0200
    18.2 +++ b/src/HOL/Nominal/Nominal.thy	Wed May 07 10:57:19 2008 +0200
    18.3 @@ -29,61 +29,6 @@
    18.4  constdefs
    18.5    "perm_aux pi x \<equiv> pi\<bullet>x"
    18.6  
    18.7 -(* permutation on sets *)
    18.8 -defs (unchecked overloaded)
    18.9 -  perm_set_def:  "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x | x. x\<in>X}"
   18.10 -
   18.11 -lemma empty_eqvt:
   18.12 -  shows "pi\<bullet>{} = {}"
   18.13 -  by (simp add: perm_set_def)
   18.14 -
   18.15 -lemma union_eqvt:
   18.16 -  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   18.17 -  by (auto simp add: perm_set_def)
   18.18 -
   18.19 -lemma insert_eqvt:
   18.20 -  shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
   18.21 -  by (auto simp add: perm_set_def)
   18.22 -
   18.23 -(* permutation on units and products *)
   18.24 -primrec (unchecked perm_unit)
   18.25 -  "pi\<bullet>() = ()"
   18.26 -  
   18.27 -primrec (unchecked perm_prod)
   18.28 -  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
   18.29 -
   18.30 -lemma fst_eqvt:
   18.31 -  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
   18.32 - by (cases x) simp
   18.33 -
   18.34 -lemma snd_eqvt:
   18.35 -  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
   18.36 - by (cases x) simp
   18.37 -
   18.38 -(* permutation on lists *)
   18.39 -primrec (unchecked perm_list)
   18.40 -  nil_eqvt:  "pi\<bullet>[]     = []"
   18.41 -  cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
   18.42 -
   18.43 -lemma append_eqvt:
   18.44 -  fixes pi :: "'x prm"
   18.45 -  and   l1 :: "'a list"
   18.46 -  and   l2 :: "'a list"
   18.47 -  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
   18.48 -  by (induct l1) auto
   18.49 -
   18.50 -lemma rev_eqvt:
   18.51 -  fixes pi :: "'x prm"
   18.52 -  and   l  :: "'a list"
   18.53 -  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
   18.54 -  by (induct l) (simp_all add: append_eqvt)
   18.55 -
   18.56 -lemma set_eqvt:
   18.57 -  fixes pi :: "'x prm"
   18.58 -  and   xs :: "'a list"
   18.59 -  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
   18.60 -by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
   18.61 -
   18.62  (* permutation on functions *)
   18.63  defs (unchecked overloaded)
   18.64    perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
   18.65 @@ -129,6 +74,48 @@
   18.66    shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
   18.67    by (simp add: perm_bool)
   18.68  
   18.69 +(* permutation on sets *)
   18.70 +lemma empty_eqvt:
   18.71 +  shows "pi\<bullet>{} = {}"
   18.72 +  by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq)
   18.73 +
   18.74 +lemma union_eqvt:
   18.75 +  shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
   18.76 +  by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
   18.77 +
   18.78 +(* permutation on units and products *)
   18.79 +primrec (unchecked perm_unit)
   18.80 +  "pi\<bullet>() = ()"
   18.81 +  
   18.82 +primrec (unchecked perm_prod)
   18.83 +  "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
   18.84 +
   18.85 +lemma fst_eqvt:
   18.86 +  "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
   18.87 + by (cases x) simp
   18.88 +
   18.89 +lemma snd_eqvt:
   18.90 +  "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
   18.91 + by (cases x) simp
   18.92 +
   18.93 +(* permutation on lists *)
   18.94 +primrec (unchecked perm_list)
   18.95 +  nil_eqvt:  "pi\<bullet>[]     = []"
   18.96 +  cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
   18.97 +
   18.98 +lemma append_eqvt:
   18.99 +  fixes pi :: "'x prm"
  18.100 +  and   l1 :: "'a list"
  18.101 +  and   l2 :: "'a list"
  18.102 +  shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
  18.103 +  by (induct l1) auto
  18.104 +
  18.105 +lemma rev_eqvt:
  18.106 +  fixes pi :: "'x prm"
  18.107 +  and   l  :: "'a list"
  18.108 +  shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
  18.109 +  by (induct l) (simp_all add: append_eqvt)
  18.110 +
  18.111  (* permutation on options *)
  18.112  
  18.113  primrec (unchecked perm_option)
  18.114 @@ -196,11 +183,7 @@
  18.115  
  18.116  lemma supp_set_empty:
  18.117    shows "supp {} = {}"
  18.118 -  by (force simp add: supp_def perm_set_def)
  18.119 -
  18.120 -lemma supp_singleton:
  18.121 -  shows "supp {x} = supp x"
  18.122 -  by (force simp add: supp_def perm_set_def)
  18.123 +  by (force simp add: supp_def empty_eqvt)
  18.124  
  18.125  lemma supp_prod: 
  18.126    fixes x :: "'a"
  18.127 @@ -284,10 +267,6 @@
  18.128    shows "a\<sharp>{}"
  18.129    by (simp add: fresh_def supp_set_empty)
  18.130  
  18.131 -lemma fresh_singleton:
  18.132 -  shows "a\<sharp>{x} = a\<sharp>x"
  18.133 -  by (simp add: fresh_def supp_singleton)
  18.134 -
  18.135  lemma fresh_unit:
  18.136    shows "a\<sharp>()"
  18.137    by (simp add: fresh_def supp_unit)
  18.138 @@ -1026,15 +1005,6 @@
  18.139  section {* permutation type instances *}
  18.140  (* ===================================*)
  18.141  
  18.142 -lemma pt_set_inst:
  18.143 -  assumes pt: "pt TYPE('a) TYPE('x)"
  18.144 -  shows  "pt TYPE('a set) TYPE('x)"
  18.145 -apply(simp add: pt_def)
  18.146 -apply(simp_all add: perm_set_def)
  18.147 -apply(simp add: pt1[OF pt])
  18.148 -apply(force simp add: pt2[OF pt] pt3[OF pt])
  18.149 -done
  18.150 -
  18.151  lemma pt_list_nil: 
  18.152    fixes xs :: "'a list"
  18.153    assumes pt: "pt TYPE('a) TYPE ('x)"
  18.154 @@ -1270,6 +1240,42 @@
  18.155  apply(rule pt1[OF pt])
  18.156  done
  18.157  
  18.158 +lemma perm_set_eq:
  18.159 +  assumes pt: "pt TYPE('a) TYPE('x)"
  18.160 +  and at: "at TYPE('x)" 
  18.161 +  shows "(pi::'x prm)\<bullet>(X::'a set) = {pi\<bullet>x | x. x\<in>X}"
  18.162 +  apply (auto simp add: perm_fun_def perm_bool mem_def)
  18.163 +  apply (rule_tac x="rev pi \<bullet> x" in exI)
  18.164 +  apply (simp add: pt_pi_rev [OF pt at])
  18.165 +  apply (simp add: pt_rev_pi [OF pt at])
  18.166 +  done
  18.167 +
  18.168 +lemma insert_eqvt:
  18.169 +  assumes pt: "pt TYPE('a) TYPE('x)"
  18.170 +  and at: "at TYPE('x)" 
  18.171 +  shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
  18.172 +  by (auto simp add: perm_set_eq [OF pt at])
  18.173 +
  18.174 +lemma set_eqvt:
  18.175 +  fixes pi :: "'x prm"
  18.176 +  and   xs :: "'a list"
  18.177 +  assumes pt: "pt TYPE('a) TYPE('x)"
  18.178 +  and at: "at TYPE('x)" 
  18.179 +  shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
  18.180 +by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
  18.181 +
  18.182 +lemma supp_singleton:
  18.183 +  assumes pt: "pt TYPE('a) TYPE('x)"
  18.184 +  and at: "at TYPE('x)" 
  18.185 +  shows "(supp {x::'a} :: 'x set) = supp x"
  18.186 +  by (force simp add: supp_def perm_set_eq [OF pt at])
  18.187 +
  18.188 +lemma fresh_singleton:
  18.189 +  assumes pt: "pt TYPE('a) TYPE('x)"
  18.190 +  and at: "at TYPE('x)" 
  18.191 +  shows "(a::'x)\<sharp>{x::'a} = a\<sharp>x"
  18.192 +  by (simp add: fresh_def supp_singleton [OF pt at])
  18.193 +
  18.194  lemma pt_set_bij1:
  18.195    fixes pi :: "'x prm"
  18.196    and   x  :: "'a"
  18.197 @@ -1277,7 +1283,7 @@
  18.198    assumes pt: "pt TYPE('a) TYPE('x)"
  18.199    and     at: "at TYPE('x)"
  18.200    shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
  18.201 -  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  18.202 +  by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  18.203  
  18.204  lemma pt_set_bij1a:
  18.205    fixes pi :: "'x prm"
  18.206 @@ -1286,7 +1292,7 @@
  18.207    assumes pt: "pt TYPE('a) TYPE('x)"
  18.208    and     at: "at TYPE('x)"
  18.209    shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
  18.210 -  by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  18.211 +  by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
  18.212  
  18.213  lemma pt_set_bij:
  18.214    fixes pi :: "'x prm"
  18.215 @@ -1295,7 +1301,7 @@
  18.216    assumes pt: "pt TYPE('a) TYPE('x)"
  18.217    and     at: "at TYPE('x)"
  18.218    shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
  18.219 -  by (simp add: perm_set_def pt_bij[OF pt, OF at])
  18.220 +  by (simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
  18.221  
  18.222  lemma pt_in_eqvt:
  18.223    fixes pi :: "'x prm"
  18.224 @@ -1342,7 +1348,7 @@
  18.225    assumes pt: "pt TYPE('a) TYPE('x)"
  18.226    and     at: "at TYPE('x)"
  18.227    shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
  18.228 -by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
  18.229 +by (auto simp add: perm_set_eq [OF pt at] perm_bool pt_bij[OF pt, OF at])
  18.230  
  18.231  lemma pt_set_diff_eqvt:
  18.232    fixes X::"'a set"
  18.233 @@ -1351,14 +1357,14 @@
  18.234    assumes pt: "pt TYPE('a) TYPE('x)"
  18.235    and     at: "at TYPE('x)"
  18.236    shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
  18.237 -  by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
  18.238 +  by (auto simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
  18.239  
  18.240  lemma pt_Collect_eqvt:
  18.241    fixes pi::"'x prm"
  18.242    assumes pt: "pt TYPE('a) TYPE('x)"
  18.243    and     at: "at TYPE('x)"
  18.244    shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
  18.245 -apply(auto simp add: perm_set_def  pt_rev_pi[OF pt, OF at])
  18.246 +apply(auto simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at])
  18.247  apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  18.248  apply(simp add: pt_pi_rev[OF pt, OF at])
  18.249  done
  18.250 @@ -1402,7 +1408,7 @@
  18.251    and     at: "at TYPE('y)"
  18.252    shows "finite (pi\<bullet>X) = finite X"
  18.253  proof -
  18.254 -  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
  18.255 +  have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_eq [OF pt at])
  18.256    show ?thesis
  18.257    proof (rule iffI)
  18.258      assume "finite (pi\<bullet>X)"
  18.259 @@ -1432,17 +1438,17 @@
  18.260    and     cp:  "cp TYPE('a) TYPE('x) TYPE('y)"
  18.261    shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
  18.262  proof -
  18.263 -  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
  18.264 +  have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_eq [OF ptb at])
  18.265    also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}" 
  18.266    proof (rule Collect_permI, rule allI, rule iffI)
  18.267      fix a
  18.268      assume "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}"
  18.269      hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  18.270 -    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_def)
  18.271 +    thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x  \<noteq> x}" by (simp add: perm_set_eq [OF ptb at])
  18.272    next
  18.273      fix a
  18.274      assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
  18.275 -    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
  18.276 +    hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_eq [OF ptb at])
  18.277      thus "infinite {b::'y. [(a,b)]\<bullet>x  \<noteq> x}" 
  18.278        by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
  18.279    qed
  18.280 @@ -1550,10 +1556,10 @@
  18.281  apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  18.282  apply(drule_tac x="pi\<bullet>xa" in bspec)
  18.283  apply(simp add: pt_set_bij1[OF ptb, OF at])
  18.284 -apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
  18.285 +apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
  18.286  apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
  18.287  apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
  18.288 -apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
  18.289 +apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
  18.290  apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
  18.291  done
  18.292  
  18.293 @@ -2012,7 +2018,8 @@
  18.294    assumes at: "at TYPE('x)"
  18.295    shows "X supports X"
  18.296  proof -
  18.297 -  have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X" by (auto simp add: perm_set_def at_calc[OF at])
  18.298 +  have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X"
  18.299 +    by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
  18.300    then show ?thesis by (simp add: supports_def)
  18.301  qed
  18.302  
  18.303 @@ -2023,7 +2030,7 @@
  18.304    using a1 a2 
  18.305    apply auto
  18.306    apply (subgoal_tac "infinite (X - {b\<in>X. P b})")
  18.307 -  apply (simp add: set_diff_def)
  18.308 +  apply (simp add: set_diff_eq)
  18.309    apply (simp add: Diff_infinite_finite)
  18.310    done
  18.311  
  18.312 @@ -2038,7 +2045,8 @@
  18.313    have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
  18.314    { fix a::"'x"
  18.315      assume asm: "a\<in>X"
  18.316 -    hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X" by (auto simp add: perm_set_def at_calc[OF at])
  18.317 +    hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X"
  18.318 +      by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
  18.319      with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection)
  18.320      hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto)
  18.321      hence "a\<in>(supp X)" by (simp add: supp_def)
  18.322 @@ -2259,7 +2267,7 @@
  18.323    proof (rule equalityI)
  18.324      case goal1
  18.325      show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
  18.326 -      apply(auto simp add: perm_set_def)
  18.327 +      apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
  18.328        apply(rule_tac x="pi\<bullet>xb" in exI)
  18.329        apply(rule conjI)
  18.330        apply(rule_tac x="xb" in exI)
  18.331 @@ -2275,7 +2283,7 @@
  18.332    next
  18.333      case goal2
  18.334      show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
  18.335 -      apply(auto simp add: perm_set_def)
  18.336 +      apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
  18.337        apply(rule_tac x="(rev pi)\<bullet>x" in exI)
  18.338        apply(rule conjI)
  18.339        apply(simp add: pt_pi_rev[OF pt_x, OF at])
  18.340 @@ -2294,7 +2302,7 @@
  18.341    and     at: "at TYPE('x)"
  18.342    shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
  18.343    apply(simp add: X_to_Un_supp_def)
  18.344 -  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
  18.345 +  apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
  18.346    apply(simp add: pt_perm_supp[OF pt, OF at])
  18.347    apply(simp add: pt_pi_rev[OF pt, OF at])
  18.348    done
  18.349 @@ -2308,7 +2316,7 @@
  18.350    apply(rule allI)+
  18.351    apply(rule impI)
  18.352    apply(erule conjE)
  18.353 -  apply(simp add: perm_set_def)
  18.354 +  apply(simp add: perm_set_eq [OF pt at])
  18.355    apply(auto)
  18.356    apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
  18.357    apply(simp)
  18.358 @@ -2339,9 +2347,9 @@
  18.359  proof -
  18.360    have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"  
  18.361      apply(rule pt_empty_supp_fun_subset)
  18.362 -    apply(force intro: pt_set_inst at_pt_inst pt at)+
  18.363 +    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
  18.364      apply(rule pt_eqvt_fun2b)
  18.365 -    apply(force intro: pt_set_inst at_pt_inst pt at)+
  18.366 +    apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
  18.367      apply(rule allI)+
  18.368      apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
  18.369      done
  18.370 @@ -2392,7 +2400,7 @@
  18.371    also have "\<dots> = (supp {x})\<union>(supp X)"
  18.372      by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
  18.373    finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)" 
  18.374 -    by (simp add: supp_singleton)
  18.375 +    by (simp add: supp_singleton [OF pt at])
  18.376  qed
  18.377  
  18.378  lemma fresh_fin_union:
  18.379 @@ -2477,17 +2485,6 @@
  18.380  apply(auto)
  18.381  done
  18.382  
  18.383 -lemma cp_set_inst:
  18.384 -  assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  18.385 -  shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
  18.386 -using c1
  18.387 -apply(simp add: cp_def)
  18.388 -apply(auto)
  18.389 -apply(auto simp add: perm_set_def)
  18.390 -apply(rule_tac x="pi2\<bullet>xc" in exI)
  18.391 -apply(auto)
  18.392 -done
  18.393 -
  18.394  lemma cp_option_inst:
  18.395    assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
  18.396    shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
  18.397 @@ -3369,7 +3366,7 @@
  18.398    plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
  18.399    
  18.400    (* sets *)
  18.401 -  union_eqvt empty_eqvt insert_eqvt set_eqvt 
  18.402 +  union_eqvt empty_eqvt
  18.403    
  18.404   
  18.405  (* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
    19.1 --- a/src/HOL/Nominal/nominal_package.ML	Wed May 07 10:56:58 2008 +0200
    19.2 +++ b/src/HOL/Nominal/nominal_package.ML	Wed May 07 10:57:19 2008 +0200
    19.3 @@ -1183,8 +1183,9 @@
    19.4  
    19.5      val ind_prems' =
    19.6        map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
    19.7 -        HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T -->
    19.8 -          HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
    19.9 +        HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
   19.10 +          (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
   19.11 +            HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
   19.12        List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
   19.13          map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
   19.14            HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
    20.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed May 07 10:56:58 2008 +0200
    20.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed May 07 10:57:19 2008 +0200
    20.3 @@ -290,7 +290,7 @@
    20.4  fun finite_guess_tac tactical ss i st =
    20.5      let val goal = List.nth(cprems_of st, i-1)
    20.6      in
    20.7 -      case Logic.strip_assums_concl (term_of goal) of
    20.8 +      case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
    20.9            _ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
   20.10            let
   20.11              val cert = Thm.cterm_of (Thm.theory_of_thm st);
   20.12 @@ -301,7 +301,8 @@
   20.13                  HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
   20.14                (vs, HOLogic.unit);
   20.15              val s' = list_abs (ps,
   20.16 -              Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
   20.17 +              Const ("Nominal.supp", fastype_of1 (Ts, s) -->
   20.18 +                snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
   20.19              val supports_rule' = Thm.lift_rule goal supports_rule;
   20.20              val _ $ (_ $ S $ _) =
   20.21                Logic.strip_assums_concl (hd (prems_of supports_rule'));
    21.1 --- a/src/HOL/Real/PReal.thy	Wed May 07 10:56:58 2008 +0200
    21.2 +++ b/src/HOL/Real/PReal.thy	Wed May 07 10:57:19 2008 +0200
    21.3 @@ -202,7 +202,7 @@
    21.4  
    21.5  (* Axiom 'order_less_le' of class 'order': *)
    21.6  lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
    21.7 -by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
    21.8 +by (simp add: preal_le_def preal_less_def Rep_preal_inject less_le)
    21.9  
   21.10  instance preal :: order
   21.11    by intro_classes
   21.12 @@ -943,7 +943,7 @@
   21.13  
   21.14  text{*at last, Gleason prop. 9-3.5(iii) page 123*}
   21.15  lemma preal_self_less_add_left: "(R::preal) < R + S"
   21.16 -apply (unfold preal_less_def psubset_def)
   21.17 +apply (unfold preal_less_def less_le)
   21.18  apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
   21.19  done
   21.20  
    22.1 --- a/src/HOL/Subst/Unify.thy	Wed May 07 10:56:58 2008 +0200
    22.2 +++ b/src/HOL/Subst/Unify.thy	Wed May 07 10:57:19 2008 +0200
    22.3 @@ -117,7 +117,7 @@
    22.4  apply blast
    22.5  txt{*@{text finite_psubset} case*}
    22.6  apply (simp add: unifyRel_def lex_prod_def)
    22.7 -apply (simp add: finite_psubset_def finite_vars_of psubset_def)
    22.8 +apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
    22.9  apply blast
   22.10  txt{*Final case, also @{text finite_psubset}*}
   22.11  apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
    23.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 07 10:56:58 2008 +0200
    23.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed May 07 10:57:19 2008 +0200
    23.3 @@ -375,12 +375,16 @@
    23.4                 (map (pair "x") Ts, S $ app_bnds f i)),
    23.5               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    23.6                 r $ (a $ app_bnds f i)), f))))
    23.7 -            (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
    23.8 +            (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
    23.9 +               REPEAT (etac allE 1), rtac thm 1, atac 1])
   23.10            end
   23.11        in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
   23.12  
   23.13      (* prove  inj dt_Rep_i  and  dt_Rep_i x : dt_rep_set_i *)
   23.14  
   23.15 +    val fun_congs = map (fn T => make_elim (Drule.instantiate'
   23.16 +      [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
   23.17 +
   23.18      fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
   23.19        let
   23.20          val (_, (tname, _, _)) = hd ds;
   23.21 @@ -422,7 +426,7 @@
   23.22                          [REPEAT (rtac ext 1),
   23.23                           REPEAT (eresolve_tac (mp :: allE ::
   23.24                             map make_elim (Suml_inject :: Sumr_inject ::
   23.25 -                             Lim_inject :: fun_cong :: inj_thms')) 1),
   23.26 +                             Lim_inject :: inj_thms') @ fun_congs) 1),
   23.27                           atac 1]))])])])]);
   23.28  
   23.29          val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
    24.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed May 07 10:56:58 2008 +0200
    24.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed May 07 10:57:19 2008 +0200
    24.3 @@ -191,11 +191,11 @@
    24.4      | _ => default)
    24.5    end;
    24.6  
    24.7 -datatype indprem = Prem of term list * term | Sidecond of term;
    24.8 +datatype indprem = Prem of term list * term * bool | Sidecond of term;
    24.9  
   24.10  fun select_mode_prem thy modes vs ps =
   24.11    find_first (is_some o snd) (ps ~~ map
   24.12 -    (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
   24.13 +    (fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) =>
   24.14            let
   24.15              val (in_ts, out_ts) = get_args is 1 us;
   24.16              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
   24.17 @@ -208,7 +208,9 @@
   24.18              term_vs t subset vs andalso
   24.19              forall is_eqT dupTs
   24.20            end)
   24.21 -            (modes_of modes t handle Option => [Mode (([], []), [], [])])
   24.22 +            (if is_set then [Mode (([], []), [], [])]
   24.23 +             else modes_of modes t handle Option =>
   24.24 +               error ("Bad predicate: " ^ Sign.string_of_term thy t))
   24.25        | Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
   24.26            else NONE) ps);
   24.27  
   24.28 @@ -221,7 +223,7 @@
   24.29        | check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
   24.30            NONE => NONE
   24.31          | SOME (x, _) => check_mode_prems
   24.32 -            (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
   24.33 +            (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
   24.34              (filter_out (equal x) ps));
   24.35      val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
   24.36      val in_vs = terms_vs in_ts;
   24.37 @@ -390,21 +392,21 @@
   24.38              val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
   24.39            in
   24.40              (case p of
   24.41 -               Prem (us, t) =>
   24.42 +               Prem (us, t, is_set) =>
   24.43                   let
   24.44                     val (in_ts, out_ts''') = get_args js 1 us;
   24.45                     val (gr2, in_ps) = foldl_map
   24.46                       (invoke_codegen thy defs dep module true) (gr1, in_ts);
   24.47 -                   val (gr3, ps) = (case body_type (fastype_of t) of
   24.48 -                       Type ("bool", []) =>
   24.49 +                   val (gr3, ps) =
   24.50 +                     if not is_set then
   24.51                         apsnd (fn ps => ps @
   24.52                             (if null in_ps then [] else [Pretty.brk 1]) @
   24.53                             separate (Pretty.brk 1) in_ps)
   24.54                           (compile_expr thy defs dep module false modes
   24.55                             (gr2, (mode, t)))
   24.56 -                     | _ =>
   24.57 +                     else
   24.58                         apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p])
   24.59 -                           (invoke_codegen thy defs dep module true (gr2, t)));
   24.60 +                           (invoke_codegen thy defs dep module true (gr2, t));
   24.61                     val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
   24.62                   in
   24.63                     (gr4, compile_match (snd nvs) eq_ps out_ps
   24.64 @@ -504,16 +506,16 @@
   24.65        fun get_nparms s = if s mem names then SOME nparms else
   24.66          Option.map #3 (get_clauses thy s);
   24.67  
   24.68 -      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], u)
   24.69 -        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq)
   24.70 +      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
   24.71 +        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
   24.72          | dest_prem (_ $ t) =
   24.73              (case strip_comb t of
   24.74 -               (v as Var _, ts) => if v mem args then Prem (ts, v) else Sidecond t
   24.75 +               (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
   24.76               | (c as Const (s, _), ts) => (case get_nparms s of
   24.77                   NONE => Sidecond t
   24.78                 | SOME k =>
   24.79                     let val (ts1, ts2) = chop k ts
   24.80 -                   in Prem (ts2, list_comb (c, ts1)) end)
   24.81 +                   in Prem (ts2, list_comb (c, ts1), false) end)
   24.82               | _ => Sidecond t);
   24.83  
   24.84        fun add_clause intr (clauses, arities) =
    25.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:56:58 2008 +0200
    25.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Wed May 07 10:57:19 2008 +0200
    25.3 @@ -237,7 +237,7 @@
    25.4          NONE => thm' RS sym
    25.5        | SOME fs' =>
    25.6            let
    25.7 -            val U = HOLogic.dest_setT (body_type T);
    25.8 +            val (_, U) = split_last (binder_types T);
    25.9              val Ts = HOLogic.prodT_factors' fs' U;
   25.10              (* FIXME: should cterm_instantiate increment indexes? *)
   25.11              val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
   25.12 @@ -413,7 +413,7 @@
   25.13        | infer (t $ u) = infer t #> infer u
   25.14        | infer _ = I;
   25.15      val new_arities = filter_out
   25.16 -      (fn (x as Free (_, Type ("fun", _)), _) => x mem params
   25.17 +      (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
   25.18          | _ => false) (fold (snd #> infer) intros []);
   25.19      val params' = map (fn x => (case AList.lookup op = new_arities x of
   25.20          SOME fs =>
   25.21 @@ -437,7 +437,7 @@
   25.22      val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
   25.23        let
   25.24          val fs = the_default [] (AList.lookup op = new_arities c);
   25.25 -        val U = HOLogic.dest_setT (body_type T);
   25.26 +        val (_, U) = split_last (binder_types T);
   25.27          val Ts = HOLogic.prodT_factors' fs U;
   25.28          val c' = Free (s ^ "p",
   25.29            map fastype_of params1 @ Ts ---> HOLogic.boolT)
    26.1 --- a/src/HOL/UNITY/ELT.thy	Wed May 07 10:56:58 2008 +0200
    26.2 +++ b/src/HOL/UNITY/ELT.thy	Wed May 07 10:57:19 2008 +0200
    26.3 @@ -102,7 +102,7 @@
    26.4  apply (simp (no_asm_use) add: givenBy_eq_Collect)
    26.5  apply safe
    26.6  apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
    26.7 -unfolding set_diff_def
    26.8 +unfolding set_diff_eq
    26.9  apply auto
   26.10  done
   26.11  
    27.1 --- a/src/HOL/UNITY/Transformers.thy	Wed May 07 10:56:58 2008 +0200
    27.2 +++ b/src/HOL/UNITY/Transformers.thy	Wed May 07 10:57:19 2008 +0200
    27.3 @@ -88,7 +88,7 @@
    27.4  done
    27.5  
    27.6  lemma wens_Id [simp]: "wens F Id B = B"
    27.7 -by (simp add: wens_def gfp_def wp_def awp_def Sup_set_def, blast)
    27.8 +by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
    27.9  
   27.10  text{*These two theorems justify the claim that @{term wens} returns the
   27.11  weakest assertion satisfying the ensures property*}
   27.12 @@ -101,7 +101,7 @@
   27.13  
   27.14  lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
   27.15  by (simp add: wens_def gfp_def constrains_def awp_def wp_def
   27.16 -              ensures_def transient_def Sup_set_def, blast)
   27.17 +              ensures_def transient_def Sup_set_eq, blast)
   27.18  
   27.19  text{*These two results constitute assertion (4.13) of the thesis*}
   27.20  lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
   27.21 @@ -110,7 +110,7 @@
   27.22  done
   27.23  
   27.24  lemma wens_weakening: "B \<subseteq> wens F act B"
   27.25 -by (simp add: wens_def gfp_def Sup_set_def, blast)
   27.26 +by (simp add: wens_def gfp_def Sup_set_eq, blast)
   27.27  
   27.28  text{*Assertion (6), or 4.16 in the thesis*}
   27.29  lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
   27.30 @@ -120,7 +120,7 @@
   27.31  
   27.32  text{*Assertion 4.17 in the thesis*}
   27.33  lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
   27.34 -by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_def, blast)
   27.35 +by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
   27.36    --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
   27.37        is declared as an iff-rule, then it's almost impossible to prove. 
   27.38        One proof is via @{text meson} after expanding all definitions, but it's
   27.39 @@ -331,7 +331,7 @@
   27.40  
   27.41  lemma wens_single_eq:
   27.42       "wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
   27.43 -by (simp add: wens_def gfp_def wp_def Sup_set_def, blast)
   27.44 +by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
   27.45  
   27.46  
   27.47  text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
    28.1 --- a/src/HOLCF/CompactBasis.thy	Wed May 07 10:56:58 2008 +0200
    28.2 +++ b/src/HOLCF/CompactBasis.thy	Wed May 07 10:57:19 2008 +0200
    28.3 @@ -227,7 +227,7 @@
    28.4  
    28.5  lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
    28.6  unfolding principal_less_iff
    28.7 -by (simp add: less_def subset_def)
    28.8 +by (simp add: less_def subset_eq)
    28.9  
   28.10  lemma lub_principal_approxes: "principal ` approxes x <<| x"
   28.11  apply (rule is_lubI)
    29.1 --- a/src/HOLCF/ConvexPD.thy	Wed May 07 10:56:58 2008 +0200
    29.2 +++ b/src/HOLCF/ConvexPD.thy	Wed May 07 10:57:19 2008 +0200
    29.3 @@ -151,7 +151,7 @@
    29.4  by (rule Rep_convex_pd [simplified])
    29.5  
    29.6  lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
    29.7 -unfolding less_convex_pd_def less_set_def .
    29.8 +unfolding less_convex_pd_def less_set_eq .
    29.9  
   29.10  
   29.11  subsection {* Principal ideals *}
   29.12 @@ -179,12 +179,12 @@
   29.13  apply (rule ideal_Rep_convex_pd)
   29.14  apply (rule cont_Rep_convex_pd)
   29.15  apply (rule Rep_convex_principal)
   29.16 -apply (simp only: less_convex_pd_def less_set_def)
   29.17 +apply (simp only: less_convex_pd_def less_set_eq)
   29.18  done
   29.19  
   29.20  lemma convex_principal_less_iff [simp]:
   29.21    "(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
   29.22 -unfolding less_convex_pd_def Rep_convex_principal less_set_def
   29.23 +unfolding less_convex_pd_def Rep_convex_principal less_set_eq
   29.24  by (fast intro: convex_le_refl elim: convex_le_trans)
   29.25  
   29.26  lemma convex_principal_mono:
    30.1 --- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 07 10:56:58 2008 +0200
    30.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 07 10:57:19 2008 +0200
    30.3 @@ -300,33 +300,33 @@
    30.4  lemma externals_of_par: "ext (A1||A2) =     
    30.5     (ext A1) Un (ext A2)"
    30.6  apply (simp add: externals_def asig_of_par asig_comp_def
    30.7 -  asig_inputs_def asig_outputs_def Un_def set_diff_def)
    30.8 +  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
    30.9  apply blast
   30.10  done
   30.11  
   30.12  lemma actions_of_par: "act (A1||A2) =     
   30.13     (act A1) Un (act A2)"
   30.14  apply (simp add: actions_def asig_of_par asig_comp_def
   30.15 -  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
   30.16 +  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
   30.17  apply blast
   30.18  done
   30.19  
   30.20  lemma inputs_of_par: "inp (A1||A2) = 
   30.21            ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
   30.22  apply (simp add: actions_def asig_of_par asig_comp_def
   30.23 -  asig_inputs_def asig_outputs_def Un_def set_diff_def)
   30.24 +  asig_inputs_def asig_outputs_def Un_def set_diff_eq)
   30.25  done
   30.26  
   30.27  lemma outputs_of_par: "out (A1||A2) = 
   30.28            (out A1) Un (out A2)"
   30.29  apply (simp add: actions_def asig_of_par asig_comp_def
   30.30 -  asig_outputs_def Un_def set_diff_def)
   30.31 +  asig_outputs_def Un_def set_diff_eq)
   30.32  done
   30.33  
   30.34  lemma internals_of_par: "int (A1||A2) = 
   30.35            (int A1) Un (int A2)"
   30.36  apply (simp add: actions_def asig_of_par asig_comp_def
   30.37 -  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
   30.38 +  asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
   30.39  done
   30.40  
   30.41  
    31.1 --- a/src/HOLCF/LowerPD.thy	Wed May 07 10:56:58 2008 +0200
    31.2 +++ b/src/HOLCF/LowerPD.thy	Wed May 07 10:57:19 2008 +0200
    31.3 @@ -106,7 +106,7 @@
    31.4  by (rule Rep_lower_pd [simplified])
    31.5  
    31.6  lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
    31.7 -unfolding less_lower_pd_def less_set_def .
    31.8 +unfolding less_lower_pd_def less_set_eq .
    31.9  
   31.10  
   31.11  subsection {* Principal ideals *}
   31.12 @@ -134,12 +134,12 @@
   31.13  apply (rule ideal_Rep_lower_pd)
   31.14  apply (rule cont_Rep_lower_pd)
   31.15  apply (rule Rep_lower_principal)
   31.16 -apply (simp only: less_lower_pd_def less_set_def)
   31.17 +apply (simp only: less_lower_pd_def less_set_eq)
   31.18  done
   31.19  
   31.20  lemma lower_principal_less_iff [simp]:
   31.21    "(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
   31.22 -unfolding less_lower_pd_def Rep_lower_principal less_set_def
   31.23 +unfolding less_lower_pd_def Rep_lower_principal less_set_eq
   31.24  by (fast intro: lower_le_refl elim: lower_le_trans)
   31.25  
   31.26  lemma lower_principal_mono:
   31.27 @@ -151,7 +151,7 @@
   31.28  apply (simp add: less_lower_pd_def)
   31.29  apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
   31.30  apply (simp add: Rep_lower_principal set_cpo_simps)
   31.31 -apply (simp add: subset_def)
   31.32 +apply (simp add: subset_eq)
   31.33  apply (drule spec, drule mp, rule lower_le_refl)
   31.34  apply (erule exE, rename_tac i)
   31.35  apply (rule_tac x=i in exI)
    32.1 --- a/src/HOLCF/UpperPD.thy	Wed May 07 10:56:58 2008 +0200
    32.2 +++ b/src/HOLCF/UpperPD.thy	Wed May 07 10:57:19 2008 +0200
    32.3 @@ -126,12 +126,12 @@
    32.4  apply (rule ideal_Rep_upper_pd)
    32.5  apply (rule cont_Rep_upper_pd)
    32.6  apply (rule Rep_upper_principal)
    32.7 -apply (simp only: less_upper_pd_def less_set_def)
    32.8 +apply (simp only: less_upper_pd_def less_set_eq)
    32.9  done
   32.10  
   32.11  lemma upper_principal_less_iff [simp]:
   32.12    "(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
   32.13 -unfolding less_upper_pd_def Rep_upper_principal less_set_def
   32.14 +unfolding less_upper_pd_def Rep_upper_principal less_set_eq
   32.15  by (fast intro: upper_le_refl elim: upper_le_trans)
   32.16  
   32.17  lemma upper_principal_mono: