--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 14:17:29 2012 +0100
@@ -115,6 +115,7 @@
"add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u\<Colon>nat), y + (v\<Colon>nat))"
quotient_definition "add\<Colon>my_int \<Rightarrow> my_int \<Rightarrow> my_int" is add_raw
+unfolding add_raw_def by auto
lemma "add x y = add x x"
nitpick [show_datatypes, expect = genuine]
--- a/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 14:17:29 2012 +0100
@@ -88,45 +88,32 @@
definition [simp]: "card_remdups = length \<circ> remdups"
definition [simp]: "foldr_remdups f xs e = foldr f (remdups xs) e"
-lemma [quot_respect]:
- "(dlist_eq) Nil Nil"
- "(dlist_eq ===> op =) List.member List.member"
- "(op = ===> dlist_eq ===> dlist_eq) Cons Cons"
- "(op = ===> dlist_eq ===> dlist_eq) removeAll removeAll"
- "(dlist_eq ===> op =) card_remdups card_remdups"
- "(dlist_eq ===> op =) remdups remdups"
- "(op = ===> dlist_eq ===> op =) foldr_remdups foldr_remdups"
- "(op = ===> dlist_eq ===> dlist_eq) map map"
- "(op = ===> dlist_eq ===> dlist_eq) filter filter"
- by (auto intro!: fun_relI simp add: remdups_filter)
- (metis (full_types) set_remdups remdups_eq_map_eq remdups_eq_member_eq)+
-
quotient_definition empty where "empty :: 'a dlist"
- is "Nil"
+ is "Nil" done
quotient_definition insert where "insert :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
- is "Cons"
+ is "Cons" by (metis (mono_tags) List.insert_def dlist_eq_def remdups.simps(2) set_remdups)
quotient_definition "member :: 'a dlist \<Rightarrow> 'a \<Rightarrow> bool"
- is "List.member"
+ is "List.member" by (metis dlist_eq_def remdups_eq_member_eq)
quotient_definition foldr where "foldr :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b \<Rightarrow> 'b"
- is "foldr_remdups"
+ is "foldr_remdups" by auto
quotient_definition "remove :: 'a \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
- is "removeAll"
+ is "removeAll" by force
quotient_definition card where "card :: 'a dlist \<Rightarrow> nat"
- is "card_remdups"
+ is "card_remdups" by fastforce
quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a dlist \<Rightarrow> 'b dlist"
- is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
+ is "List.map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" by (metis dlist_eq_def remdups_eq_map_eq)
quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a dlist \<Rightarrow> 'a dlist"
- is "List.filter"
+ is "List.filter" by (metis dlist_eq_def remdups_filter)
quotient_definition "list_of_dlist :: 'a dlist \<Rightarrow> 'a list"
- is "remdups"
+ is "remdups" by simp
text {* lifted theorems *}
--- a/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 14:17:29 2012 +0100
@@ -179,140 +179,6 @@
by (rule quotient_compose_list_g, rule Quotient_fset, rule list_eq_equivp)
-
-subsection {* Respectfulness lemmas for list operations *}
-
-lemma list_equiv_rsp [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
- by (auto intro!: fun_relI)
-
-lemma append_rsp [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append"
- by (auto intro!: fun_relI)
-
-lemma sub_list_rsp [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list"
- by (auto intro!: fun_relI)
-
-lemma member_rsp [quot_respect]:
- shows "(op \<approx> ===> op =) List.member List.member"
-proof
- fix x y assume "x \<approx> y"
- then show "List.member x = List.member y"
- unfolding fun_eq_iff by simp
-qed
-
-lemma nil_rsp [quot_respect]:
- shows "(op \<approx>) Nil Nil"
- by simp
-
-lemma cons_rsp [quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) Cons Cons"
- by (auto intro!: fun_relI)
-
-lemma map_rsp [quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) map map"
- by (auto intro!: fun_relI)
-
-lemma set_rsp [quot_respect]:
- "(op \<approx> ===> op =) set set"
- by (auto intro!: fun_relI)
-
-lemma inter_list_rsp [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) inter_list inter_list"
- by (auto intro!: fun_relI)
-
-lemma removeAll_rsp [quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) removeAll removeAll"
- by (auto intro!: fun_relI)
-
-lemma diff_list_rsp [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) diff_list diff_list"
- by (auto intro!: fun_relI)
-
-lemma card_list_rsp [quot_respect]:
- shows "(op \<approx> ===> op =) card_list card_list"
- by (auto intro!: fun_relI)
-
-lemma filter_rsp [quot_respect]:
- shows "(op = ===> op \<approx> ===> op \<approx>) filter filter"
- by (auto intro!: fun_relI)
-
-lemma remdups_removeAll: (*FIXME move*)
- "remdups (removeAll x xs) = remove1 x (remdups xs)"
- by (induct xs) auto
-
-lemma member_commute_fold_once:
- assumes "rsp_fold f"
- and "x \<in> set xs"
- shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
-proof -
- from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
- by (auto intro!: fold_remove1_split elim: rsp_foldE)
- then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
-qed
-
-lemma fold_once_set_equiv:
- assumes "xs \<approx> ys"
- shows "fold_once f xs = fold_once f ys"
-proof (cases "rsp_fold f")
- case False then show ?thesis by simp
-next
- case True
- then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
- by (rule rsp_foldE)
- moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
- by (simp add: set_eq_iff_multiset_of_remdups_eq)
- ultimately have "fold f (remdups xs) = fold f (remdups ys)"
- by (rule fold_multiset_equiv)
- with True show ?thesis by (simp add: fold_once_fold_remdups)
-qed
-
-lemma fold_once_rsp [quot_respect]:
- shows "(op = ===> op \<approx> ===> op =) fold_once fold_once"
- unfolding fun_rel_def by (auto intro: fold_once_set_equiv)
-
-lemma concat_rsp_pre:
- assumes a: "list_all2 op \<approx> x x'"
- and b: "x' \<approx> y'"
- and c: "list_all2 op \<approx> y' y"
- and d: "\<exists>x\<in>set x. xa \<in> set x"
- shows "\<exists>x\<in>set y. xa \<in> set x"
-proof -
- obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
- have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
- then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
- have "ya \<in> set y'" using b h by simp
- then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
- then show ?thesis using f i by auto
-qed
-
-lemma concat_rsp [quot_respect]:
- shows "(list_all2 op \<approx> OOO op \<approx> ===> op \<approx>) concat concat"
-proof (rule fun_relI, elim pred_compE)
- fix a b ba bb
- assume a: "list_all2 op \<approx> a ba"
- with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
- assume b: "ba \<approx> bb"
- with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
- assume c: "list_all2 op \<approx> bb b"
- with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
- have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
- proof
- fix x
- show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
- proof
- assume d: "\<exists>xa\<in>set a. x \<in> set xa"
- show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
- next
- assume e: "\<exists>xa\<in>set b. x \<in> set xa"
- show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
- qed
- qed
- then show "concat a \<approx> concat b" by auto
-qed
-
-
section {* Quotient definitions for fsets *}
@@ -323,7 +189,7 @@
quotient_definition
"bot :: 'a fset"
- is "Nil :: 'a list"
+ is "Nil :: 'a list" done
abbreviation
empty_fset ("{||}")
@@ -332,7 +198,7 @@
quotient_definition
"less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
- is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)"
+ is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" by simp
abbreviation
subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
@@ -351,7 +217,7 @@
quotient_definition
"sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
abbreviation
union_fset (infixl "|\<union>|" 65)
@@ -360,7 +226,7 @@
quotient_definition
"inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp
abbreviation
inter_fset (infixl "|\<inter>|" 65)
@@ -369,7 +235,7 @@
quotient_definition
"minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by fastforce
instance
proof
@@ -413,7 +279,7 @@
quotient_definition
"insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is "Cons"
+ is "Cons" by auto
syntax
"_insert_fset" :: "args => 'a fset" ("{|(_)|}")
@@ -425,7 +291,7 @@
quotient_definition
fset_member
where
- "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member"
+ "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" by fastforce
abbreviation
in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50)
@@ -442,31 +308,84 @@
quotient_definition
"card_fset :: 'a fset \<Rightarrow> nat"
- is card_list
+ is card_list by simp
quotient_definition
"map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
- is map
+ is map by simp
quotient_definition
"remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is removeAll
+ is removeAll by simp
quotient_definition
"fset :: 'a fset \<Rightarrow> 'a set"
- is "set"
+ is "set" by simp
+
+lemma fold_once_set_equiv:
+ assumes "xs \<approx> ys"
+ shows "fold_once f xs = fold_once f ys"
+proof (cases "rsp_fold f")
+ case False then show ?thesis by simp
+next
+ case True
+ then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
+ by (rule rsp_foldE)
+ moreover from assms have "multiset_of (remdups xs) = multiset_of (remdups ys)"
+ by (simp add: set_eq_iff_multiset_of_remdups_eq)
+ ultimately have "fold f (remdups xs) = fold f (remdups ys)"
+ by (rule fold_multiset_equiv)
+ with True show ?thesis by (simp add: fold_once_fold_remdups)
+qed
quotient_definition
"fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
- is fold_once
+ is fold_once by (rule fold_once_set_equiv)
+
+lemma concat_rsp_pre:
+ assumes a: "list_all2 op \<approx> x x'"
+ and b: "x' \<approx> y'"
+ and c: "list_all2 op \<approx> y' y"
+ and d: "\<exists>x\<in>set x. xa \<in> set x"
+ shows "\<exists>x\<in>set y. xa \<in> set x"
+proof -
+ obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
+ have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
+ then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
+ have "ya \<in> set y'" using b h by simp
+ then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
+ then show ?thesis using f i by auto
+qed
quotient_definition
"concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
- is concat
+ is concat
+proof (elim pred_compE)
+fix a b ba bb
+ assume a: "list_all2 op \<approx> a ba"
+ with list_symp [OF list_eq_symp] have a': "list_all2 op \<approx> ba a" by (rule sympE)
+ assume b: "ba \<approx> bb"
+ with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
+ assume c: "list_all2 op \<approx> bb b"
+ with list_symp [OF list_eq_symp] have c': "list_all2 op \<approx> b bb" by (rule sympE)
+ have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
+ proof
+ fix x
+ show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
+ proof
+ assume d: "\<exists>xa\<in>set a. x \<in> set xa"
+ show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
+ next
+ assume e: "\<exists>xa\<in>set b. x \<in> set xa"
+ show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
+ qed
+ qed
+ then show "concat a \<approx> concat b" by auto
+qed
quotient_definition
"filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
- is filter
+ is filter by force
subsection {* Compositional respectfulness and preservation lemmas *}
@@ -538,7 +457,7 @@
lemma append_rsp2 [quot_respect]:
"(list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx> ===> list_all2 op \<approx> OOO op \<approx>) append append"
- by (intro compositional_rsp3 append_rsp)
+ by (intro compositional_rsp3)
(auto intro!: fun_relI simp add: append_rsp2_pre)
lemma map_rsp2 [quot_respect]:
@@ -967,6 +886,20 @@
(if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
by descending (simp add: fold_once_fold_remdups)
+lemma remdups_removeAll:
+ "remdups (removeAll x xs) = remove1 x (remdups xs)"
+ by (induct xs) auto
+
+lemma member_commute_fold_once:
+ assumes "rsp_fold f"
+ and "x \<in> set xs"
+ shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
+proof -
+ from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
+ by (auto intro!: fold_remove1_split elim: rsp_foldE)
+ then show ?thesis using `rsp_fold f` by (simp add: fold_once_fold_remdups remdups_removeAll)
+qed
+
lemma in_commute_fold_fset:
"rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
by descending (simp add: member_commute_fold_once)
@@ -1170,7 +1103,7 @@
then have e': "List.member r a" using list_eq_def [simplified List.member_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
+ have g: "removeAll a l \<approx> removeAll a r" using remove_fset_rsp b by simp
have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
have i: "l \<approx>2 (a # removeAll a l)"
--- a/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 14:17:29 2012 +0100
@@ -23,17 +23,17 @@
by (simp add: identity_equivp)
quotient_definition "comp' :: ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" is
- "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
+ "comp :: ('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" done
quotient_definition "fcomp' :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'a \<Rightarrow> 'c" is
- fcomp
+ fcomp done
quotient_definition "map_fun' :: ('c \<rightarrow> 'a) \<rightarrow> ('b \<rightarrow> 'd) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'c \<rightarrow> 'd"
- is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd"
+ is "map_fun::('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" done
-quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on
+quotient_definition "inj_on' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> bool" is inj_on done
-quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw
+quotient_definition "bij_betw' :: ('a \<rightarrow> 'b) \<rightarrow> 'a set \<rightarrow> 'b set \<rightarrow> bool" is bij_betw done
subsection {* Co/Contravariant type variables *}
@@ -47,7 +47,7 @@
where "map_endofun' f g e = map_fun g f e"
quotient_definition "map_endofun :: ('a \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun" is
- map_endofun'
+ map_endofun' done
text {* Registration of the map function for 'a endofun. *}
@@ -63,7 +63,7 @@
by (auto simp: map_endofun_def map_endofun'_def map_fun_def fun_eq_iff) (simp add: a o_assoc)
qed
-quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
+quotient_definition "endofun_id_id :: ('a endofun) endofun" is "id :: ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" done
term endofun_id_id
thm endofun_id_id_def
@@ -73,7 +73,7 @@
text {* We have to map "'a endofun" to "('a endofun') endofun", i.e., mapping (lifting)
over a type variable which is a covariant and contravariant type variable. *}
-quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id
+quotient_definition "endofun'_id_id :: ('a endofun') endofun'" is endofun_id_id done
term endofun'_id_id
thm endofun'_id_id_def
--- a/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 14:17:29 2012 +0100
@@ -18,7 +18,7 @@
local_setup {* fn lthy =>
let
val quotients = {qtyp = @{typ "('a, 'b) rbt"}, rtyp = @{typ "('a, 'b) RBT_Impl.rbt"},
- equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+ equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
val qty_full_name = @{type_name "rbt"}
fun qinfo phi = Quotient_Info.transform_quotients phi quotients
@@ -50,6 +50,7 @@
subsection {* Primitive operations *}
quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+done
declare lookup_def[unfolded map_fun_def comp_def id_def, code]
@@ -67,21 +68,21 @@
*)
quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)"
+is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" done
lemma impl_of_empty [code abstract]:
"impl_of empty = RBT_Impl.Empty"
by (simp add: empty_def RBT_inverse)
quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.insert"
+is "RBT_Impl.insert" done
lemma impl_of_insert [code abstract]:
"impl_of (insert k v t) = RBT_Impl.insert k v (impl_of t)"
by (simp add: insert_def RBT_inverse)
quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.delete"
+is "RBT_Impl.delete" done
lemma impl_of_delete [code abstract]:
"impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
@@ -89,24 +90,24 @@
(* FIXME: unnecessary type annotations *)
quotient_definition "entries :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a \<times> 'b) list"
-is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list"
+is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" done
lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
unfolding entries_def map_fun_def comp_def id_def ..
(* FIXME: unnecessary type annotations *)
quotient_definition "keys :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a list"
-is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list"
+is "RBT_Impl.keys :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'a list" done
quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.bulkload"
+is "RBT_Impl.bulkload" done
lemma impl_of_bulkload [code abstract]:
"impl_of (bulkload xs) = RBT_Impl.bulkload xs"
by (simp add: bulkload_def RBT_inverse)
quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map_entry"
+is "RBT_Impl.map_entry" done
lemma impl_of_map_entry [code abstract]:
"impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
@@ -115,13 +116,15 @@
(* FIXME: unnecesary type annotations *)
quotient_definition map where "map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
is "RBT_Impl.map :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a, 'b) RBT_Impl.rbt"
+done
lemma impl_of_map [code abstract]:
"impl_of (map f t) = RBT_Impl.map f (impl_of t)"
by (simp add: map_def RBT_inverse)
(* FIXME: unnecessary type annotations *)
-quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+quotient_definition fold where "fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c"
+is "RBT_Impl.fold :: ('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> 'c \<Rightarrow> 'c" done
lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
unfolding fold_def map_fun_def comp_def id_def ..
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 14:17:29 2012 +0100
@@ -20,7 +20,7 @@
let
val quotients =
{qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
- equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
+ equiv_rel = @{term "op ="}, equiv_thm = @{thm refl}}
val qty_full_name = @{type_name "set"}
fun qinfo phi = Quotient_Info.transform_quotients phi quotients
@@ -37,7 +37,7 @@
text {* Now, we can employ quotient_definition to lift definitions. *}
quotient_definition empty where "empty :: 'a set"
-is "bot :: 'a \<Rightarrow> bool"
+is "bot :: 'a \<Rightarrow> bool" done
term "Lift_Set.empty"
thm Lift_Set.empty_def
@@ -46,7 +46,7 @@
"insertp x P y \<longleftrightarrow> y = x \<or> P y"
quotient_definition insert where "insert :: 'a => 'a set => 'a set"
-is insertp
+is insertp done
term "Lift_Set.insert"
thm Lift_Set.insert_def
--- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 14:17:29 2012 +0100
@@ -21,75 +21,50 @@
subsection {* Operations *}
-lemma [quot_respect]:
- "(op = ===> set_eq ===> op =) (op \<in>) (op \<in>)"
- "(op = ===> set_eq) Collect Collect"
- "(set_eq ===> op =) Set.is_empty Set.is_empty"
- "(op = ===> set_eq ===> set_eq) Set.insert Set.insert"
- "(op = ===> set_eq ===> set_eq) Set.remove Set.remove"
- "(op = ===> set_eq ===> set_eq) image image"
- "(op = ===> set_eq ===> set_eq) Set.project Set.project"
- "(set_eq ===> op =) Ball Ball"
- "(set_eq ===> op =) Bex Bex"
- "(set_eq ===> op =) Finite_Set.card Finite_Set.card"
- "(set_eq ===> set_eq ===> op =) (op \<subseteq>) (op \<subseteq>)"
- "(set_eq ===> set_eq ===> op =) (op \<subset>) (op \<subset>)"
- "(set_eq ===> set_eq ===> set_eq) (op \<inter>) (op \<inter>)"
- "(set_eq ===> set_eq ===> set_eq) (op \<union>) (op \<union>)"
- "set_eq {} {}"
- "set_eq UNIV UNIV"
- "(set_eq ===> set_eq) uminus uminus"
- "(set_eq ===> set_eq ===> set_eq) minus minus"
- "(set_eq ===> op =) Inf Inf"
- "(set_eq ===> op =) Sup Sup"
- "(op = ===> set_eq) List.set List.set"
- "(set_eq ===> (op = ===> set_eq) ===> set_eq) UNION UNION"
-by (auto simp: fun_rel_eq)
-
quotient_definition "member :: 'a => 'a Quotient_Cset.set => bool"
-is "op \<in>"
+is "op \<in>" by simp
quotient_definition "Set :: ('a => bool) => 'a Quotient_Cset.set"
-is Collect
+is Collect done
quotient_definition is_empty where "is_empty :: 'a Quotient_Cset.set \<Rightarrow> bool"
-is Set.is_empty
+is Set.is_empty by simp
quotient_definition insert where "insert :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.insert
+is Set.insert by simp
quotient_definition remove where "remove :: 'a \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.remove
+is Set.remove by simp
quotient_definition map where "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'b Quotient_Cset.set"
-is image
+is image by simp
quotient_definition filter where "filter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is Set.project
+is Set.project by simp
quotient_definition "forall :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Ball
+is Ball by simp
quotient_definition "exists :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-is Bex
+is Bex by simp
quotient_definition card where "card :: 'a Quotient_Cset.set \<Rightarrow> nat"
-is Finite_Set.card
+is Finite_Set.card by simp
quotient_definition set where "set :: 'a list => 'a Quotient_Cset.set"
-is List.set
+is List.set done
quotient_definition subset where "subset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+is "op \<subseteq> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
quotient_definition psubset where "psubset :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> bool"
-is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+is "op \<subset> :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool" by simp
quotient_definition inter where "inter :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "op \<inter> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
quotient_definition union where "union :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "op \<union> :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
quotient_definition empty where "empty :: 'a Quotient_Cset.set"
-is "{} :: 'a set"
+is "{} :: 'a set" done
quotient_definition UNIV where "UNIV :: 'a Quotient_Cset.set"
-is "Set.UNIV :: 'a set"
+is "Set.UNIV :: 'a set" done
quotient_definition uminus where "uminus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set"
+is "uminus_class.uminus :: 'a set \<Rightarrow> 'a set" by simp
quotient_definition minus where "minus :: 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set \<Rightarrow> 'a Quotient_Cset.set"
-is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+is "(op -) :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" by simp
quotient_definition Inf where "Inf :: ('a :: Inf) Quotient_Cset.set \<Rightarrow> 'a"
-is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a"
+is "Inf_class.Inf :: ('a :: Inf) set \<Rightarrow> 'a" by simp
quotient_definition Sup where "Sup :: ('a :: Sup) Quotient_Cset.set \<Rightarrow> 'a"
-is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a"
+is "Sup_class.Sup :: ('a :: Sup) set \<Rightarrow> 'a" by simp
quotient_definition UNION where "UNION :: 'a Quotient_Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Quotient_Cset.set) \<Rightarrow> 'b Quotient_Cset.set"
-is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+is "Complete_Lattices.UNION :: 'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" by simp
hide_const (open) is_empty insert remove map filter forall exists card
set subset psubset inter union empty UNIV uminus minus Inf Sup UNION
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 14:17:29 2012 +0100
@@ -22,10 +22,10 @@
begin
quotient_definition
- "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+ "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)" done
quotient_definition
- "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+ "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)" done
fun
plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -33,7 +33,7 @@
"plus_int_raw (x, y) (u, v) = (x + u, y + v)"
quotient_definition
- "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+ "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw" by auto
fun
uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
@@ -41,7 +41,7 @@
"uminus_int_raw (x, y) = (y, x)"
quotient_definition
- "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+ "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw" by auto
definition
minus_int_def: "z - w = z + (-w\<Colon>int)"
@@ -51,8 +51,38 @@
where
"times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+lemma times_int_raw_fst:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw x y \<approx> times_int_raw z y"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+done
+
+lemma times_int_raw_snd:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw y x \<approx> times_int_raw y z"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+done
+
quotient_definition
"(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+ apply(rule equivp_transp[OF int_equivp])
+ apply(rule times_int_raw_fst)
+ apply(assumption)
+ apply(rule times_int_raw_snd)
+ apply(assumption)
+done
fun
le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
@@ -60,7 +90,7 @@
"le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw" by auto
definition
less_int_def: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -75,47 +105,6 @@
end
-lemma [quot_respect]:
- 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 intro!: fun_relI)
-
-lemma times_int_raw_fst:
- assumes a: "x \<approx> z"
- shows "times_int_raw x y \<approx> times_int_raw z y"
- using a
- apply(cases x, cases y, cases z)
- apply(auto simp add: times_int_raw.simps intrel.simps)
- apply(rename_tac u v w x y z)
- apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
- apply(simp add: add_mult_distrib [symmetric])
- done
-
-lemma times_int_raw_snd:
- assumes a: "x \<approx> z"
- shows "times_int_raw y x \<approx> times_int_raw y z"
- using a
- apply(cases x, cases y, cases z)
- apply(auto simp add: times_int_raw.simps intrel.simps)
- apply(rename_tac u v w x y z)
- apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
- apply(simp add: mult_ac)
- apply(simp add: add_mult_distrib [symmetric])
- done
-
-lemma [quot_respect]:
- shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
- apply(simp only: fun_rel_def)
- apply(rule allI | rule impI)+
- apply(rule equivp_transp[OF int_equivp])
- apply(rule times_int_raw_fst)
- apply(assumption)
- apply(rule times_int_raw_snd)
- apply(assumption)
- done
-
text{* The integers form a @{text comm_ring_1}*}
@@ -165,11 +154,7 @@
"int_of_nat_raw m = (m :: nat, 0 :: nat)"
quotient_definition
- "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
-
-lemma[quot_respect]:
- shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
- by (auto simp add: equivp_reflp [OF int_equivp])
+ "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw" done
lemma int_of_nat:
shows "of_nat m = int_of_nat m"
@@ -304,11 +289,7 @@
quotient_definition
"int_to_nat::int \<Rightarrow> nat"
is
- "int_to_nat_raw"
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
- by (auto iff: int_to_nat_raw_def)
+ "int_to_nat_raw" unfolding int_to_nat_raw_def by force
lemma nat_le_eq_zle:
fixes w z::"int"
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 14:17:29 2012 +0100
@@ -136,29 +136,25 @@
"Nonce :: nat \<Rightarrow> msg"
is
"NONCE"
+done
quotient_definition
"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
is
"MPAIR"
+by (rule MPAIR)
quotient_definition
"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
is
"CRYPT"
+by (rule CRYPT)
quotient_definition
"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
is
"DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
-by (auto intro: DECRYPT)
+by (rule DECRYPT)
text{*Establishing these two equations is the point of the whole exercise*}
theorem CD_eq [simp]:
@@ -175,25 +171,14 @@
"nonces:: msg \<Rightarrow> nat set"
is
"freenonces"
+by (rule msgrel_imp_eq_freenonces)
text{*Now prove the four equations for @{term nonces}*}
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freenonces freenonces"
- by (auto simp add: msgrel_imp_eq_freenonces)
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim>) NONCE NONCE"
- by (auto simp add: NONCE)
-
lemma nonces_Nonce [simp]:
shows "nonces (Nonce N) = {N}"
by (lifting freenonces.simps(1))
-lemma [quot_respect]:
- shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
- by (auto simp add: MPAIR)
-
lemma nonces_MPair [simp]:
shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
by (lifting freenonces.simps(2))
@@ -212,10 +197,7 @@
"left:: msg \<Rightarrow> msg"
is
"freeleft"
-
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
- by (auto simp add: msgrel_imp_eqv_freeleft)
+by (rule msgrel_imp_eqv_freeleft)
lemma left_Nonce [simp]:
shows "left (Nonce N) = Nonce N"
@@ -239,13 +221,10 @@
"right:: msg \<Rightarrow> msg"
is
"freeright"
+by (rule msgrel_imp_eqv_freeright)
text{*Now prove the four equations for @{term right}*}
-lemma [quot_respect]:
- shows "(op \<sim> ===> op \<sim>) freeright freeright"
- by (auto simp add: msgrel_imp_eqv_freeright)
-
lemma right_Nonce [simp]:
shows "right (Nonce N) = Nonce N"
by (lifting freeright.simps(1))
@@ -352,13 +331,10 @@
"discrim:: msg \<Rightarrow> int"
is
"freediscrim"
+by (rule msgrel_imp_eq_freediscrim)
text{*Now prove the four equations for @{term discrim}*}
-lemma [quot_respect]:
- shows "(op \<sim> ===> op =) freediscrim freediscrim"
- by (auto simp add: msgrel_imp_eq_freediscrim)
-
lemma discrim_Nonce [simp]:
shows "discrim (Nonce N) = 0"
by (lifting freediscrim.simps(1))
--- a/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 14:03:58 2012 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 14:17:29 2012 +0100
@@ -32,28 +32,29 @@
begin
quotient_definition
- "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)"
+ "0 \<Colon> rat" is "(0\<Colon>int, 1\<Colon>int)" by simp
quotient_definition
- "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)"
+ "1 \<Colon> rat" is "(1\<Colon>int, 1\<Colon>int)" by simp
fun times_rat_raw where
"times_rat_raw (a :: int, b :: int) (c, d) = (a * c, b * d)"
quotient_definition
- "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw
+ "(op *) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is times_rat_raw by (auto simp add: mult_assoc mult_left_commute)
fun plus_rat_raw where
"plus_rat_raw (a :: int, b :: int) (c, d) = (a * d + c * b, b * d)"
quotient_definition
- "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
+ "(op +) :: (rat \<Rightarrow> rat \<Rightarrow> rat)" is plus_rat_raw
+ by (auto simp add: mult_commute mult_left_commute int_distrib(2))
fun uminus_rat_raw where
"uminus_rat_raw (a :: int, b :: int) = (-a, b)"
quotient_definition
- "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw"
+ "(uminus \<Colon> (rat \<Rightarrow> rat))" is "uminus_rat_raw" by fastforce
definition
minus_rat_def: "a - b = a + (-b\<Colon>rat)"
@@ -63,6 +64,32 @@
quotient_definition
"(op \<le>) :: rat \<Rightarrow> rat \<Rightarrow> bool" is "le_rat_raw"
+proof -
+ {
+ fix a b c d e f g h :: int
+ assume "a * f * (b * f) \<le> e * b * (b * f)"
+ then have le: "a * f * b * f \<le> e * b * b * f" by simp
+ assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
+ then have b2: "b * b > 0"
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ have f2: "f * f > 0" using nz(3)
+ by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
+ assume eq: "a * d = c * b" "e * h = g * f"
+ have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
+ by (metis (no_types) mult_assoc mult_commute)
+ then have "c * f * f * d \<le> e * f * d * d" using b2
+ by (metis leD linorder_le_less_linear mult_strict_right_mono)
+ then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
+ by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
+ then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
+ by (metis (no_types) mult_assoc mult_commute)
+ then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
+ by (metis leD linorder_le_less_linear mult_strict_right_mono)
+ }
+ then show "\<And>x y xa ya. x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> le_rat_raw x xa = le_rat_raw y ya" by auto
+qed
definition
less_rat_def: "(z\<Colon>rat) < w = (z \<le> w \<and> z \<noteq> w)"
@@ -83,14 +110,7 @@
where [simp]: "Fract_raw a b = (if b = 0 then (0, 1) else (a, b))"
quotient_definition "Fract :: int \<Rightarrow> int \<Rightarrow> rat" is
- Fract_raw
-
-lemma [quot_respect]:
- "(op \<approx> ===> op \<approx> ===> op \<approx>) times_rat_raw times_rat_raw"
- "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_rat_raw plus_rat_raw"
- "(op \<approx> ===> op \<approx>) uminus_rat_raw uminus_rat_raw"
- "(op = ===> op = ===> op \<approx>) Fract_raw Fract_raw"
- by (auto intro!: fun_relI simp add: mult_assoc mult_commute mult_left_commute int_distrib(2))
+ Fract_raw by simp
lemmas [simp] = Respects_def
@@ -156,15 +176,11 @@
"rat_inverse_raw (a :: int, b :: int) = (if a = 0 then (0, 1) else (b, a))"
quotient_definition
- "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw
+ "inverse :: rat \<Rightarrow> rat" is rat_inverse_raw by (force simp add: mult_commute)
definition
divide_rat_def: "q / r = q * inverse (r::rat)"
-lemma [quot_respect]:
- "(op \<approx> ===> op \<approx>) rat_inverse_raw rat_inverse_raw"
- by (auto intro!: fun_relI simp add: mult_commute)
-
instance proof
fix q :: rat
assume "q \<noteq> 0"
@@ -179,34 +195,6 @@
end
-lemma [quot_respect]: "(op \<approx> ===> op \<approx> ===> op =) le_rat_raw le_rat_raw"
-proof -
- {
- fix a b c d e f g h :: int
- assume "a * f * (b * f) \<le> e * b * (b * f)"
- then have le: "a * f * b * f \<le> e * b * b * f" by simp
- assume nz: "b \<noteq> 0" "d \<noteq> 0" "f \<noteq> 0" "h \<noteq> 0"
- then have b2: "b * b > 0"
- by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
- have f2: "f * f > 0" using nz(3)
- by (metis linorder_neqE_linordered_idom mult_eq_0_iff not_square_less_zero)
- assume eq: "a * d = c * b" "e * h = g * f"
- have "a * f * b * f * d * d \<le> e * b * b * f * d * d" using le nz(2)
- by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
- then have "c * f * f * d * (b * b) \<le> e * f * d * d * (b * b)" using eq
- by (metis (no_types) mult_assoc mult_commute)
- then have "c * f * f * d \<le> e * f * d * d" using b2
- by (metis leD linorder_le_less_linear mult_strict_right_mono)
- then have "c * f * f * d * h * h \<le> e * f * d * d * h * h" using nz(4)
- by (metis linorder_le_cases mult_right_mono mult_right_mono_neg)
- then have "c * h * (d * h) * (f * f) \<le> g * d * (d * h) * (f * f)" using eq
- by (metis (no_types) mult_assoc mult_commute)
- then have "c * h * (d * h) \<le> g * d * (d * h)" using f2
- by (metis leD linorder_le_less_linear mult_strict_right_mono)
- }
- then show ?thesis by (auto intro!: fun_relI)
-qed
-
instantiation rat :: linorder
begin