--- a/src/HOL/Library/Quotient_List.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Library/Quotient_List.thy Tue Nov 09 16:18:40 2010 +0100
@@ -82,21 +82,15 @@
apply(rule list_all2_rel[OF q])
done
-lemma cons_prs_aux:
- assumes q: "Quotient R Abs Rep"
- shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
- by (induct t) (simp_all add: Quotient_abs_rep[OF q])
-
lemma cons_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
- by (simp only: fun_eq_iff fun_map_def cons_prs_aux[OF q])
- (simp)
+ by (auto simp add: fun_eq_iff comp_def Quotient_abs_rep [OF q])
lemma cons_rsp[quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "(R ===> list_all2 R ===> list_all2 R) (op #) (op #)"
- by (auto)
+ by auto
lemma nil_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
@@ -120,15 +114,16 @@
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
and "((abs1 ---> id) ---> map rep1 ---> id) map = map"
- by (simp_all only: fun_eq_iff fun_map_def map_prs_aux[OF a b])
- (simp_all add: Quotient_abs_rep[OF a])
+ by (simp_all only: fun_eq_iff map_prs_aux[OF a b] comp_def)
+ (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
+
lemma map_rsp[quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "((R1 ===> R2) ===> (list_all2 R1) ===> list_all2 R2) map map"
and "((R1 ===> op =) ===> (list_all2 R1) ===> op =) map map"
- apply simp_all
+ apply (simp_all add: fun_rel_def)
apply(rule_tac [!] allI)+
apply(rule_tac [!] impI)
apply(rule_tac [!] allI)+
@@ -146,7 +141,8 @@
assumes a: "Quotient R1 abs1 rep1"
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
- by (simp only: fun_eq_iff fun_map_def foldr_prs_aux[OF a b])
+ apply (simp add: fun_eq_iff)
+ by (simp only: fun_eq_iff foldr_prs_aux[OF a b])
(simp)
lemma foldl_prs_aux:
@@ -160,8 +156,7 @@
assumes a: "Quotient R1 abs1 rep1"
and b: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
- by (simp only: fun_eq_iff fun_map_def foldl_prs_aux[OF a b])
- (simp)
+ by (simp add: fun_eq_iff foldl_prs_aux [OF a b])
lemma list_all2_empty:
shows "list_all2 R [] b \<Longrightarrow> length b = 0"
@@ -172,7 +167,7 @@
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_all2 R2 ===> R1) foldl foldl"
- apply(auto)
+ apply(auto simp add: fun_rel_def)
apply (subgoal_tac "R1 xa ya \<longrightarrow> list_all2 R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
apply simp
apply (rule_tac x="xa" in spec)
@@ -186,7 +181,7 @@
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
shows "((R1 ===> R2 ===> R2) ===> list_all2 R1 ===> R2 ===> R2) foldr foldr"
- apply auto
+ apply (auto simp add: fun_rel_def)
apply(subgoal_tac "R2 xb yb \<longrightarrow> list_all2 R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
apply simp
apply (rule_tac xs="xa" and ys="ya" in list_induct2)
@@ -224,7 +219,7 @@
lemma[quot_respect]:
"((R ===> R ===> op =) ===> list_all2 R ===> list_all2 R ===> op =) list_all2 list_all2"
- by (simp add: list_all2_rsp)
+ by (simp add: list_all2_rsp fun_rel_def)
lemma[quot_preserve]:
assumes a: "Quotient R abs1 rep1"
--- a/src/HOL/Library/Quotient_Option.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Library/Quotient_Option.thy Tue Nov 09 16:18:40 2010 +0100
@@ -9,7 +9,7 @@
begin
fun
- option_rel
+ option_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
where
"option_rel R None None = True"
| "option_rel R (Some x) None = False"
@@ -56,7 +56,7 @@
lemma option_Some_rsp[quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "(R ===> option_rel R) Some Some"
- by simp
+ by auto
lemma option_None_prs[quot_preserve]:
assumes q: "Quotient R Abs Rep"
--- a/src/HOL/Library/Quotient_Product.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Library/Quotient_Product.thy Tue Nov 09 16:18:40 2010 +0100
@@ -8,13 +8,16 @@
imports Main Quotient_Syntax
begin
-fun
- prod_rel
+definition
+ prod_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
declare [[map prod = (prod_fun, prod_rel)]]
+lemma prod_rel_apply [simp]:
+ "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
+ by (simp add: prod_rel_def)
lemma prod_equivp[quot_equiv]:
assumes a: "equivp R1"
@@ -22,7 +25,7 @@
shows "equivp (prod_rel R1 R2)"
apply(rule equivpI)
unfolding reflp_def symp_def transp_def
- apply(simp_all add: split_paired_all)
+ apply(simp_all add: split_paired_all prod_rel_def)
apply(blast intro: equivp_reflp[OF a] equivp_reflp[OF b])
apply(blast intro: equivp_symp[OF a] equivp_symp[OF b])
apply(blast intro: equivp_transp[OF a] equivp_transp[OF b])
@@ -45,7 +48,7 @@
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
- by simp
+ by (auto simp add: prod_rel_def)
lemma Pair_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -59,33 +62,29 @@
assumes "Quotient R1 Abs1 Rep1"
assumes "Quotient R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R1) fst fst"
- by simp
+ by auto
lemma fst_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
- apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q1])
- done
+ by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
lemma snd_rsp[quot_respect]:
assumes "Quotient R1 Abs1 Rep1"
assumes "Quotient R2 Abs2 Rep2"
shows "(prod_rel R1 R2 ===> R2) snd snd"
- by simp
+ by auto
lemma snd_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
- apply(simp add: fun_eq_iff)
- apply(simp add: Quotient_abs_rep[OF q2])
- done
+ by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
lemma split_rsp[quot_respect]:
shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
- by auto
+ by (auto intro!: fun_relI elim!: fun_relE)
lemma split_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -96,7 +95,7 @@
lemma [quot_respect]:
shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
- by auto
+ by (auto simp add: fun_rel_def)
lemma [quot_preserve]:
assumes q1: "Quotient R1 abs1 rep1"
@@ -114,7 +113,7 @@
lemma prod_fun_id[id_simps]:
shows "prod_fun id id = id"
- by (simp add: prod_fun_def)
+ by (simp add: fun_eq_iff)
lemma prod_rel_eq[id_simps]:
shows "prod_rel (op =) (op =) = (op =)"
--- a/src/HOL/Library/Quotient_Sum.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Nov 09 16:18:40 2010 +0100
@@ -9,15 +9,15 @@
begin
fun
- sum_rel
+ sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
where
"sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-fun
- sum_map
+primrec
+ sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
where
"sum_map f1 f2 (Inl a) = Inl (f1 a)"
| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
@@ -62,13 +62,13 @@
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R1 ===> sum_rel R1 R2) Inl Inl"
- by simp
+ by auto
lemma sum_Inr_rsp[quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
shows "(R2 ===> sum_rel R1 R2) Inr Inr"
- by simp
+ by auto
lemma sum_Inl_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
--- a/src/HOL/Quotient.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Quotient.thy Tue Nov 09 16:18:40 2010 +0100
@@ -5,7 +5,7 @@
header {* Definition of Quotient Types *}
theory Quotient
-imports Plain Hilbert_Choice
+imports Plain Hilbert_Choice Equiv_Relations
uses
("Tools/Quotient/quotient_info.ML")
("Tools/Quotient/quotient_typ.ML")
@@ -21,33 +21,49 @@
*}
definition
- "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+ "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+
+lemma refl_reflp:
+ "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
+ by (simp add: refl_on_def reflp_def)
definition
- "reflp E \<equiv> \<forall>x. E x x"
+ "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+
+lemma sym_symp:
+ "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
+ by (simp add: sym_def symp_def)
definition
- "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+ "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+
+lemma trans_transp:
+ "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
+ by (auto simp add: trans_def transp_def)
definition
- "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+ "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
lemma equivp_reflp_symp_transp:
shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
by blast
+lemma equiv_equivp:
+ "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
+ by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
+
lemma equivp_reflp:
shows "equivp E \<Longrightarrow> E x x"
by (simp only: equivp_reflp_symp_transp reflp_def)
lemma equivp_symp:
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
- by (metis equivp_reflp_symp_transp symp_def)
+ by (simp add: equivp_def)
lemma equivp_transp:
shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
- by (metis equivp_reflp_symp_transp transp_def)
+ by (simp add: equivp_def)
lemma equivpI:
assumes "reflp R" "symp R" "transp R"
@@ -62,7 +78,7 @@
text {* Partial equivalences *}
definition
- "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
+ "part_equivp E \<longleftrightarrow> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
lemma equivp_implies_part_equivp:
assumes a: "equivp E"
@@ -114,6 +130,11 @@
then show "part_equivp E" unfolding part_equivp_def using a by metis
qed
+lemma part_equivpI:
+ assumes "\<exists>x. R x x" "symp R" "transp R"
+ shows "part_equivp R"
+ using assms by (simp add: part_equivp_refl_symp_transp)
+
text {* Composition of Relations *}
abbreviation
@@ -128,45 +149,54 @@
subsection {* Respects predicate *}
definition
- Respects
+ Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
where
- "Respects R x \<equiv> R x x"
+ "Respects R x = R x x"
lemma in_respects:
- shows "(x \<in> Respects R) = R x x"
+ shows "x \<in> Respects R \<longleftrightarrow> R x x"
unfolding mem_def Respects_def
by simp
subsection {* Function map and function relation *}
definition
- fun_map (infixr "--->" 55)
+ fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
where
-[simp]: "fun_map f g h x = g (h (f x))"
+ "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
+
+lemma fun_map_apply [simp]:
+ "(f ---> g) h x = g (h (f x))"
+ by (simp add: fun_map_def)
+
+lemma fun_map_id:
+ "(id ---> id) = id"
+ by (simp add: fun_eq_iff id_def)
definition
- fun_rel (infixr "===>" 55)
+ fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
where
-[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+ "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
lemma fun_relI [intro]:
- assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
- shows "(P ===> Q) x y"
+ assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
+ shows "(E1 ===> E2) f g"
using assms by (simp add: fun_rel_def)
-lemma fun_map_id:
- shows "(id ---> id) = id"
- by (simp add: fun_eq_iff id_def)
+lemma fun_relE:
+ assumes "(E1 ===> E2) f g" and "E1 x y"
+ obtains "E2 (f x) (g y)"
+ using assms by (simp add: fun_rel_def)
lemma fun_rel_eq:
shows "((op =) ===> (op =)) = (op =)"
- by (simp add: fun_eq_iff)
+ by (auto simp add: fun_eq_iff elim: fun_relE)
subsection {* Quotient Predicate *}
definition
- "Quotient E Abs Rep \<equiv>
+ "Quotient E Abs Rep \<longleftrightarrow>
(\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
(\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
@@ -232,21 +262,17 @@
and q2: "Quotient R2 abs2 rep2"
shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
proof -
- have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
- using q1 q2
- unfolding Quotient_def
- unfolding fun_eq_iff
- by simp
+ have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
+ using q1 q2 by (simp add: Quotient_def fun_eq_iff)
moreover
- have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
- using q1 q2
- unfolding Quotient_def
- by (simp (no_asm)) (metis)
+ have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
+ by (rule fun_relI)
+ (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
+ simp (no_asm) add: Quotient_def, simp)
moreover
- have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
+ have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
(rep1 ---> abs2) r = (rep1 ---> abs2) s)"
- unfolding fun_eq_iff
- apply(auto)
+ apply(auto simp add: fun_rel_def fun_eq_iff)
using q1 q2 unfolding Quotient_def
apply(metis)
using q1 q2 unfolding Quotient_def
@@ -281,7 +307,7 @@
shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
unfolding fun_eq_iff
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
- by simp
+ by (simp add:)
lemma lambda_prs1:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -289,7 +315,7 @@
shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
unfolding fun_eq_iff
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
- by simp
+ by (simp add:)
lemma rep_abs_rsp:
assumes q: "Quotient R Abs Rep"
@@ -317,12 +343,12 @@
assumes q: "Quotient R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
- using a by simp
+ using a by (auto elim: fun_relE)
lemma apply_rsp':
assumes a: "(R1 ===> R2) f g" "R1 x y"
shows "R2 (f x) (g y)"
- using a by simp
+ using a by (auto elim: fun_relE)
subsection {* lemmas for regularisation of ball and bex *}
@@ -370,7 +396,7 @@
apply(rule iffI)
apply(rule allI)
apply(drule_tac x="\<lambda>y. f x" in bspec)
- apply(simp add: in_respects)
+ apply(simp add: in_respects fun_rel_def)
apply(rule impI)
using a equivp_reflp_symp_transp[of "R2"]
apply(simp add: reflp_def)
@@ -384,7 +410,7 @@
apply(auto)
apply(rule_tac x="\<lambda>y. f x" in bexI)
apply(simp)
- apply(simp add: Respects_def in_respects)
+ apply(simp add: Respects_def in_respects fun_rel_def)
apply(rule impI)
using a equivp_reflp_symp_transp[of "R2"]
apply(simp add: reflp_def)
@@ -429,7 +455,7 @@
subsection {* Bounded abstraction *}
definition
- Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+ Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
where
"x \<in> p \<Longrightarrow> Babs p m x = m x"
@@ -437,10 +463,10 @@
assumes q: "Quotient R1 Abs1 Rep1"
and a: "(R1 ===> R2) f g"
shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
- apply (auto simp add: Babs_def in_respects)
+ apply (auto simp add: Babs_def in_respects fun_rel_def)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
- using a apply (simp add: Babs_def)
- apply (simp add: in_respects)
+ using a apply (simp add: Babs_def fun_rel_def)
+ apply (simp add: in_respects fun_rel_def)
using Quotient_rel[OF q]
by metis
@@ -449,7 +475,7 @@
and q2: "Quotient R2 Abs2 Rep2"
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
apply (rule ext)
- apply (simp)
+ apply (simp add:)
apply (subgoal_tac "Rep1 x \<in> Respects R1")
apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
apply (simp add: in_respects Quotient_rel_rep[OF q1])
@@ -460,7 +486,7 @@
shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
apply(rule iffI)
apply(simp_all only: babs_rsp[OF q])
- apply(auto simp add: Babs_def)
+ apply(auto simp add: Babs_def fun_rel_def)
apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
apply(metis Babs_def)
apply (simp add: in_respects)
@@ -478,30 +504,29 @@
lemma ball_rsp:
assumes a: "(R ===> (op =)) f g"
shows "Ball (Respects R) f = Ball (Respects R) g"
- using a by (simp add: Ball_def in_respects)
+ using a by (auto simp add: Ball_def in_respects elim: fun_relE)
lemma bex_rsp:
assumes a: "(R ===> (op =)) f g"
shows "(Bex (Respects R) f = Bex (Respects R) g)"
- using a by (simp add: Bex_def in_respects)
+ using a by (auto simp add: Bex_def in_respects elim: fun_relE)
lemma bex1_rsp:
assumes a: "(R ===> (op =)) f g"
shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
- using a
- by (simp add: Ex1_def in_respects) auto
+ using a by (auto elim: fun_relE simp add: Ex1_def in_respects)
(* 2 lemmas needed for cleaning of quantifiers *)
lemma all_prs:
assumes a: "Quotient R absf repf"
shows "Ball (Respects R) ((absf ---> id) f) = All f"
- using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
+ using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
by metis
lemma ex_prs:
assumes a: "Quotient R absf repf"
shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
- using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
+ using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
by metis
subsection {* @{text Bex1_rel} quantifier *}
@@ -552,7 +577,7 @@
lemma bex1_rel_rsp:
assumes a: "Quotient R absf repf"
shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
- apply simp
+ apply (simp add: fun_rel_def)
apply clarify
apply rule
apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
@@ -564,7 +589,7 @@
lemma ex1_prs:
assumes a: "Quotient R absf repf"
shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
-apply simp
+apply (simp add:)
apply (subst Bex1_rel_def)
apply (subst Bex_def)
apply (subst Ex1_def)
@@ -643,12 +668,12 @@
shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
and "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
- unfolding o_def fun_eq_iff by simp_all
+ by (simp_all add: fun_eq_iff)
lemma o_rsp:
"((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
"(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
- unfolding fun_rel_def o_def fun_eq_iff by auto
+ by (auto intro!: fun_relI elim: fun_relE)
lemma cond_prs:
assumes a: "Quotient R absf repf"
@@ -664,7 +689,7 @@
lemma if_rsp:
assumes q: "Quotient R Abs Rep"
shows "(op = ===> R ===> R ===> R) If If"
- by auto
+ by (auto intro!: fun_relI)
lemma let_prs:
assumes q1: "Quotient R1 Abs1 Rep1"
@@ -675,11 +700,11 @@
lemma let_rsp:
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
- by auto
+ by (auto intro!: fun_relI elim: fun_relE)
lemma mem_rsp:
shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
- by (simp add: mem_def)
+ by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
lemma mem_prs:
assumes a1: "Quotient R1 Abs1 Rep1"
@@ -689,13 +714,12 @@
lemma id_rsp:
shows "(R ===> R) id id"
- by simp
+ by (auto intro: fun_relI)
lemma id_prs:
assumes a: "Quotient R Abs Rep"
shows "(Rep ---> Abs) id = id"
- unfolding fun_eq_iff
- by (simp add: Quotient_abs_rep[OF a])
+ by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
locale quot_type =
@@ -710,12 +734,12 @@
begin
definition
- abs::"'a \<Rightarrow> 'b"
+ abs :: "'a \<Rightarrow> 'b"
where
- "abs x \<equiv> Abs (R x)"
+ "abs x = Abs (R x)"
definition
- rep::"'b \<Rightarrow> 'a"
+ rep :: "'b \<Rightarrow> 'a"
where
"rep a = Eps (Rep a)"
@@ -799,7 +823,9 @@
about the lifted theorem in a tactic.
*}
definition
- "Quot_True (x :: 'a) \<equiv> True"
+ Quot_True :: "'a \<Rightarrow> bool"
+where
+ "Quot_True x \<longleftrightarrow> True"
lemma
shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
@@ -858,4 +884,3 @@
fun_rel (infixr "===>" 55)
end
-
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Nov 09 16:18:40 2010 +0100
@@ -14,10 +14,10 @@
over lists. The definition of the equivalence:
*}
-fun
+definition
list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
- "list_eq xs ys \<longleftrightarrow> set xs = set ys"
+ [simp]: "list_eq xs ys \<longleftrightarrow> set xs = set ys"
lemma list_eq_equivp:
shows "equivp list_eq"
@@ -96,8 +96,7 @@
qed
lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
- unfolding list_eq.simps
- by (simp only: set_map)
+ by (simp only: list_eq_def set_map)
lemma quotient_compose_list_g:
assumes q: "Quotient R Abs Rep"
@@ -167,19 +166,19 @@
lemma list_equiv_rsp [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
- by auto
+ by (auto intro!: fun_relI)
lemma append_rsp [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
- by simp
+ by (auto intro!: fun_relI)
lemma sub_list_rsp [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
- by simp
+ by (auto intro!: fun_relI)
lemma memb_rsp [quot_respect]:
shows "(op = ===> op \<approx> ===> op =) memb memb"
- by simp
+ by (auto intro!: fun_relI)
lemma nil_rsp [quot_respect]:
shows "(op \<approx>) Nil Nil"
@@ -187,35 +186,35 @@
lemma cons_rsp [quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
- by simp
+ by (auto intro!: fun_relI)
lemma map_rsp [quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) map map"
- by auto
+ by (auto intro!: fun_relI)
lemma set_rsp [quot_respect]:
"(op \<approx> ===> op =) set set"
- by auto
+ by (auto intro!: fun_relI)
lemma inter_list_rsp [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
- by simp
+ by (auto intro!: fun_relI)
lemma removeAll_rsp [quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
- by simp
+ by (auto intro!: fun_relI)
lemma diff_list_rsp [quot_respect]:
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
- by simp
+ by (auto intro!: fun_relI)
lemma card_list_rsp [quot_respect]:
shows "(op \<approx> ===> op =) card_list card_list"
- by simp
+ by (auto intro!: fun_relI)
lemma filter_rsp [quot_respect]:
shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
- by simp
+ by (auto intro!: fun_relI)
lemma memb_commute_fold_list:
assumes a: "rsp_fold f"
@@ -348,13 +347,11 @@
"minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
instance
proof
fix x y z :: "'a fset"
show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
- unfolding less_fset_def
- by (descending) (auto)
+ by (unfold less_fset_def, descending) auto
show "x |\<subseteq>| x" by (descending) (simp)
show "{||} |\<subseteq>| x" by (descending) (simp)
show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
@@ -451,7 +448,7 @@
lemma Cons_rsp2 [quot_respect]:
shows "(op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) Cons Cons"
- apply auto
+ apply (auto intro!: fun_relI)
apply (rule_tac b="x # b" in pred_compI)
apply auto
apply (rule_tac b="x # ba" in pred_compI)
@@ -477,7 +474,7 @@
assumes a: "reflp R"
and b: "list_all2 R l r"
shows "list_all2 R (z @ l) (z @ r)"
- by (induct z) (simp_all add: b rev_iffD1[OF a meta_eq_to_obj_eq[OF reflp_def]])
+ by (induct z) (simp_all add: b rev_iffD1 [OF a reflp_def])
lemma append_rsp2_pre0:
assumes a:"list_all2 op \<approx> x x'"
@@ -490,7 +487,7 @@
shows "list_all2 op \<approx> (z @ x) (z @ x')"
using a apply (induct x x' arbitrary: z rule: list_induct2')
apply (rule list_all2_refl'[OF list_eq_equivp])
- apply (simp_all del: list_eq.simps)
+ apply (simp_all del: list_eq_def)
apply (rule list_all2_app_l)
apply (simp_all add: reflp_def)
done
@@ -760,7 +757,7 @@
lemma inj_map_fset_cong:
shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
- by (descending) (metis inj_vimage_image_eq list_eq.simps set_map)
+ by (descending) (metis inj_vimage_image_eq list_eq_def set_map)
lemma map_union_fset:
shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
@@ -1111,7 +1108,7 @@
apply(blast)
done
then obtain a where e: "memb a l" by auto
- then have e': "memb a r" using list_eq.simps[simplified memb_def[symmetric], of l r] b
+ then have e': "memb a r" using list_eq_def [simplified memb_def [symmetric], of l r] b
by auto
have f: "card_list (removeAll a l) = m" using e d by (simp)
have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Tue Nov 09 16:18:40 2010 +0100
@@ -77,7 +77,7 @@
shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
- by auto
+ by (auto intro!: fun_relI)
lemma times_int_raw_fst:
assumes a: "x \<approx> z"
@@ -167,7 +167,7 @@
lemma[quot_respect]:
shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
- by (simp add: equivp_reflp[OF int_equivp])
+ by (auto simp add: equivp_reflp [OF int_equivp])
lemma int_of_nat:
shows "of_nat m = int_of_nat m"
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Tue Nov 09 16:18:40 2010 +0100
@@ -179,11 +179,11 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op =) freenonces freenonces"
- by (simp add: msgrel_imp_eq_freenonces)
+ by (auto simp add: msgrel_imp_eq_freenonces)
lemma [quot_respect]:
shows "(op = ===> op \<sim>) NONCE NONCE"
- by (simp add: NONCE)
+ by (auto simp add: NONCE)
lemma nonces_Nonce [simp]:
shows "nonces (Nonce N) = {N}"
@@ -191,7 +191,7 @@
lemma [quot_respect]:
shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
- by (simp add: MPAIR)
+ by (auto simp add: MPAIR)
lemma nonces_MPair [simp]:
shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
@@ -214,7 +214,7 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
- by (simp add: msgrel_imp_eqv_freeleft)
+ by (auto simp add: msgrel_imp_eqv_freeleft)
lemma left_Nonce [simp]:
shows "left (Nonce N) = Nonce N"
@@ -243,7 +243,7 @@
lemma [quot_respect]:
shows "(op \<sim> ===> op \<sim>) freeright freeright"
- by (simp add: msgrel_imp_eqv_freeright)
+ by (auto simp add: msgrel_imp_eqv_freeright)
lemma right_Nonce [simp]:
shows "right (Nonce N) = Nonce N"
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Nov 09 14:00:10 2010 +0000
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Nov 09 16:18:40 2010 +0100
@@ -434,7 +434,7 @@
((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
if member (op=) xs h
then Conv.all_conv ctrm
- else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm
+ else Conv.rewr_conv @{thm fun_map_apply [THEN eq_reflection]} ctrm
| _ => Conv.all_conv ctrm
fun fun_map_conv xs ctxt ctrm =