--- a/doc-src/TutorialI/Sets/Relations.thy Wed May 07 10:56:58 2008 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy Wed May 07 10:57:19 2008 +0200
@@ -151,7 +151,7 @@
text{*Pow, Inter too little used*}
lemma "(A \<subset> B) = (A \<subseteq> B \<and> A \<noteq> B)"
-apply (simp add: psubset_def)
+apply (simp add: psubset_eq)
done
end
--- a/src/HOL/Algebra/Sylow.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Algebra/Sylow.thy Wed May 07 10:57:19 2008 +0200
@@ -262,7 +262,7 @@
apply (rule coset_join1 [THEN in_H_imp_eq])
apply (rule_tac [3] H_is_subgroup)
prefer 2 apply (blast intro: m_closed M_elem_map_carrier inv_closed)
-apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_def)
+apply (simp add: coset_mult_inv2 H_def M_elem_map_carrier subset_eq)
done
--- a/src/HOL/Complex/ex/BigO_Complex.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Complex/ex/BigO_Complex.thy Wed May 07 10:57:19 2008 +0200
@@ -42,7 +42,7 @@
apply (drule set_plus_imp_minus)
apply (drule bigo_LIMSEQ1)
apply assumption
- apply (simp only: func_diff)
+ apply (simp only: fun_diff_def)
apply (erule LIMSEQ_diff_approach_zero2)
apply assumption
done
--- a/src/HOL/Hyperreal/NatStar.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy Wed May 07 10:57:19 2008 +0200
@@ -36,7 +36,7 @@
by (auto simp add: InternalSets_def starset_n_Int [symmetric])
lemma starset_n_Compl: "*sn* ((%n. - A n)) = -( *sn* A)"
-apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_def)
+apply (simp add: starset_n_def star_n_eq_starfun_whn Compl_eq)
apply (rule_tac x=whn in spec, transfer, simp)
done
@@ -44,7 +44,7 @@
by (auto simp add: InternalSets_def starset_n_Compl [symmetric])
lemma starset_n_diff: "*sn* (%n. (A n) - (B n)) = *sn* A - *sn* B"
-apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_def)
+apply (simp add: starset_n_def star_n_eq_starfun_whn set_diff_eq)
apply (rule_tac x=whn in spec, transfer, simp)
done
--- a/src/HOL/Hyperreal/StarDef.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy Wed May 07 10:57:19 2008 +0200
@@ -18,7 +18,7 @@
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>"
apply (unfold FreeUltrafilterNat_def)
-apply (rule someI_ex)
+apply (rule someI_ex [where P=freeultrafilter])
apply (rule freeultrafilter_Ex)
apply (rule nat_infinite)
done
@@ -401,10 +401,10 @@
by (transfer Int_def, rule refl)
lemma starset_Compl: "*s* -A = -( *s* A)"
-by (transfer Compl_def, rule refl)
+by (transfer Compl_eq, rule refl)
lemma starset_diff: "*s* (A - B) = *s* A - *s* B"
-by (transfer set_diff_def, rule refl)
+by (transfer set_diff_eq, rule refl)
lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)"
by (transfer image_def, rule refl)
@@ -413,7 +413,7 @@
by (transfer vimage_def, rule refl)
lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)"
-by (transfer subset_def, rule refl)
+by (transfer subset_eq, rule refl)
lemma starset_eq: "( *s* A = *s* B) = (A = B)"
by (transfer, rule refl)
--- a/src/HOL/IOA/IOA.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/IOA/IOA.thy Wed May 07 10:57:19 2008 +0200
@@ -337,7 +337,7 @@
lemma externals_of_par: "externals(asig_of(A1||A2)) =
(externals(asig_of(A1)) Un externals(asig_of(A2)))"
apply (simp add: externals_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def Un_def set_diff_def)
+ asig_inputs_def asig_outputs_def Un_def set_diff_eq)
apply blast
done
--- a/src/HOL/Induct/Com.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Induct/Com.thy Wed May 07 10:57:19 2008 +0200
@@ -85,11 +85,11 @@
lemma [pred_set_conv]:
"((\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> R) <= (\<lambda>x x' y y'. ((x, x'), (y, y')) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def)
+ by (auto simp add: le_fun_def le_bool_def mem_def)
lemma [pred_set_conv]:
"((\<lambda>x x' y. ((x, x'), y) \<in> R) <= (\<lambda>x x' y. ((x, x'), y) \<in> S)) = (R <= S)"
- by (auto simp add: le_fun_def le_bool_def)
+ by (auto simp add: le_fun_def le_bool_def mem_def)
declare [[unify_trace_bound = 30, unify_search_bound = 60]]
--- a/src/HOL/Lambda/InductTermi.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Wed May 07 10:57:19 2008 +0200
@@ -34,7 +34,6 @@
apply clarify
apply (rule accp.accI)
apply (safe elim!: apps_betasE)
- apply assumption
apply (blast intro: subst_preserves_beta apps_preserves_beta)
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtranclp_converseI
dest: accp_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *)
@@ -44,7 +43,7 @@
lemma IT_implies_termi: "IT t ==> termip beta t"
apply (induct set: IT)
apply (drule rev_predicate1D [OF _ listsp_mono [where B="termip beta"]])
- apply fast
+ apply (fast intro!: predicate1I)
apply (drule lists_accD)
apply (erule accp_induct)
apply (rule accp.accI)
--- a/src/HOL/Library/Order_Relation.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/Order_Relation.thy Wed May 07 10:57:19 2008 +0200
@@ -103,7 +103,7 @@
lemma subset_Image_Image_iff:
"\<lbrakk> Preorder r; A \<subseteq> Field r; B \<subseteq> Field r\<rbrakk> \<Longrightarrow>
r `` A \<subseteq> r `` B \<longleftrightarrow> (\<forall>a\<in>A.\<exists>b\<in>B. (b,a):r)"
-apply(auto simp add:subset_def preorder_on_def refl_def Image_def)
+apply(auto simp add: subset_eq preorder_on_def refl_def Image_def)
apply metis
by(metis trans_def)
--- a/src/HOL/Library/RType.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/RType.thy Wed May 07 10:57:19 2008 +0200
@@ -87,7 +87,6 @@
#> RType.add_def @{type_name fun}
#> RType.add_def @{type_name itself}
#> RType.add_def @{type_name bool}
- #> RType.add_def @{type_name set}
#> TypedefPackage.interpretation RType.perhaps_add_def
*}
--- a/src/HOL/Library/Zorn.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Library/Zorn.thy Wed May 07 10:57:19 2008 +0200
@@ -44,7 +44,6 @@
where
succI: "x \<in> TFin S ==> succ S x \<in> TFin S"
| Pow_UnionI: "Y \<in> Pow(TFin S) ==> Union(Y) \<in> TFin S"
- monos Pow_mono
subsection{*Mathematical Preamble*}
@@ -57,22 +56,20 @@
text{*This is theorem @{text increasingD2} of ZF/Zorn.thy*}
lemma Abrial_axiom1: "x \<subseteq> succ S x"
- apply (unfold succ_def)
- apply (rule split_if [THEN iffD2])
- apply (auto simp add: super_def maxchain_def psubset_def)
+ apply (auto simp add: succ_def super_def maxchain_def)
apply (rule contrapos_np, assumption)
- apply (rule someI2, blast+)
+ apply (rule_tac Q="\<lambda>S. xa \<in> S" in someI2, blast+)
done
lemmas TFin_UnionI = TFin.Pow_UnionI [OF PowI]
lemma TFin_induct:
- "[| n \<in> TFin S;
- !!x. [| x \<in> TFin S; P(x) |] ==> P(succ S x);
- !!Y. [| Y \<subseteq> TFin S; Ball Y P |] ==> P(Union Y) |]
- ==> P(n)"
- apply (induct set: TFin)
- apply blast+
+ assumes H: "n \<in> TFin S"
+ and I: "!!x. x \<in> TFin S ==> P x ==> P (succ S x)"
+ "!!Y. Y \<subseteq> TFin S ==> Ball Y P ==> P(Union Y)"
+ shows "P n" using H
+ apply (induct rule: TFin.induct [where P=P])
+ apply (blast intro: I)+
done
lemma succ_trans: "x \<subseteq> y ==> x \<subseteq> succ S y"
@@ -163,14 +160,14 @@
lemma select_super:
"c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c): super S c"
apply (erule mem_super_Ex [THEN exE])
- apply (rule someI2, auto)
+ apply (rule someI2 [where Q="%X. X : super S c"], auto)
done
lemma select_not_equals:
"c \<in> chain S - maxchain S ==> (\<some>c'. c': super S c) \<noteq> c"
apply (rule notI)
apply (drule select_super)
- apply (simp add: super_def psubset_def)
+ apply (simp add: super_def less_le)
done
lemma succI3: "c \<in> chain S - maxchain S ==> succ S c = (\<some>c'. c': super S c)"
@@ -189,7 +186,7 @@
apply (rule CollectI, safe)
apply (drule bspec, assumption)
apply (rule_tac [2] m1 = Xa and n1 = X in TFin_subset_linear [THEN disjE],
- blast+)
+ best+)
done
theorem Hausdorff: "\<exists>c. (c :: 'a set set): maxchain S"
@@ -223,7 +220,7 @@
apply (erule conjE)
apply (subgoal_tac "({u} Un c) \<in> super S c")
apply simp
-apply (unfold super_def psubset_def)
+apply (unfold super_def less_le)
apply (blast intro: chain_extend dest: chain_Union_upper)
done
@@ -253,7 +250,7 @@
apply (rule ccontr)
apply (frule_tac z = x in chain_extend)
apply (assumption, blast)
-apply (unfold maxchain_def super_def psubset_def)
+apply (unfold maxchain_def super_def less_le)
apply (blast elim!: equalityCE)
done
--- a/src/HOL/MetisExamples/Tarski.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MetisExamples/Tarski.thy Wed May 07 10:57:19 2008 +0200
@@ -672,7 +672,7 @@
declare (in CLF) rel_imp_elem[intro]
declare interval_def [simp]
lemma (in CLF) interval_subset: "[| a \<in> A; b \<in> A |] ==> interval r a b \<subseteq> A"
-by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_def)
+by (metis CO_refl interval_imp_mem reflD reflD2 rel_imp_elem subset_eq)
declare (in CLF) rel_imp_elem[rule del]
declare interval_def [simp del]
@@ -1013,7 +1013,7 @@
ML_command{*ResAtp.problem_name:="Tarski__fz_in_int_rel"*} (*ALL THEOREMS*)
lemma (in Tarski) f'z_in_int_rel: "[| z \<in> P; \<forall>y\<in>Y. (y, z) \<in> induced P r |]
==> ((%x: intY1. f x) z, z) \<in> induced intY1 r"
-apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_def z_in_interval)
+apply (metis P_def acc_def fix_imp_eq fix_subset indI reflE restrict_apply subset_eq z_in_interval)
done
(*never proved, 2007-01-22*)
--- a/src/HOL/MetisExamples/set.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MetisExamples/set.thy Wed May 07 10:57:19 2008 +0200
@@ -238,7 +238,7 @@
lemma (*singleton_example_2:*)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_def)
+by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
--- a/src/HOL/MicroJava/BV/Listn.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/MicroJava/BV/Listn.thy Wed May 07 10:57:19 2008 +0200
@@ -330,7 +330,7 @@
apply (rename_tac m n)
apply (case_tac "m=n")
apply simp
- apply (fast intro!: equals0I [to_pred bot_empty_eq] dest: not_sym)
+ apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym)
apply clarify
apply (rename_tac n)
apply (induct_tac n)
--- a/src/HOL/Nominal/Examples/Class.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Wed May 07 10:57:19 2008 +0200
@@ -10317,7 +10317,7 @@
lemma NOTRIGHT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10343,7 +10343,7 @@
lemma NOTRIGHT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(NOTRIGHT (NOT B) X)) = NOTRIGHT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10377,7 +10377,7 @@
lemma NOTLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10403,7 +10403,7 @@
lemma NOTLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(NOTLEFT (NOT B) X)) = NOTLEFT (NOT B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10438,7 +10438,7 @@
lemma ANDRIGHT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>c" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10473,7 +10473,7 @@
lemma ANDRIGHT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDRIGHT (A AND B) X Y)) = ANDRIGHT (A AND B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>c" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10516,7 +10516,7 @@
lemma ANDLEFT1_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10542,7 +10542,7 @@
lemma ANDLEFT1_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDLEFT1 (A AND B) X)) = ANDLEFT1 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10576,7 +10576,7 @@
lemma ANDLEFT2_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10602,7 +10602,7 @@
lemma ANDLEFT2_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ANDLEFT2 (A AND B) X)) = ANDLEFT2 (A AND B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10637,7 +10637,7 @@
lemma ORLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>z" in exI)
@@ -10672,7 +10672,7 @@
lemma ORLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORLEFT (A OR B) X Y)) = ORLEFT (A OR B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
apply(rule_tac x="pi\<bullet>z" in exI)
@@ -10715,7 +10715,7 @@
lemma ORRIGHT1_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10741,7 +10741,7 @@
lemma ORRIGHT1_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORRIGHT1 (A OR B) X)) = ORRIGHT1 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10775,7 +10775,7 @@
lemma ORRIGHT2_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10801,7 +10801,7 @@
lemma ORRIGHT2_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(ORRIGHT2 (A OR B) X)) = ORRIGHT2 (A OR B) (pi\<bullet>X)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
@@ -10838,7 +10838,7 @@
lemma IMPRIGHT_eqvt_name:
fixes pi::"name prm"
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)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10898,7 +10898,7 @@
lemma IMPRIGHT_eqvt_coname:
fixes pi::"coname prm"
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)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>b" in exI)
@@ -10966,7 +10966,7 @@
lemma IMPLEFT_eqvt_name:
fixes pi::"name prm"
shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
@@ -11001,7 +11001,7 @@
lemma IMPLEFT_eqvt_coname:
fixes pi::"coname prm"
shows "(pi\<bullet>(IMPLEFT (A IMP B) X Y)) = IMPLEFT (A IMP B) (pi\<bullet>X) (pi\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>a" in exI)
apply(rule_tac x="pi\<bullet>y" in exI)
@@ -11098,16 +11098,6 @@
shows "x\<in>(X\<inter>Y) = (x\<in>X \<and> x\<in>Y)"
by blast
-lemma pt_Collect_eqvt:
- fixes pi::"'x prm"
- assumes pt: "pt TYPE('a) TYPE('x)"
- and at: "at TYPE('x)"
- shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
-apply(rule_tac x="(rev pi)\<bullet>x" in exI)
-apply(simp add: pt_pi_rev[OF pt, OF at])
-done
-
lemma big_inter_eqvt:
fixes pi1::"name prm"
and X::"('a::pt_name) set set"
@@ -11115,7 +11105,7 @@
and Y::"('b::pt_coname) set set"
shows "(pi1\<bullet>(\<Inter> X)) = \<Inter> (pi1\<bullet>X)"
and "(pi2\<bullet>(\<Inter> Y)) = \<Inter> (pi2\<bullet>Y)"
-apply(auto simp add: perm_set_def)
+apply(auto simp add: perm_set_eq)
apply(rule_tac x="(rev pi1)\<bullet>x" in exI)
apply(perm_simp)
apply(rule ballI)
@@ -11150,7 +11140,7 @@
shows "pi1\<bullet>(lfp f) = lfp (pi1\<bullet>f)"
and "pi2\<bullet>(lfp g) = lfp (pi2\<bullet>g)"
apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_name_inst, OF at_name_inst])
apply(subgoal_tac "{u. (pi1\<bullet>f) u \<subseteq> u} = {u. ((rev pi1)\<bullet>((pi1\<bullet>f) u)) \<subseteq> ((rev pi1)\<bullet>u)}")
@@ -11162,7 +11152,7 @@
apply(drule subseteq_eqvt(1)[THEN iffD2])
apply(simp add: perm_bool)
apply(simp add: lfp_def)
-apply(simp add: Inf_set_def)
+apply(simp add: Inf_set_eq)
apply(simp add: big_inter_eqvt)
apply(simp add: pt_Collect_eqvt[OF pt_coname_inst, OF at_coname_inst])
apply(subgoal_tac "{u. (pi2\<bullet>g) u \<subseteq> u} = {u. ((rev pi2)\<bullet>((pi2\<bullet>g) u)) \<subseteq> ((rev pi2)\<bullet>u)}")
@@ -11345,7 +11335,7 @@
fixes pi::"name prm"
shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)"
and "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)"
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
@@ -11400,7 +11390,7 @@
fixes pi::"coname prm"
shows "(pi\<bullet>(BINDINGn B X)) = BINDINGn B (pi\<bullet>X)"
and "(pi\<bullet>(BINDINGc B Y)) = BINDINGc B (pi\<bullet>Y)"
-apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_def)
+apply(auto simp add: BINDINGn_def BINDINGc_def perm_set_eq)
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule_tac x="pi\<bullet>M" in exI)
apply(simp)
@@ -11460,7 +11450,7 @@
{ case 1 show ?case
apply -
apply(simp add: lfp_eqvt)
- apply(simp add: perm_fun_def)
+ apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(perm_simp)
done
@@ -11471,7 +11461,7 @@
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(simp add: lfp_eqvt)
apply(simp add: comp_def)
- apply(simp add: perm_fun_def)
+ apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp add: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name)
apply(perm_simp)
done
@@ -11484,7 +11474,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name NOTRIGHT_eqvt_name NOTLEFT_eqvt_name)
apply(perm_simp add: ih1 ih2)
@@ -11504,7 +11494,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ANDRIGHT_eqvt_name
ANDLEFT2_eqvt_name ANDLEFT1_eqvt_name)
@@ -11526,7 +11516,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name ORRIGHT1_eqvt_name
ORRIGHT2_eqvt_name ORLEFT_eqvt_name)
@@ -11548,7 +11538,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_name BINDING_eqvt_name IMPRIGHT_eqvt_name IMPLEFT_eqvt_name)
apply(perm_simp add: ih1 ih2 ih3 ih4)
@@ -11570,7 +11560,7 @@
{ case 1 show ?case
apply -
apply(simp add: lfp_eqvt)
- apply(simp add: perm_fun_def)
+ apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(perm_simp)
done
@@ -11581,7 +11571,7 @@
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(simp add: lfp_eqvt)
apply(simp add: comp_def)
- apply(simp add: perm_fun_def)
+ apply(simp add: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp add: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname)
apply(perm_simp)
done
@@ -11594,7 +11584,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname
NOTRIGHT_eqvt_coname NOTLEFT_eqvt_coname)
@@ -11616,7 +11606,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ANDRIGHT_eqvt_coname
ANDLEFT2_eqvt_coname ANDLEFT1_eqvt_coname)
@@ -11638,7 +11628,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname ORRIGHT1_eqvt_coname
ORRIGHT2_eqvt_coname ORLEFT_eqvt_coname)
@@ -11660,7 +11650,7 @@
apply -
apply(simp only: lfp_eqvt)
apply(simp only: comp_def)
- apply(simp only: perm_fun_def)
+ apply(simp only: perm_fun_def [where 'a="ntrm \<Rightarrow> bool"])
apply(simp only: NEGc.simps NEGn.simps)
apply(simp only: union_eqvt AXIOMS_eqvt_coname BINDING_eqvt_coname IMPRIGHT_eqvt_coname
IMPLEFT_eqvt_coname)
--- a/src/HOL/Nominal/Examples/SOS.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy Wed May 07 10:57:19 2008 +0200
@@ -422,7 +422,7 @@
shows "(pi\<bullet>x)\<in>V T"
using a
apply(nominal_induct T arbitrary: pi x rule: ty.induct)
-apply(auto simp add: trm.inject perm_set_def)
+apply(auto simp add: trm.inject)
apply(simp add: eqvts)
apply(rule_tac x="pi\<bullet>xa" in exI)
apply(rule_tac x="pi\<bullet>e" in exI)
--- a/src/HOL/Nominal/Examples/Support.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Examples/Support.thy Wed May 07 10:57:19 2008 +0200
@@ -100,14 +100,14 @@
proof (cases "x\<in>S")
case True
have "x\<in>S" by fact
- hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+ hence "\<forall>b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
with asm2 have "infinite {b\<in>(UNIV-S). [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
next
case False
have "x\<notin>S" by fact
- hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_def calc_atm)
+ hence "\<forall>b\<in>S. [(x,b)]\<bullet>S\<noteq>S" by (auto simp add: perm_set_eq calc_atm)
with asm1 have "infinite {b\<in>S. [(x,b)]\<bullet>S\<noteq>S}" by (rule infinite_Collection)
hence "infinite {b. [(x,b)]\<bullet>S\<noteq>S}" by (rule_tac infinite_super, auto)
then show "x\<in>(supp S)" by (simp add: supp_def)
@@ -131,7 +131,7 @@
shows "supp (UNIV::atom set) = ({}::atom set)"
proof -
have "\<forall>(x::atom) (y::atom). [(x,y)]\<bullet>UNIV = (UNIV::atom set)"
- by (auto simp add: perm_set_def calc_atm)
+ by (auto simp add: perm_set_eq calc_atm)
then show "supp (UNIV::atom set) = ({}::atom set)" by (simp add: supp_def)
qed
--- a/src/HOL/Nominal/Nominal.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy Wed May 07 10:57:19 2008 +0200
@@ -29,61 +29,6 @@
constdefs
"perm_aux pi x \<equiv> pi\<bullet>x"
-(* permutation on sets *)
-defs (unchecked overloaded)
- perm_set_def: "pi\<bullet>(X::'a set) \<equiv> {pi\<bullet>x | x. x\<in>X}"
-
-lemma empty_eqvt:
- shows "pi\<bullet>{} = {}"
- by (simp add: perm_set_def)
-
-lemma union_eqvt:
- shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
- by (auto simp add: perm_set_def)
-
-lemma insert_eqvt:
- shows "pi\<bullet>(insert x X) = insert (pi\<bullet>x) (pi\<bullet>X)"
- by (auto simp add: perm_set_def)
-
-(* permutation on units and products *)
-primrec (unchecked perm_unit)
- "pi\<bullet>() = ()"
-
-primrec (unchecked perm_prod)
- "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
-
-lemma fst_eqvt:
- "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
- by (cases x) simp
-
-lemma snd_eqvt:
- "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
- by (cases x) simp
-
-(* permutation on lists *)
-primrec (unchecked perm_list)
- nil_eqvt: "pi\<bullet>[] = []"
- cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
-
-lemma append_eqvt:
- fixes pi :: "'x prm"
- and l1 :: "'a list"
- and l2 :: "'a list"
- shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
- by (induct l1) auto
-
-lemma rev_eqvt:
- fixes pi :: "'x prm"
- and l :: "'a list"
- shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
- by (induct l) (simp_all add: append_eqvt)
-
-lemma set_eqvt:
- fixes pi :: "'x prm"
- and xs :: "'a list"
- shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt)
-
(* permutation on functions *)
defs (unchecked overloaded)
perm_fun_def: "pi\<bullet>(f::'a\<Rightarrow>'b) \<equiv> (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))"
@@ -129,6 +74,48 @@
shows "pi\<bullet>(\<not> A) = (\<not> (pi\<bullet>A))"
by (simp add: perm_bool)
+(* permutation on sets *)
+lemma empty_eqvt:
+ shows "pi\<bullet>{} = {}"
+ by (simp add: perm_fun_def perm_bool empty_iff [unfolded mem_def] expand_fun_eq)
+
+lemma union_eqvt:
+ shows "(pi\<bullet>(X\<union>Y)) = (pi\<bullet>X) \<union> (pi\<bullet>Y)"
+ by (simp add: perm_fun_def perm_bool Un_iff [unfolded mem_def] expand_fun_eq)
+
+(* permutation on units and products *)
+primrec (unchecked perm_unit)
+ "pi\<bullet>() = ()"
+
+primrec (unchecked perm_prod)
+ "pi\<bullet>(x,y) = (pi\<bullet>x,pi\<bullet>y)"
+
+lemma fst_eqvt:
+ "pi\<bullet>(fst x) = fst (pi\<bullet>x)"
+ by (cases x) simp
+
+lemma snd_eqvt:
+ "pi\<bullet>(snd x) = snd (pi\<bullet>x)"
+ by (cases x) simp
+
+(* permutation on lists *)
+primrec (unchecked perm_list)
+ nil_eqvt: "pi\<bullet>[] = []"
+ cons_eqvt: "pi\<bullet>(x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)"
+
+lemma append_eqvt:
+ fixes pi :: "'x prm"
+ and l1 :: "'a list"
+ and l2 :: "'a list"
+ shows "pi\<bullet>(l1@l2) = (pi\<bullet>l1)@(pi\<bullet>l2)"
+ by (induct l1) auto
+
+lemma rev_eqvt:
+ fixes pi :: "'x prm"
+ and l :: "'a list"
+ shows "pi\<bullet>(rev l) = rev (pi\<bullet>l)"
+ by (induct l) (simp_all add: append_eqvt)
+
(* permutation on options *)
primrec (unchecked perm_option)
@@ -196,11 +183,7 @@
lemma supp_set_empty:
shows "supp {} = {}"
- by (force simp add: supp_def perm_set_def)
-
-lemma supp_singleton:
- shows "supp {x} = supp x"
- by (force simp add: supp_def perm_set_def)
+ by (force simp add: supp_def empty_eqvt)
lemma supp_prod:
fixes x :: "'a"
@@ -284,10 +267,6 @@
shows "a\<sharp>{}"
by (simp add: fresh_def supp_set_empty)
-lemma fresh_singleton:
- shows "a\<sharp>{x} = a\<sharp>x"
- by (simp add: fresh_def supp_singleton)
-
lemma fresh_unit:
shows "a\<sharp>()"
by (simp add: fresh_def supp_unit)
@@ -1026,15 +1005,6 @@
section {* permutation type instances *}
(* ===================================*)
-lemma pt_set_inst:
- assumes pt: "pt TYPE('a) TYPE('x)"
- shows "pt TYPE('a set) TYPE('x)"
-apply(simp add: pt_def)
-apply(simp_all add: perm_set_def)
-apply(simp add: pt1[OF pt])
-apply(force simp add: pt2[OF pt] pt3[OF pt])
-done
-
lemma pt_list_nil:
fixes xs :: "'a list"
assumes pt: "pt TYPE('a) TYPE ('x)"
@@ -1270,6 +1240,42 @@
apply(rule pt1[OF pt])
done
+lemma perm_set_eq:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi::'x prm)\<bullet>(X::'a set) = {pi\<bullet>x | x. x\<in>X}"
+ apply (auto simp add: perm_fun_def perm_bool mem_def)
+ apply (rule_tac x="rev pi \<bullet> x" in exI)
+ apply (simp add: pt_pi_rev [OF pt at])
+ apply (simp add: pt_rev_pi [OF pt at])
+ done
+
+lemma insert_eqvt:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+ by (auto simp add: perm_set_eq [OF pt at])
+
+lemma set_eqvt:
+ fixes pi :: "'x prm"
+ and xs :: "'a list"
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
+by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+
+lemma supp_singleton:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(supp {x::'a} :: 'x set) = supp x"
+ by (force simp add: supp_def perm_set_eq [OF pt at])
+
+lemma fresh_singleton:
+ assumes pt: "pt TYPE('a) TYPE('x)"
+ and at: "at TYPE('x)"
+ shows "(a::'x)\<sharp>{x::'a} = a\<sharp>x"
+ by (simp add: fresh_def supp_singleton [OF pt at])
+
lemma pt_set_bij1:
fixes pi :: "'x prm"
and x :: "'a"
@@ -1277,7 +1283,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "((pi\<bullet>x)\<in>X) = (x\<in>((rev pi)\<bullet>X))"
- by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+ by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
lemma pt_set_bij1a:
fixes pi :: "'x prm"
@@ -1286,7 +1292,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "(x\<in>(pi\<bullet>X)) = (((rev pi)\<bullet>x)\<in>X)"
- by (force simp add: perm_set_def pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
+ by (force simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at] pt_pi_rev[OF pt, OF at])
lemma pt_set_bij:
fixes pi :: "'x prm"
@@ -1295,7 +1301,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "((pi\<bullet>x)\<in>(pi\<bullet>X)) = (x\<in>X)"
- by (simp add: perm_set_def pt_bij[OF pt, OF at])
+ by (simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
lemma pt_in_eqvt:
fixes pi :: "'x prm"
@@ -1342,7 +1348,7 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "(pi\<bullet>(X\<subseteq>Y)) = ((pi\<bullet>X)\<subseteq>(pi\<bullet>Y))"
-by (auto simp add: perm_set_def perm_bool pt_bij[OF pt, OF at])
+by (auto simp add: perm_set_eq [OF pt at] perm_bool pt_bij[OF pt, OF at])
lemma pt_set_diff_eqvt:
fixes X::"'a set"
@@ -1351,14 +1357,14 @@
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>(X - Y) = (pi\<bullet>X) - (pi\<bullet>Y)"
- by (auto simp add: perm_set_def pt_bij[OF pt, OF at])
+ by (auto simp add: perm_set_eq [OF pt at] pt_bij[OF pt, OF at])
lemma pt_Collect_eqvt:
fixes pi::"'x prm"
assumes pt: "pt TYPE('a) TYPE('x)"
and at: "at TYPE('x)"
shows "pi\<bullet>{x::'a. P x} = {x. P ((rev pi)\<bullet>x)}"
-apply(auto simp add: perm_set_def pt_rev_pi[OF pt, OF at])
+apply(auto simp add: perm_set_eq [OF pt at] pt_rev_pi[OF pt, OF at])
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
apply(simp add: pt_pi_rev[OF pt, OF at])
done
@@ -1402,7 +1408,7 @@
and at: "at TYPE('y)"
shows "finite (pi\<bullet>X) = finite X"
proof -
- have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_def)
+ have image: "(pi\<bullet>X) = (perm pi ` X)" by (force simp only: perm_set_eq [OF pt at])
show ?thesis
proof (rule iffI)
assume "finite (pi\<bullet>X)"
@@ -1432,17 +1438,17 @@
and cp: "cp TYPE('a) TYPE('x) TYPE('y)"
shows "(pi\<bullet>((supp x)::'y set)) = supp (pi\<bullet>x)" (is "?LHS = ?RHS")
proof -
- have "?LHS = {pi\<bullet>a | a. infinite {b. [(a,b)]\<bullet>x \<noteq> x}}" by (simp add: supp_def perm_set_def)
+ 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])
also have "\<dots> = {pi\<bullet>a | a. infinite {pi\<bullet>b | b. [(a,b)]\<bullet>x \<noteq> x}}"
proof (rule Collect_permI, rule allI, rule iffI)
fix a
assume "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
- thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_def)
+ thus "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}" by (simp add: perm_set_eq [OF ptb at])
next
fix a
assume "infinite {pi\<bullet>b |b::'y. [(a,b)]\<bullet>x \<noteq> x}"
- hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_def)
+ hence "infinite (pi\<bullet>{b::'y. [(a,b)]\<bullet>x \<noteq> x})" by (simp add: perm_set_eq [OF ptb at])
thus "infinite {b::'y. [(a,b)]\<bullet>x \<noteq> x}"
by (simp add: pt_set_infinite_ineq[OF ptb, OF at])
qed
@@ -1550,10 +1556,10 @@
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="pi\<bullet>xa" in bspec)
apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: set_eqvt pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt)
+apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
done
@@ -2012,7 +2018,8 @@
assumes at: "at TYPE('x)"
shows "X supports X"
proof -
- 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])
+ have "\<forall>a b. a\<notin>X \<and> b\<notin>X \<longrightarrow> [(a,b)]\<bullet>X = X"
+ by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
then show ?thesis by (simp add: supports_def)
qed
@@ -2023,7 +2030,7 @@
using a1 a2
apply auto
apply (subgoal_tac "infinite (X - {b\<in>X. P b})")
- apply (simp add: set_diff_def)
+ apply (simp add: set_diff_eq)
apply (simp add: Diff_infinite_finite)
done
@@ -2038,7 +2045,8 @@
have inf: "infinite (UNIV-X)" using at4[OF at] fs by (auto simp add: Diff_infinite_finite)
{ fix a::"'x"
assume asm: "a\<in>X"
- hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X" by (auto simp add: perm_set_def at_calc[OF at])
+ hence "\<forall>b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X"
+ by (auto simp add: perm_set_eq [OF at_pt_inst [OF at] at] at_calc[OF at])
with inf have "infinite {b\<in>(UNIV-X). [(a,b)]\<bullet>X\<noteq>X}" by (rule infinite_Collection)
hence "infinite {b. [(a,b)]\<bullet>X\<noteq>X}" by (rule_tac infinite_super, auto)
hence "a\<in>(supp X)" by (simp add: supp_def)
@@ -2259,7 +2267,7 @@
proof (rule equalityI)
case goal1
show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
- apply(auto simp add: perm_set_def)
+ apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
apply(rule_tac x="pi\<bullet>xb" in exI)
apply(rule conjI)
apply(rule_tac x="xb" in exI)
@@ -2275,7 +2283,7 @@
next
case goal2
show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
- apply(auto simp add: perm_set_def)
+ apply(auto simp add: perm_set_eq [OF pt at] perm_set_eq [OF at_pt_inst [OF at] at])
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
apply(rule conjI)
apply(simp add: pt_pi_rev[OF pt_x, OF at])
@@ -2294,7 +2302,7 @@
and at: "at TYPE('x)"
shows "pi\<bullet>(X_to_Un_supp X) = ((X_to_Un_supp (pi\<bullet>X))::'x set)"
apply(simp add: X_to_Un_supp_def)
- apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def)
+ apply(simp add: UNION_f_eqvt[OF pt, OF at] perm_fun_def [where 'b="'x set"])
apply(simp add: pt_perm_supp[OF pt, OF at])
apply(simp add: pt_pi_rev[OF pt, OF at])
done
@@ -2308,7 +2316,7 @@
apply(rule allI)+
apply(rule impI)
apply(erule conjE)
- apply(simp add: perm_set_def)
+ apply(simp add: perm_set_eq [OF pt at])
apply(auto)
apply(subgoal_tac "[(a,b)]\<bullet>xa = xa")(*A*)
apply(simp)
@@ -2339,9 +2347,9 @@
proof -
have "supp ((X_to_Un_supp X)::'x set) \<subseteq> ((supp X)::'x set)"
apply(rule pt_empty_supp_fun_subset)
- apply(force intro: pt_set_inst at_pt_inst pt at)+
+ apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
apply(rule pt_eqvt_fun2b)
- apply(force intro: pt_set_inst at_pt_inst pt at)+
+ apply(force intro: pt_fun_inst pt_bool_inst at_pt_inst pt at)+
apply(rule allI)+
apply(rule X_to_Un_supp_eqvt[OF pt, OF at])
done
@@ -2392,7 +2400,7 @@
also have "\<dots> = (supp {x})\<union>(supp X)"
by (rule supp_fin_union[OF pt, OF at, OF fs], simp_all add: f)
finally show "(supp (insert x X)) = (supp x)\<union>((supp X)::'x set)"
- by (simp add: supp_singleton)
+ by (simp add: supp_singleton [OF pt at])
qed
lemma fresh_fin_union:
@@ -2477,17 +2485,6 @@
apply(auto)
done
-lemma cp_set_inst:
- assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
- shows "cp TYPE ('a set) TYPE('x) TYPE('y)"
-using c1
-apply(simp add: cp_def)
-apply(auto)
-apply(auto simp add: perm_set_def)
-apply(rule_tac x="pi2\<bullet>xc" in exI)
-apply(auto)
-done
-
lemma cp_option_inst:
assumes c1: "cp TYPE ('a) TYPE('x) TYPE('y)"
shows "cp TYPE ('a option) TYPE('x) TYPE('y)"
@@ -3369,7 +3366,7 @@
plus_int_eqvt minus_int_eqvt mult_int_eqvt div_int_eqvt
(* sets *)
- union_eqvt empty_eqvt insert_eqvt set_eqvt
+ union_eqvt empty_eqvt
(* the lemmas numeral_nat_eqvt numeral_int_eqvt do not conform with the *)
--- a/src/HOL/Nominal/nominal_package.ML Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed May 07 10:57:19 2008 +0200
@@ -1183,8 +1183,9 @@
val ind_prems' =
map (fn (_, f as Free (_, T)) => list_all_free ([("x", fsT')],
- HOLogic.mk_Trueprop (Const ("Finite_Set.finite", body_type T -->
- HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
+ HOLogic.mk_Trueprop (Const ("Finite_Set.finite",
+ (snd (split_last (binder_types T)) --> HOLogic.boolT) -->
+ HOLogic.boolT) $ (f $ Free ("x", fsT'))))) fresh_fs @
List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
map (make_ind_prem fsT' (fn T => fn t => fn u => HOLogic.Not $
HOLogic.mk_mem (t, the (AList.lookup op = fresh_fs T) $ u)) i T)
--- a/src/HOL/Nominal/nominal_permeq.ML Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Wed May 07 10:57:19 2008 +0200
@@ -290,7 +290,7 @@
fun finite_guess_tac tactical ss i st =
let val goal = List.nth(cprems_of st, i-1)
in
- case Logic.strip_assums_concl (term_of goal) of
+ case Envir.eta_contract (Logic.strip_assums_concl (term_of goal)) of
_ $ (Const ("Finite_Set.finite", _) $ (Const ("Nominal.supp", T) $ x)) =>
let
val cert = Thm.cterm_of (Thm.theory_of_thm st);
@@ -301,7 +301,8 @@
HOLogic.pair_const (fastype_of1 (Ts, v)) (fastype_of1 (Ts, s)) $ v $ s)
(vs, HOLogic.unit);
val s' = list_abs (ps,
- Const ("Nominal.supp", fastype_of1 (Ts, s) --> body_type T) $ s);
+ Const ("Nominal.supp", fastype_of1 (Ts, s) -->
+ snd (split_last (binder_types T)) --> HOLogic.boolT) $ s);
val supports_rule' = Thm.lift_rule goal supports_rule;
val _ $ (_ $ S $ _) =
Logic.strip_assums_concl (hd (prems_of supports_rule'));
--- a/src/HOL/Real/PReal.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Real/PReal.thy Wed May 07 10:57:19 2008 +0200
@@ -202,7 +202,7 @@
(* Axiom 'order_less_le' of class 'order': *)
lemma preal_less_le: "((w::preal) < z) = (w \<le> z & w \<noteq> z)"
-by (simp add: preal_le_def preal_less_def Rep_preal_inject psubset_def)
+by (simp add: preal_le_def preal_less_def Rep_preal_inject less_le)
instance preal :: order
by intro_classes
@@ -943,7 +943,7 @@
text{*at last, Gleason prop. 9-3.5(iii) page 123*}
lemma preal_self_less_add_left: "(R::preal) < R + S"
-apply (unfold preal_less_def psubset_def)
+apply (unfold preal_less_def less_le)
apply (simp add: Rep_preal_self_subset Rep_preal_sum_not_eq [THEN not_sym])
done
--- a/src/HOL/Subst/Unify.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Subst/Unify.thy Wed May 07 10:57:19 2008 +0200
@@ -117,7 +117,7 @@
apply blast
txt{*@{text finite_psubset} case*}
apply (simp add: unifyRel_def lex_prod_def)
-apply (simp add: finite_psubset_def finite_vars_of psubset_def)
+apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
apply blast
txt{*Final case, also @{text finite_psubset}*}
apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def)
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed May 07 10:57:19 2008 +0200
@@ -375,12 +375,16 @@
(map (pair "x") Ts, S $ app_bnds f i)),
HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
r $ (a $ app_bnds f i)), f))))
- (fn _ => EVERY [REPEAT (rtac ext 1), REPEAT (etac allE 1), rtac thm 1, atac 1])
+ (fn _ => EVERY [REPEAT_DETERM_N i (rtac ext 1),
+ REPEAT (etac allE 1), rtac thm 1, atac 1])
end
in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
+ val fun_congs = map (fn T => make_elim (Drule.instantiate'
+ [SOME (ctyp_of thy5 T)] [] fun_cong)) branchTs;
+
fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
let
val (_, (tname, _, _)) = hd ds;
@@ -422,7 +426,7 @@
[REPEAT (rtac ext 1),
REPEAT (eresolve_tac (mp :: allE ::
map make_elim (Suml_inject :: Sumr_inject ::
- Lim_inject :: fun_cong :: inj_thms')) 1),
+ Lim_inject :: inj_thms') @ fun_congs) 1),
atac 1]))])])])]);
val inj_thms'' = map (fn r => r RS @{thm datatype_injI})
--- a/src/HOL/Tools/inductive_codegen.ML Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed May 07 10:57:19 2008 +0200
@@ -191,11 +191,11 @@
| _ => default)
end;
-datatype indprem = Prem of term list * term | Sidecond of term;
+datatype indprem = Prem of term list * term * bool | Sidecond of term;
fun select_mode_prem thy modes vs ps =
find_first (is_some o snd) (ps ~~ map
- (fn Prem (us, t) => find_first (fn Mode (_, is, _) =>
+ (fn Prem (us, t, is_set) => find_first (fn Mode (_, is, _) =>
let
val (in_ts, out_ts) = get_args is 1 us;
val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
@@ -208,7 +208,9 @@
term_vs t subset vs andalso
forall is_eqT dupTs
end)
- (modes_of modes t handle Option => [Mode (([], []), [], [])])
+ (if is_set then [Mode (([], []), [], [])]
+ else modes_of modes t handle Option =>
+ error ("Bad predicate: " ^ Sign.string_of_term thy t))
| Sidecond t => if term_vs t subset vs then SOME (Mode (([], []), [], []))
else NONE) ps);
@@ -221,7 +223,7 @@
| check_mode_prems vs ps = (case select_mode_prem thy modes' vs ps of
NONE => NONE
| SOME (x, _) => check_mode_prems
- (case x of Prem (us, _) => vs union terms_vs us | _ => vs)
+ (case x of Prem (us, _, _) => vs union terms_vs us | _ => vs)
(filter_out (equal x) ps));
val (in_ts, in_ts') = List.partition (is_constrt thy) (fst (get_args is 1 ts));
val in_vs = terms_vs in_ts;
@@ -390,21 +392,21 @@
val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
in
(case p of
- Prem (us, t) =>
+ Prem (us, t, is_set) =>
let
val (in_ts, out_ts''') = get_args js 1 us;
val (gr2, in_ps) = foldl_map
(invoke_codegen thy defs dep module true) (gr1, in_ts);
- val (gr3, ps) = (case body_type (fastype_of t) of
- Type ("bool", []) =>
+ val (gr3, ps) =
+ if not is_set then
apsnd (fn ps => ps @
(if null in_ps then [] else [Pretty.brk 1]) @
separate (Pretty.brk 1) in_ps)
(compile_expr thy defs dep module false modes
(gr2, (mode, t)))
- | _ =>
+ else
apsnd (fn p => [Pretty.str "DSeq.of_list", Pretty.brk 1, p])
- (invoke_codegen thy defs dep module true (gr2, t)));
+ (invoke_codegen thy defs dep module true (gr2, t));
val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
in
(gr4, compile_match (snd nvs) eq_ps out_ps
@@ -504,16 +506,16 @@
fun get_nparms s = if s mem names then SOME nparms else
Option.map #3 (get_clauses thy s);
- fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], u)
- | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq)
+ fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
+ | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
| dest_prem (_ $ t) =
(case strip_comb t of
- (v as Var _, ts) => if v mem args then Prem (ts, v) else Sidecond t
+ (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
| (c as Const (s, _), ts) => (case get_nparms s of
NONE => Sidecond t
| SOME k =>
let val (ts1, ts2) = chop k ts
- in Prem (ts2, list_comb (c, ts1)) end)
+ in Prem (ts2, list_comb (c, ts1), false) end)
| _ => Sidecond t);
fun add_clause intr (clauses, arities) =
--- a/src/HOL/Tools/inductive_set_package.ML Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Wed May 07 10:57:19 2008 +0200
@@ -237,7 +237,7 @@
NONE => thm' RS sym
| SOME fs' =>
let
- val U = HOLogic.dest_setT (body_type T);
+ val (_, U) = split_last (binder_types T);
val Ts = HOLogic.prodT_factors' fs' U;
(* FIXME: should cterm_instantiate increment indexes? *)
val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
@@ -413,7 +413,7 @@
| infer (t $ u) = infer t #> infer u
| infer _ = I;
val new_arities = filter_out
- (fn (x as Free (_, Type ("fun", _)), _) => x mem params
+ (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
| _ => false) (fold (snd #> infer) intros []);
val params' = map (fn x => (case AList.lookup op = new_arities x of
SOME fs =>
@@ -437,7 +437,7 @@
val ((cs', cs_info), eqns) = cs |> map (fn c as Free (s, T) =>
let
val fs = the_default [] (AList.lookup op = new_arities c);
- val U = HOLogic.dest_setT (body_type T);
+ val (_, U) = split_last (binder_types T);
val Ts = HOLogic.prodT_factors' fs U;
val c' = Free (s ^ "p",
map fastype_of params1 @ Ts ---> HOLogic.boolT)
--- a/src/HOL/UNITY/ELT.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/UNITY/ELT.thy Wed May 07 10:57:19 2008 +0200
@@ -102,7 +102,7 @@
apply (simp (no_asm_use) add: givenBy_eq_Collect)
apply safe
apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI)
-unfolding set_diff_def
+unfolding set_diff_eq
apply auto
done
--- a/src/HOL/UNITY/Transformers.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOL/UNITY/Transformers.thy Wed May 07 10:57:19 2008 +0200
@@ -88,7 +88,7 @@
done
lemma wens_Id [simp]: "wens F Id B = B"
-by (simp add: wens_def gfp_def wp_def awp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def Sup_set_eq, blast)
text{*These two theorems justify the claim that @{term wens} returns the
weakest assertion satisfying the ensures property*}
@@ -101,7 +101,7 @@
lemma wens_ensures: "act \<in> Acts F ==> F \<in> (wens F act B) ensures B"
by (simp add: wens_def gfp_def constrains_def awp_def wp_def
- ensures_def transient_def Sup_set_def, blast)
+ ensures_def transient_def Sup_set_eq, blast)
text{*These two results constitute assertion (4.13) of the thesis*}
lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
@@ -110,7 +110,7 @@
done
lemma wens_weakening: "B \<subseteq> wens F act B"
-by (simp add: wens_def gfp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def Sup_set_eq, blast)
text{*Assertion (6), or 4.16 in the thesis*}
lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B"
@@ -120,7 +120,7 @@
text{*Assertion 4.17 in the thesis*}
lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
-by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def awp_def constrains_def Sup_set_eq, blast)
--{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
is declared as an iff-rule, then it's almost impossible to prove.
One proof is via @{text meson} after expanding all definitions, but it's
@@ -331,7 +331,7 @@
lemma wens_single_eq:
"wens (mk_program (init, {act}, allowed)) act B = B \<union> wp act B"
-by (simp add: wens_def gfp_def wp_def Sup_set_def, blast)
+by (simp add: wens_def gfp_def wp_def Sup_set_eq, blast)
text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
--- a/src/HOLCF/CompactBasis.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy Wed May 07 10:57:19 2008 +0200
@@ -227,7 +227,7 @@
lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
unfolding principal_less_iff
-by (simp add: less_def subset_def)
+by (simp add: less_def subset_eq)
lemma lub_principal_approxes: "principal ` approxes x <<| x"
apply (rule is_lubI)
--- a/src/HOLCF/ConvexPD.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy Wed May 07 10:57:19 2008 +0200
@@ -151,7 +151,7 @@
by (rule Rep_convex_pd [simplified])
lemma Rep_convex_pd_mono: "xs \<sqsubseteq> ys \<Longrightarrow> Rep_convex_pd xs \<subseteq> Rep_convex_pd ys"
-unfolding less_convex_pd_def less_set_def .
+unfolding less_convex_pd_def less_set_eq .
subsection {* Principal ideals *}
@@ -179,12 +179,12 @@
apply (rule ideal_Rep_convex_pd)
apply (rule cont_Rep_convex_pd)
apply (rule Rep_convex_principal)
-apply (simp only: less_convex_pd_def less_set_def)
+apply (simp only: less_convex_pd_def less_set_eq)
done
lemma convex_principal_less_iff [simp]:
"(convex_principal t \<sqsubseteq> convex_principal u) = (t \<le>\<natural> u)"
-unfolding less_convex_pd_def Rep_convex_principal less_set_def
+unfolding less_convex_pd_def Rep_convex_principal less_set_eq
by (fast intro: convex_le_refl elim: convex_le_trans)
lemma convex_principal_mono:
--- a/src/HOLCF/IOA/meta_theory/Automata.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed May 07 10:57:19 2008 +0200
@@ -300,33 +300,33 @@
lemma externals_of_par: "ext (A1||A2) =
(ext A1) Un (ext A2)"
apply (simp add: externals_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def Un_def set_diff_def)
+ asig_inputs_def asig_outputs_def Un_def set_diff_eq)
apply blast
done
lemma actions_of_par: "act (A1||A2) =
(act A1) Un (act A2)"
apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
+ asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
apply blast
done
lemma inputs_of_par: "inp (A1||A2) =
((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def Un_def set_diff_def)
+ asig_inputs_def asig_outputs_def Un_def set_diff_eq)
done
lemma outputs_of_par: "out (A1||A2) =
(out A1) Un (out A2)"
apply (simp add: actions_def asig_of_par asig_comp_def
- asig_outputs_def Un_def set_diff_def)
+ asig_outputs_def Un_def set_diff_eq)
done
lemma internals_of_par: "int (A1||A2) =
(int A1) Un (int A2)"
apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_def)
+ asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
done
--- a/src/HOLCF/LowerPD.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/LowerPD.thy Wed May 07 10:57:19 2008 +0200
@@ -106,7 +106,7 @@
by (rule Rep_lower_pd [simplified])
lemma Rep_lower_pd_mono: "x \<sqsubseteq> y \<Longrightarrow> Rep_lower_pd x \<subseteq> Rep_lower_pd y"
-unfolding less_lower_pd_def less_set_def .
+unfolding less_lower_pd_def less_set_eq .
subsection {* Principal ideals *}
@@ -134,12 +134,12 @@
apply (rule ideal_Rep_lower_pd)
apply (rule cont_Rep_lower_pd)
apply (rule Rep_lower_principal)
-apply (simp only: less_lower_pd_def less_set_def)
+apply (simp only: less_lower_pd_def less_set_eq)
done
lemma lower_principal_less_iff [simp]:
"(lower_principal t \<sqsubseteq> lower_principal u) = (t \<le>\<flat> u)"
-unfolding less_lower_pd_def Rep_lower_principal less_set_def
+unfolding less_lower_pd_def Rep_lower_principal less_set_eq
by (fast intro: lower_le_refl elim: lower_le_trans)
lemma lower_principal_mono:
@@ -151,7 +151,7 @@
apply (simp add: less_lower_pd_def)
apply (simp add: cont2contlubE [OF cont_Rep_lower_pd])
apply (simp add: Rep_lower_principal set_cpo_simps)
-apply (simp add: subset_def)
+apply (simp add: subset_eq)
apply (drule spec, drule mp, rule lower_le_refl)
apply (erule exE, rename_tac i)
apply (rule_tac x=i in exI)
--- a/src/HOLCF/UpperPD.thy Wed May 07 10:56:58 2008 +0200
+++ b/src/HOLCF/UpperPD.thy Wed May 07 10:57:19 2008 +0200
@@ -126,12 +126,12 @@
apply (rule ideal_Rep_upper_pd)
apply (rule cont_Rep_upper_pd)
apply (rule Rep_upper_principal)
-apply (simp only: less_upper_pd_def less_set_def)
+apply (simp only: less_upper_pd_def less_set_eq)
done
lemma upper_principal_less_iff [simp]:
"(upper_principal t \<sqsubseteq> upper_principal u) = (t \<le>\<sharp> u)"
-unfolding less_upper_pd_def Rep_upper_principal less_set_def
+unfolding less_upper_pd_def Rep_upper_principal less_set_eq
by (fast intro: upper_le_refl elim: upper_le_trans)
lemma upper_principal_mono: