--- a/etc/isar-keywords.el Fri Mar 23 16:16:15 2012 +0000
+++ b/etc/isar-keywords.el Fri Mar 23 16:16:35 2012 +0000
@@ -221,6 +221,7 @@
"sect"
"section"
"setup"
+ "setup_lifting"
"show"
"simproc_setup"
"sledgehammer"
@@ -518,13 +519,13 @@
"print_translation"
"quickcheck_generator"
"quickcheck_params"
- "quotient_definition"
"realizability"
"realizers"
"recdef"
"record"
"refute_params"
"setup"
+ "setup_lifting"
"simproc_setup"
"sledgehammer_params"
"spark_end"
@@ -563,6 +564,7 @@
"nominal_inductive2"
"nominal_primrec"
"pcpodef"
+ "quotient_definition"
"quotient_type"
"recdef_tc"
"rep_datatype"
--- a/src/HOL/Library/Quotient_List.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Library/Quotient_List.thy Fri Mar 23 16:16:35 2012 +0000
@@ -8,8 +8,6 @@
imports Main Quotient_Syntax
begin
-declare [[map list = list_all2]]
-
lemma map_id [id_simps]:
"map id = id"
by (fact List.map.id)
@@ -75,6 +73,8 @@
by (induct xs ys rule: list_induct2') auto
qed
+declare [[map list = (list_all2, list_quotient)]]
+
lemma cons_prs [quot_preserve]:
assumes q: "Quotient R Abs Rep"
shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
--- a/src/HOL/Library/Quotient_Option.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Library/Quotient_Option.thy Fri Mar 23 16:16:35 2012 +0000
@@ -16,8 +16,6 @@
| "option_rel R None (Some x) = False"
| "option_rel R (Some x) (Some y) = R x y"
-declare [[map option = option_rel]]
-
lemma option_rel_unfold:
"option_rel R x y = (case (x, y) of (None, None) \<Rightarrow> True
| (Some x, Some y) \<Rightarrow> R x y
@@ -65,6 +63,8 @@
apply (simp add: option_rel_unfold split: option.split)
done
+declare [[map option = (option_rel, option_quotient)]]
+
lemma option_None_rsp [quot_respect]:
assumes q: "Quotient R Abs Rep"
shows "option_rel R None None"
--- a/src/HOL/Library/Quotient_Product.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Library/Quotient_Product.thy Fri Mar 23 16:16:35 2012 +0000
@@ -13,8 +13,6 @@
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-declare [[map prod = 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)
@@ -45,6 +43,8 @@
apply (auto simp add: split_paired_all)
done
+declare [[map prod = (prod_rel, prod_quotient)]]
+
lemma Pair_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
--- a/src/HOL/Library/Quotient_Set.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Library/Quotient_Set.thy Fri Mar 23 16:16:35 2012 +0000
@@ -26,6 +26,8 @@
by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
qed
+declare [[map set = (set_rel, set_quotient)]]
+
lemma empty_set_rsp[quot_respect]:
"set_rel R {} {}"
unfolding set_rel_def by simp
--- a/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Library/Quotient_Sum.thy Fri Mar 23 16:16:35 2012 +0000
@@ -16,8 +16,6 @@
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-declare [[map sum = sum_rel]]
-
lemma sum_rel_unfold:
"sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
| (Inr x, Inr y) \<Rightarrow> R2 x y
@@ -67,6 +65,8 @@
apply (simp add: sum_rel_unfold comp_def split: sum.split)
done
+declare [[map sum = (sum_rel, sum_quotient)]]
+
lemma sum_Inl_rsp [quot_respect]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Quotient.thy Fri Mar 23 16:16:35 2012 +0000
@@ -9,7 +9,8 @@
keywords
"print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
"quotient_type" :: thy_goal and "/" and
- "quotient_definition" :: thy_decl
+ "setup_lifting" :: thy_decl and
+ "quotient_definition" :: thy_goal
uses
("Tools/Quotient/quotient_info.ML")
("Tools/Quotient/quotient_type.ML")
@@ -79,6 +80,10 @@
shows "((op =) ===> (op =)) = (op =)"
by (auto simp add: fun_eq_iff elim: fun_relE)
+lemma fun_rel_eq_rel:
+ shows "((op =) ===> R) = (\<lambda>f g. \<forall>x. R (f x) (g x))"
+ by (simp add: fun_rel_def)
+
subsection {* set map (vimage) and set relation *}
definition "set_rel R xs ys \<equiv> \<forall>x y. R x y \<longrightarrow> x \<in> xs \<longleftrightarrow> y \<in> ys"
@@ -133,6 +138,18 @@
unfolding Quotient_def
by blast
+lemma Quotient_refl1:
+ assumes a: "Quotient R Abs Rep"
+ shows "R r s \<Longrightarrow> R r r"
+ using a unfolding Quotient_def
+ by fast
+
+lemma Quotient_refl2:
+ assumes a: "Quotient R Abs Rep"
+ shows "R r s \<Longrightarrow> R s s"
+ using a unfolding Quotient_def
+ by fast
+
lemma Quotient_rel_rep:
assumes a: "Quotient R Abs Rep"
shows "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
@@ -259,6 +276,15 @@
shows "R2 (f x) (g y)"
using a by (auto elim: fun_relE)
+lemma apply_rsp'':
+ assumes "Quotient R Abs Rep"
+ and "(R ===> S) f f"
+ shows "S (f (Rep x)) (f (Rep x))"
+proof -
+ from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp)
+ then show ?thesis using assms(2) by (auto intro: apply_rsp')
+qed
+
subsection {* lemmas for regularisation of ball and bex *}
lemma ball_reg_eqv:
@@ -675,6 +701,153 @@
end
+subsection {* Quotient composition *}
+
+lemma OOO_quotient:
+ fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+ fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+ fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
+ assumes R1: "Quotient R1 Abs1 Rep1"
+ assumes R2: "Quotient R2 Abs2 Rep2"
+ assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
+ assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
+ shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+apply (rule QuotientI)
+ apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
+ apply simp
+ apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+ apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+ apply (rule Quotient_rep_reflp [OF R1])
+ apply (rule Rep1)
+ apply (rule Quotient_rep_reflp [OF R2])
+ apply safe
+ apply (rename_tac x y)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_refl1 [OF R2], drule Rep1)
+ apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
+ apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
+ apply (erule pred_compI)
+ apply (erule Quotient_symp [OF R1, THEN sympD])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl1 [OF R1])
+ apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+ apply (subst Quotient_abs_rep [OF R1])
+ apply (erule Quotient_rel_abs [OF R1])
+ apply (rename_tac x y)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_refl2 [OF R2], drule Rep1)
+ apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
+ apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
+ apply (erule pred_compI)
+ apply (erule Quotient_symp [OF R1, THEN sympD])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl2 [OF R1])
+ apply (rule conjI, rule Quotient_rep_reflp [OF R1])
+ apply (subst Quotient_abs_rep [OF R1])
+ apply (erule Quotient_rel_abs [OF R1, THEN sym])
+ apply simp
+ apply (rule Quotient_rel_abs [OF R2])
+ apply (rule Quotient_rel_abs [OF R1, THEN ssubst], assumption)
+ apply (rule Quotient_rel_abs [OF R1, THEN subst], assumption)
+ apply (erule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (rename_tac a b c d)
+ apply simp
+ apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (rule conjI, erule Quotient_refl1 [OF R1])
+ apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+ apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
+ apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
+ apply (erule Quotient_refl2 [OF R1])
+ apply (rule Rep1)
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Abs1)
+ apply (erule Quotient_refl2 [OF R1])
+ apply (erule Quotient_refl1 [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply (drule Quotient_rel_abs [OF R1])
+ apply simp
+ apply (rule Quotient_rel[symmetric, OF R2, THEN iffD2])
+ apply simp
+done
+
+lemma OOO_eq_quotient:
+ fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
+ fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
+ assumes R1: "Quotient R1 Abs1 Rep1"
+ assumes R2: "Quotient op= Abs2 Rep2"
+ shows "Quotient (R1 OOO op=) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
+using assms
+by (rule OOO_quotient) auto
+
+subsection {* Invariant *}
+
+definition invariant :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ where "invariant R = (\<lambda>x y. R x \<and> x = y)"
+
+lemma invariant_to_eq:
+ assumes "invariant P x y"
+ shows "x = y"
+using assms by (simp add: invariant_def)
+
+lemma fun_rel_eq_invariant:
+ shows "((invariant R) ===> S) = (\<lambda>f g. \<forall>x. R x \<longrightarrow> S (f x) (g x))"
+by (auto simp add: invariant_def fun_rel_def)
+
+lemma invariant_same_args:
+ shows "invariant P x x \<equiv> P x"
+using assms by (auto simp add: invariant_def)
+
+lemma copy_type_to_Quotient:
+ assumes "type_definition Rep Abs UNIV"
+ shows "Quotient (op =) Abs Rep"
+proof -
+ interpret type_definition Rep Abs UNIV by fact
+ from Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI)
+qed
+
+lemma copy_type_to_equivp:
+ fixes Abs :: "'a \<Rightarrow> 'b"
+ and Rep :: "'b \<Rightarrow> 'a"
+ assumes "type_definition Rep Abs (UNIV::'a set)"
+ shows "equivp (op=::'a\<Rightarrow>'a\<Rightarrow>bool)"
+by (rule identity_equivp)
+
+lemma invariant_type_to_Quotient:
+ assumes "type_definition Rep Abs {x. P x}"
+ shows "Quotient (invariant P) Abs Rep"
+proof -
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: QuotientI simp: invariant_def)
+qed
+
+lemma invariant_type_to_part_equivp:
+ assumes "type_definition Rep Abs {x. P x}"
+ shows "part_equivp (invariant P)"
+proof (intro part_equivpI)
+ interpret type_definition Rep Abs "{x. P x}" by fact
+ show "\<exists>x. invariant P x x" using Rep by (auto simp: invariant_def)
+next
+ show "symp (invariant P)" by (auto intro: sympI simp: invariant_def)
+next
+ show "transp (invariant P)" by (auto intro: transpI simp: invariant_def)
+qed
+
subsection {* ML setup *}
text {* Auxiliary data for the quotient package *}
@@ -682,8 +855,7 @@
use "Tools/Quotient/quotient_info.ML"
setup Quotient_Info.setup
-declare [[map "fun" = fun_rel]]
-declare [[map set = set_rel]]
+declare [[map "fun" = (fun_rel, fun_quotient)]]
lemmas [quot_thm] = fun_quotient
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
--- a/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/DList.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/FSet.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Lift_Fun.thy Fri Mar 23 16:16:35 2012 +0000
@@ -6,7 +6,7 @@
theory Lift_Fun
-imports Main
+imports Main "~~/src/HOL/Library/Quotient_Syntax"
begin
text {* This file is meant as a test case for features introduced in the changeset 2d8949268303.
@@ -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,45 @@
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)"
+text {* Relator for 'a endofun. *}
+
+definition
+ endofun_rel' :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> bool"
+where
+ "endofun_rel' R = (\<lambda>f g. (R ===> R) f g)"
+
+quotient_definition "endofun_rel :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a endofun \<Rightarrow> 'b endofun \<Rightarrow> bool" is
+ endofun_rel' done
+
+lemma endofun_quotient:
+assumes a: "Quotient R Abs Rep"
+shows "Quotient (endofun_rel R) (map_endofun Abs Rep) (map_endofun Rep Abs)"
+proof (intro QuotientI)
+ show "\<And>a. map_endofun Abs Rep (map_endofun Rep Abs a) = a"
+ by (metis (hide_lams, no_types) a abs_o_rep id_apply map_endofun.comp map_endofun.id o_eq_dest_lhs)
+next
+ show "\<And>a. endofun_rel R (map_endofun Rep Abs a) (map_endofun Rep Abs a)"
+ using fun_quotient[OF a a, THEN Quotient_rep_reflp]
+ unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def
+ by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
+next
+ show "\<And>r s. endofun_rel R r s =
+ (endofun_rel R r r \<and>
+ endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
+ apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
+ using fun_quotient[OF a a,THEN Quotient_refl1]
+ apply metis
+ using fun_quotient[OF a a,THEN Quotient_refl2]
+ apply metis
+ using fun_quotient[OF a a, THEN Quotient_rel]
+ apply metis
+ using fun_quotient[OF a a, THEN Quotient_rel]
+ by (smt Quotient_endofun rep_abs_rsp)
+qed
+
+declare [[map endofun = (endofun_rel, endofun_quotient)]]
+
+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 +111,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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Lift_RBT.thy Fri Mar 23 16:16:35 2012 +0000
@@ -15,21 +15,6 @@
then show ?thesis ..
qed
-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}}
- val qty_full_name = @{type_name "rbt"}
-
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- in lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
- #> Quotient_Info.update_abs_rep qty_full_name (Quotient_Info.transform_abs_rep phi
- {abs = @{term "RBT"}, rep = @{term "impl_of"}}))
- end
-*}
-
lemma rbt_eq_iff:
"t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
by (simp add: impl_of_inject)
@@ -46,12 +31,12 @@
"RBT (impl_of t) = t"
by (simp add: impl_of_inverse)
-
subsection {* Primitive operations *}
-quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+setup_lifting type_definition_rbt
-declare lookup_def[unfolded map_fun_def comp_def id_def, code]
+quotient_definition lookup where "lookup :: ('a\<Colon>linorder, 'b) rbt \<Rightarrow> 'a \<rightharpoonup> 'b" is "RBT_Impl.lookup"
+by simp
(* FIXME: quotient_definition at the moment requires that types variables match exactly,
i.e., sort constraints must be annotated to the constant being lifted.
@@ -67,65 +52,38 @@
*)
quotient_definition empty where "empty :: ('a\<Colon>linorder, 'b) rbt"
-is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)"
-
-lemma impl_of_empty [code abstract]:
- "impl_of empty = RBT_Impl.Empty"
- by (simp add: empty_def RBT_inverse)
+is "(RBT_Impl.Empty :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt)" by (simp add: empty_def)
quotient_definition insert where "insert :: 'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.insert"
-
-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)
+is "RBT_Impl.insert" by simp
quotient_definition delete where "delete :: 'a\<Colon>linorder \<Rightarrow> ('a, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.delete"
-
-lemma impl_of_delete [code abstract]:
- "impl_of (delete k t) = RBT_Impl.delete k (impl_of t)"
- by (simp add: delete_def RBT_inverse)
+is "RBT_Impl.delete" by simp
(* 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"
-
-lemma [code]: "entries t = RBT_Impl.entries (impl_of t)"
-unfolding entries_def map_fun_def comp_def id_def ..
+is "RBT_Impl.entries :: ('a\<Colon>linorder, 'b) RBT_Impl.rbt \<Rightarrow> ('a \<times> 'b) list" by simp
(* 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" by simp
quotient_definition "bulkload :: ('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.bulkload"
-
-lemma impl_of_bulkload [code abstract]:
- "impl_of (bulkload xs) = RBT_Impl.bulkload xs"
- by (simp add: bulkload_def RBT_inverse)
+is "RBT_Impl.bulkload" by simp
quotient_definition "map_entry :: 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) rbt \<Rightarrow> ('a, 'b) rbt"
-is "RBT_Impl.map_entry"
-
-lemma impl_of_map_entry [code abstract]:
- "impl_of (map_entry k f t) = RBT_Impl.map_entry k f (impl_of t)"
- by (simp add: map_entry_def RBT_inverse)
+is "RBT_Impl.map_entry" by simp
(* 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"
-
-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)
+by simp
(* 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" by simp
-lemma [code]: "fold f t = RBT_Impl.fold f (impl_of t)"
-unfolding fold_def map_fun_def comp_def id_def ..
-
+export_code lookup empty insert delete entries keys bulkload map_entry map fold in SML
subsection {* Derived operations *}
@@ -189,6 +147,10 @@
"fold f t = List.fold (prod_case f) (entries t)"
by (simp add: fold_def fun_eq_iff RBT_Impl.fold_def entries_impl_of)
+lemma impl_of_empty:
+ "impl_of empty = RBT_Impl.Empty"
+ by (simp add: empty_def RBT_inverse)
+
lemma is_empty_empty [simp]:
"is_empty t \<longleftrightarrow> t = empty"
by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
@@ -210,5 +172,4 @@
by (simp add: keys_def RBT_Impl.keys_def distinct_entries)
-
end
\ No newline at end of file
--- a/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy Fri Mar 23 16:16:35 2012 +0000
@@ -14,30 +14,12 @@
morphisms member Set
unfolding set_def by auto
-text {* Here is some ML setup that should eventually be incorporated in the typedef command. *}
-
-local_setup {* fn lthy =>
- let
- val quotients =
- {qtyp = @{typ "'a set"}, rtyp = @{typ "'a => bool"},
- equiv_rel = @{term "dummy"}, equiv_thm = @{thm refl}}
- val qty_full_name = @{type_name "set"}
-
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- in
- lthy
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi =>
- Quotient_Info.update_quotients qty_full_name (qinfo phi) #>
- Quotient_Info.update_abs_rep qty_full_name
- (Quotient_Info.transform_abs_rep phi {abs = @{term "Set"}, rep = @{term "member"}}))
- end
-*}
+setup_lifting type_definition_set[unfolded set_def]
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,10 +28,12 @@
"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
+export_code empty insert in SML
+
end
--- a/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Cset.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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 16:16:15 2012 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Rat.thy Fri Mar 23 16:16:35 2012 +0000
@@ -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
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 23 16:16:35 2012 +0000
@@ -6,13 +6,17 @@
signature QUOTIENT_DEF =
sig
+ val add_quotient_def:
+ ((binding * mixfix) * Attrib.binding) * (term * term) -> thm ->
+ local_theory -> Quotient_Info.quotconsts * local_theory
+
val quotient_def:
(binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
- local_theory -> Quotient_Info.quotconsts * local_theory
+ local_theory -> Proof.state
val quotient_def_cmd:
(binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
- local_theory -> Quotient_Info.quotconsts * local_theory
+ local_theory -> Proof.state
val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
Quotient_Info.quotconsts * local_theory
@@ -23,6 +27,130 @@
(** Interface and Syntax Setup **)
+(* Generation of the code certificate from the rsp theorem *)
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+fun get_body_types (Type ("fun", [_, U]), Type ("fun", [_, V])) = get_body_types (U, V)
+ | get_body_types (U, V) = (U, V)
+
+fun get_binder_types (Type ("fun", [T, U]), Type ("fun", [V, W])) = (T, V) :: get_binder_types (U, W)
+ | get_binder_types _ = []
+
+fun unabs_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ fun dest_abs (Abs (var_name, T, _)) = (var_name, T)
+ | dest_abs tm = raise TERM("get_abs_var",[tm])
+ val (var_name, T) = dest_abs (term_of rhs)
+ val (new_var_names, ctxt') = Variable.variant_fixes [var_name] ctxt
+ val thy = Proof_Context.theory_of ctxt'
+ val refl_thm = Thm.reflexive (cterm_of thy (Free (hd new_var_names, T)))
+ in
+ Thm.combination def refl_thm |>
+ singleton (Proof_Context.export ctxt' ctxt)
+ end
+
+fun unabs_all_def ctxt def =
+ let
+ val (_, rhs) = Thm.dest_equals (cprop_of def)
+ val xs = strip_abs_vars (term_of rhs)
+ in
+ fold (K (unabs_def ctxt)) xs def
+ end
+
+val map_fun_unfolded =
+ @{thm map_fun_def[abs_def]} |>
+ unabs_def @{context} |>
+ unabs_def @{context} |>
+ Local_Defs.unfold @{context} [@{thm comp_def}]
+
+fun unfold_fun_maps ctm =
+ let
+ fun unfold_conv ctm =
+ case (Thm.term_of ctm) of
+ Const (@{const_name "map_fun"}, _) $ _ $ _ =>
+ (Conv.arg_conv unfold_conv then_conv Conv.rewr_conv map_fun_unfolded) ctm
+ | _ => Conv.all_conv ctm
+ val try_beta_conv = Conv.try_conv (Thm.beta_conversion false)
+ in
+ (Conv.arg_conv (Conv.fun_conv unfold_conv then_conv try_beta_conv)) ctm
+ end
+
+fun prove_rel ctxt rsp_thm (rty, qty) =
+ let
+ val ty_args = get_binder_types (rty, qty)
+ fun disch_arg args_ty thm =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem ctxt args_ty
+ in
+ [quot_thm, thm] MRSL @{thm apply_rsp''}
+ end
+ in
+ fold disch_arg ty_args rsp_thm
+ end
+
+exception CODE_CERT_GEN of string
+
+fun simplify_code_eq ctxt def_thm =
+ Local_Defs.unfold ctxt [@{thm o_def}, @{thm map_fun_def}, @{thm id_def}] def_thm
+
+fun generate_code_cert ctxt def_thm rsp_thm (rty, qty) =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem ctxt (get_body_types (rty, qty))
+ val fun_rel = prove_rel ctxt rsp_thm (rty, qty)
+ val abs_rep_thm = [quot_thm, fun_rel] MRSL @{thm Quotient_rep_abs}
+ val abs_rep_eq =
+ case (HOLogic.dest_Trueprop o prop_of) fun_rel of
+ Const (@{const_name HOL.eq}, _) $ _ $ _ => abs_rep_thm
+ | Const (@{const_name invariant}, _) $ _ $ _ $ _ => abs_rep_thm RS @{thm invariant_to_eq}
+ | _ => raise CODE_CERT_GEN "relation is neither equality nor invariant"
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val unabs_def = unabs_all_def ctxt unfolded_def
+ val rep = (snd o Thm.dest_comb o snd o Thm.dest_comb o cprop_of) quot_thm
+ val rep_refl = Thm.reflexive rep RS @{thm meta_eq_to_obj_eq}
+ val repped_eq = [rep_refl, unabs_def RS @{thm meta_eq_to_obj_eq}] MRSL @{thm cong}
+ val code_cert = [repped_eq, abs_rep_eq] MRSL @{thm trans}
+ in
+ simplify_code_eq ctxt code_cert
+ end
+
+fun define_code_cert def_thm rsp_thm (rty, qty) lthy =
+ let
+ val quot_thm = Quotient_Term.prove_quot_theorem lthy (get_body_types (rty, qty))
+ in
+ if Quotient_Type.can_generate_code_cert quot_thm then
+ let
+ val code_cert = generate_code_cert lthy def_thm rsp_thm (rty, qty)
+ val add_abs_eqn_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abs_eqn thm) I)
+ val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [add_abs_eqn_attrib]), [code_cert])
+ end
+ else
+ lthy
+ end
+
+fun define_code_eq def_thm lthy =
+ let
+ val unfolded_def = Conv.fconv_rule unfold_fun_maps def_thm
+ val code_eq = unabs_all_def lthy unfolded_def
+ val simp_code_eq = simplify_code_eq lthy code_eq
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [Code.add_default_eqn_attrib]), [simp_code_eq])
+ end
+
+fun define_code def_thm rsp_thm (rty, qty) lthy =
+ if body_type rty = body_type qty then
+ define_code_eq def_thm lthy
+ else
+ define_code_cert def_thm rsp_thm (rty, qty) lthy
+
(* The ML-interface for a quotient definition takes
as argument:
@@ -30,6 +158,7 @@
- attributes
- the new constant as term
- the rhs of the definition as term
+ - respectfulness theorem for the rhs
It stores the qconst_info in the quotconsts data slot.
@@ -45,7 +174,84 @@
quote str ^ " differs from declaration " ^ name ^ pos)
end
-fun gen_quotient_def prep_vars prep_term (raw_var, ((name, atts), (lhs_raw, rhs_raw))) lthy =
+fun add_quotient_def ((var, (name, atts)), (lhs, rhs)) rsp_thm lthy =
+ let
+ val rty = fastype_of rhs
+ val qty = fastype_of lhs
+ val absrep_trm =
+ Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (rty, qty) $ rhs
+ val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
+ val (_, prop') = Local_Defs.cert_def lthy prop
+ val (_, newrhs) = Local_Defs.abs_def prop'
+
+ val ((trm, (_ , def_thm)), lthy') =
+ Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
+
+ (* data storage *)
+ val qconst_data = {qconst = trm, rconst = rhs, def = def_thm}
+ fun get_rsp_thm_name (lhs_name, _) = Binding.suffix_name "_rsp" lhs_name
+
+ val lthy'' = lthy'
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi =>
+ (case Quotient_Info.transform_quotconsts phi qconst_data of
+ qcinfo as {qconst = Const (c, _), ...} =>
+ Quotient_Info.update_quotconsts c qcinfo
+ | _ => I))
+ |> (snd oo Local_Theory.note)
+ ((get_rsp_thm_name var, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
+ [rsp_thm])
+ |> define_code def_thm rsp_thm (rty, qty)
+
+ in
+ (qconst_data, lthy'')
+ end
+
+fun mk_readable_rsp_thm_eq tm lthy =
+ let
+ val ctm = cterm_of (Proof_Context.theory_of lthy) tm
+
+ fun norm_fun_eq ctm =
+ let
+ fun abs_conv2 cv = Conv.abs_conv (K (Conv.abs_conv (K cv) lthy)) lthy
+ fun erase_quants ctm' =
+ case (Thm.term_of ctm') of
+ Const ("HOL.eq", _) $ _ $ _ => Conv.all_conv ctm'
+ | _ => (Conv.binder_conv (K erase_quants) lthy then_conv
+ Conv.rewr_conv @{thm fun_eq_iff[symmetric, THEN eq_reflection]}) ctm'
+ in
+ (abs_conv2 erase_quants then_conv Thm.eta_conversion) ctm
+ end
+
+ fun simp_arrows_conv ctm =
+ let
+ val unfold_conv = Conv.rewrs_conv
+ [@{thm fun_rel_eq_invariant[THEN eq_reflection]}, @{thm fun_rel_eq_rel[THEN eq_reflection]},
+ @{thm fun_rel_def[THEN eq_reflection]}]
+ val left_conv = simp_arrows_conv then_conv Conv.try_conv norm_fun_eq
+ fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+ in
+ case (Thm.term_of ctm) of
+ Const (@{const_name "fun_rel"}, _) $ _ $ _ =>
+ (binop_conv2 left_conv simp_arrows_conv then_conv unfold_conv) ctm
+ | _ => Conv.all_conv ctm
+ end
+
+ val unfold_ret_val_invs = Conv.bottom_conv
+ (K (Conv.try_conv (Conv.rewr_conv @{thm invariant_same_args}))) lthy
+ val simp_conv = Conv.arg_conv (Conv.fun2_conv simp_arrows_conv)
+ val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
+ val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
+ val beta_conv = Thm.beta_conversion true
+ val eq_thm =
+ (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs) ctm
+ in
+ Object_Logic.rulify(eq_thm RS Drule.equal_elim_rule2)
+ end
+
+
+
+fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
let
val (vars, ctxt) = prep_vars (the_list raw_var) lthy
val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
@@ -63,27 +269,50 @@
if Variable.check_name binding = lhs_str then (binding, mx)
else error_msg binding lhs_str
| _ => raise Match)
-
- val absrep_trm = Quotient_Term.absrep_fun lthy Quotient_Term.AbsF (fastype_of rhs, lhs_ty) $ rhs
- val prop = Syntax.check_term lthy (Logic.mk_equals (lhs, absrep_trm))
- val (_, prop') = Local_Defs.cert_def lthy prop
- val (_, newrhs) = Local_Defs.abs_def prop'
-
- val ((trm, (_ , thm)), lthy') =
- Local_Theory.define (var, ((Thm.def_binding_optional (#1 var) name, atts), newrhs)) lthy
+
+ fun try_to_prove_refl thm =
+ let
+ val lhs_eq =
+ thm
+ |> prop_of
+ |> Logic.dest_implies
+ |> fst
+ |> strip_all_body
+ |> try HOLogic.dest_Trueprop
+ in
+ case lhs_eq of
+ SOME (Const ("HOL.eq", _) $ _ $ _) => SOME (@{thm refl} RS thm)
+ | SOME _ => (case body_type (fastype_of lhs) of
+ Type (typ_name, _) => ( SOME
+ (#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
+ RS @{thm Equiv_Relations.equivp_reflp} RS thm)
+ handle _ => NONE)
+ | _ => NONE
+ )
+ | _ => NONE
+ end
- (* data storage *)
- val qconst_data = {qconst = trm, rconst = rhs, def = thm}
+ val rsp_rel = Quotient_Term.equiv_relation lthy (fastype_of rhs, lhs_ty)
+ val internal_rsp_tm = HOLogic.mk_Trueprop (Syntax.check_term lthy (rsp_rel $ rhs $ rhs))
+ val readable_rsp_thm_eq = mk_readable_rsp_thm_eq internal_rsp_tm lthy
+ val maybe_proven_rsp_thm = try_to_prove_refl readable_rsp_thm_eq
+ val (readable_rsp_tm, _) = Logic.dest_implies (prop_of readable_rsp_thm_eq)
+
+ fun after_qed thm_list lthy =
+ let
+ val internal_rsp_thm =
+ case thm_list of
+ [] => the maybe_proven_rsp_thm
+ | [[thm]] => Goal.prove ctxt [] [] internal_rsp_tm
+ (fn _ => rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac [thm] 1)
+ in
+ snd (add_quotient_def ((var, attr), (lhs, rhs)) internal_rsp_thm lthy)
+ end
- val lthy'' = lthy'
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi =>
- (case Quotient_Info.transform_quotconsts phi qconst_data of
- qcinfo as {qconst = Const (c, _), ...} =>
- Quotient_Info.update_quotconsts c qcinfo
- | _ => I));
in
- (qconst_data, lthy'')
+ case maybe_proven_rsp_thm of
+ SOME _ => Proof.theorem NONE after_qed [] lthy
+ | NONE => Proof.theorem NONE after_qed [[(readable_rsp_tm,[])]] lthy
end
fun check_term' cnstr ctxt =
@@ -103,16 +332,19 @@
val qty = Quotient_Term.derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
- quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
+ (*quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt*)
+ ({qconst = lhs, rconst = lhs, def = @{thm refl}}, ctxt)
end
-(* command *)
+(* parser and command *)
+val quotdef_parser =
+ Scan.option Parse_Spec.constdecl --
+ Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
val _ =
- Outer_Syntax.local_theory @{command_spec "quotient_definition"}
+ Outer_Syntax.local_theory_to_proof @{command_spec "quotient_definition"}
"definition for constants over the quotient type"
- (Scan.option Parse_Spec.constdecl --
- Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
- >> (snd oo quotient_def_cmd))
+ (quotdef_parser >> quotient_def_cmd)
+
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 23 16:16:35 2012 +0000
@@ -6,7 +6,7 @@
signature QUOTIENT_INFO =
sig
- type quotmaps = {relmap: string}
+ type quotmaps = {relmap: string, quot_thm: thm}
val lookup_quotmaps: Proof.context -> string -> quotmaps option
val lookup_quotmaps_global: theory -> string -> quotmaps option
val print_quotmaps: Proof.context -> unit
@@ -18,7 +18,7 @@
val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
val print_abs_rep: Proof.context -> unit
- type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+ type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
val transform_quotients: morphism -> quotients -> quotients
val lookup_quotients: Proof.context -> string -> quotients option
val lookup_quotients_global: theory -> string -> quotients option
@@ -54,7 +54,7 @@
(* FIXME just one data slot (record) per program unit *)
(* info about map- and rel-functions for a type *)
-type quotmaps = {relmap: string}
+type quotmaps = {relmap: string, quot_thm: thm}
structure Quotmaps = Generic_Data
(
@@ -71,19 +71,24 @@
val quotmaps_attribute_setup =
Attrib.setup @{binding map}
- ((Args.type_name true --| Scan.lift (@{keyword "="})) -- Args.const_proper true >>
- (fn (tyname, relname) =>
- let val minfo = {relmap = relname}
+ ((Args.type_name true --| Scan.lift (@{keyword "="})) --
+ (Scan.lift (@{keyword "("}) |-- Args.const_proper true --| Scan.lift (@{keyword ","}) --
+ Attrib.thm --| Scan.lift (@{keyword ")"})) >>
+ (fn (tyname, (relname, qthm)) =>
+ let val minfo = {relmap = relname, quot_thm = qthm}
in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
"declaration of map information"
fun print_quotmaps ctxt =
let
- fun prt_map (ty_name, {relmap}) =
+ fun prt_map (ty_name, {relmap, quot_thm}) =
Pretty.block (separate (Pretty.brk 2)
- (map Pretty.str
- ["type:", ty_name,
- "relation map:", relmap]))
+ [Pretty.str "type:",
+ Pretty.str ty_name,
+ Pretty.str "relation map:",
+ Pretty.str relmap,
+ Pretty.str "quot. theorem:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
in
map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
|> Pretty.big_list "maps for type constructors:"
@@ -125,7 +130,7 @@
end
(* info about quotient types *)
-type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
structure Quotients = Generic_Data
(
@@ -135,11 +140,12 @@
fun merge data = Symtab.merge (K true) data
)
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
{qtyp = Morphism.typ phi qtyp,
rtyp = Morphism.typ phi rtyp,
equiv_rel = Morphism.term phi equiv_rel,
- equiv_thm = Morphism.thm phi equiv_thm}
+ equiv_thm = Morphism.thm phi equiv_thm,
+ quot_thm = Morphism.thm phi quot_thm}
val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
@@ -151,7 +157,7 @@
fun print_quotients ctxt =
let
- fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+ fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
Pretty.block (separate (Pretty.brk 2)
[Pretty.str "quotient type:",
Syntax.pretty_typ ctxt qtyp,
@@ -160,7 +166,9 @@
Pretty.str "relation:",
Syntax.pretty_term ctxt equiv_rel,
Pretty.str "equiv. thm:",
- Syntax.pretty_term ctxt (prop_of equiv_thm)])
+ Syntax.pretty_term ctxt (prop_of equiv_thm),
+ Pretty.str "quot. thm:",
+ Syntax.pretty_term ctxt (prop_of quot_thm)])
in
map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
|> Pretty.big_list "quotients:"
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Fri Mar 23 16:16:35 2012 +0000
@@ -20,6 +20,9 @@
val equiv_relation: Proof.context -> typ * typ -> term
val equiv_relation_chk: Proof.context -> typ * typ -> term
+ val get_rel_from_quot_thm: thm -> term
+ val prove_quot_theorem: Proof.context -> typ * typ -> thm
+
val regularize_trm: Proof.context -> term * term -> term
val regularize_trm_chk: Proof.context -> term * term -> term
@@ -72,9 +75,6 @@
fun defined_mapfun_data ctxt s =
Symtab.defined (Enriched_Type.entries ctxt) s
-
-(* makes a Free out of a TVar *)
-fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
(* looks up the (varified) rty and qty for
a quotient definition
@@ -279,35 +279,10 @@
SOME map_data => Const (#relmap map_data, dummyT)
| NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"))
-(* takes two type-environments and looks
- up in both of them the variable v, which
- must be listed in the environment
-*)
-fun double_lookup rtyenv qtyenv v =
- let
- val v' = fst (dest_TVar v)
- in
- (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
- end
-
-fun mk_relmap ctxt vs rty =
- let
- val vs' = map (mk_Free) vs
-
- fun mk_relmap_aux rty =
- case rty of
- TVar _ => mk_Free rty
- | Type (_, []) => HOLogic.eq_const rty
- | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
- | _ => raise LIFT_MATCH ("mk_relmap (default)")
- in
- fold_rev Term.lambda vs' (mk_relmap_aux rty)
- end
-
fun get_equiv_rel thy s =
(case Quotient_Info.lookup_quotients thy s of
SOME qdata => #equiv_rel qdata
- | NONE => raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")"))
+ | NONE => raise LIFT_MATCH ("get_equiv_rel (no quotient found for type " ^ s ^ ")"))
fun equiv_match_err ctxt ty_pat ty =
let
@@ -336,11 +311,10 @@
end
else
let
- val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
- val rtyenv = match ctxt equiv_match_err rty_pat rty
+ val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
val qtyenv = match ctxt equiv_match_err qty_pat qty
- val args_aux = map (double_lookup rtyenv qtyenv) vs
- val args = map (equiv_relation ctxt) args_aux
+ val rtys' = map (Envir.subst_type qtyenv) rtys
+ val args = map (equiv_relation ctxt) (tys ~~ rtys')
val eqv_rel = get_equiv_rel ctxt s'
val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
in
@@ -348,8 +322,7 @@
then eqv_rel'
else
let
- val rel_map = mk_relmap ctxt vs rty_pat
- val result = list_comb (rel_map, args)
+ val result = list_comb (get_relmap ctxt s, args)
in
mk_rel_compose (result, eqv_rel')
end
@@ -361,6 +334,78 @@
equiv_relation ctxt (rty, qty)
|> Syntax.check_term ctxt
+(* generation of the Quotient theorem *)
+
+fun get_quot_thm ctxt s =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ (case Quotient_Info.lookup_quotients_global thy s of
+ SOME qdata => #quot_thm qdata
+ | NONE => raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found."))
+ end
+
+fun get_rel_quot_thm thy s =
+ (case Quotient_Info.lookup_quotmaps thy s of
+ SOME map_data => #quot_thm map_data
+ | NONE => raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")"));
+
+fun is_id_quot thm = (prop_of thm = prop_of @{thm identity_quotient})
+
+infix 0 MRSL
+
+fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
+
+exception NOT_IMPL of string
+
+fun get_rel_from_quot_thm quot_thm =
+ let
+ val (_ $ rel $ _ $ _) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+ in
+ rel
+ end
+
+fun mk_quot_thm_compose (rel_quot_thm, quot_thm) =
+ let
+ val quot_thm_rel = get_rel_from_quot_thm quot_thm
+ in
+ if is_eq quot_thm_rel then [rel_quot_thm, quot_thm] MRSL @{thm OOO_eq_quotient}
+ else raise NOT_IMPL "nested quotients: not implemented yet"
+ end
+
+fun prove_quot_theorem ctxt (rty, qty) =
+ if rty = qty
+ then @{thm identity_quotient}
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then
+ let
+ val args = map (prove_quot_theorem ctxt) (tys ~~ tys')
+ in
+ args MRSL (get_rel_quot_thm ctxt s)
+ end
+ else
+ let
+ val (Type (_, rtys), qty_pat) = get_rty_qty ctxt s'
+ val qtyenv = match ctxt equiv_match_err qty_pat qty
+ val rtys' = map (Envir.subst_type qtyenv) rtys
+ val args = map (prove_quot_theorem ctxt) (tys ~~ rtys')
+ val quot_thm = get_quot_thm ctxt s'
+ in
+ if forall is_id_quot args
+ then
+ quot_thm
+ else
+ let
+ val rel_quot_thm = args MRSL (get_rel_quot_thm ctxt s)
+ in
+ mk_quot_thm_compose (rel_quot_thm, quot_thm)
+ end
+ end
+ | _ => @{thm identity_quotient}
+
(*** Regularization ***)
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 23 16:16:35 2012 +0000
@@ -6,6 +6,8 @@
signature QUOTIENT_TYPE =
sig
+ val can_generate_code_cert: thm -> bool
+
val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) *
((binding * binding) option)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
@@ -25,7 +27,7 @@
val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
-(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
+(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
fun typedef_term rel rty lthy =
let
val [x, c] =
@@ -76,6 +78,44 @@
Goal.prove lthy [] [] goal
(K (typedef_quot_type_tac equiv_thm typedef_info))
end
+
+fun can_generate_code_cert quot_thm =
+ case Quotient_Term.get_rel_from_quot_thm quot_thm of
+ Const (@{const_name HOL.eq}, _) => true
+ | Const (@{const_name invariant}, _) $ _ => true
+ | _ => false
+
+fun define_abs_type quot_thm lthy =
+ if can_generate_code_cert quot_thm then
+ let
+ val abs_type_thm = quot_thm RS @{thm Quotient_abs_rep}
+ val add_abstype_attribute =
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_abstype thm) I)
+ val add_abstype_attrib = Attrib.internal (K add_abstype_attribute);
+ in
+ lthy
+ |> (snd oo Local_Theory.note) ((Binding.empty, [add_abstype_attrib]), [abs_type_thm])
+ end
+ else
+ lthy
+
+fun init_quotient_infr quot_thm equiv_thm lthy =
+ let
+ val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
+ val (qtyp, rtyp) = (dest_funT o fastype_of) rep
+ val qty_full_name = (fst o dest_Type) qtyp
+ val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm,
+ quot_thm = quot_thm }
+ fun quot_info phi = Quotient_Info.transform_quotients phi quotients
+ val abs_rep = {abs = abs, rep = rep}
+ fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
+ in
+ lthy
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
+ #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
+ |> define_abs_type quot_thm
+ end
(* main function for constructing a quotient type *)
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), opt_morphs), equiv_thm) lthy =
@@ -86,7 +126,7 @@
else equiv_thm RS @{thm equivp_implies_part_equivp}
(* generates the typedef *)
- val ((qty_full_name, typedef_info), lthy1) =
+ val ((_, typedef_info), lthy1) =
typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
(* abs and rep functions from the typedef *)
@@ -108,9 +148,9 @@
NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
| SOME morphs => morphs)
- val ((abs_t, (_, abs_def)), lthy2) = lthy1
+ val ((_, (_, abs_def)), lthy2) = lthy1
|> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
- val ((rep_t, (_, rep_def)), lthy3) = lthy2
+ val ((_, (_, rep_def)), lthy3) = lthy2
|> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
(* quot_type theorem *)
@@ -126,15 +166,11 @@
val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
(* storing the quotients *)
- val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
-
- fun qinfo phi = Quotient_Info.transform_quotients phi quotients
- fun abs_rep phi = Quotient_Info.transform_abs_rep phi {abs = abs_t, rep = rep_t}
+ val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm,
+ quot_thm = quotient_thm}
val lthy4 = lthy3
- |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi)
- #> Quotient_Info.update_abs_rep qty_full_name (abs_rep phi))
+ |> init_quotient_infr quotient_thm equiv_thm
|> (snd oo Local_Theory.note)
((equiv_thm_name,
if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
@@ -264,15 +300,43 @@
val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
+val quotspec_parser =
+ Parse.and_list1
+ ((Parse.type_args -- Parse.binding) --
+ (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+ (@{keyword "/"} |-- (partial -- Parse.term)) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
+
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
"quotient type definitions (require equivalence proofs)"
- (Parse.and_list1
- ((Parse.type_args -- Parse.binding) --
- (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
- (@{keyword "/"} |-- (partial -- Parse.term)) --
- Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
- >> quotient_type_cmd)
+ (quotspec_parser >> quotient_type_cmd)
+
+(* Setup lifting using type_def_thm *)
+
+exception SETUP_LIFT_TYPE of string
+
+fun setup_lift_type typedef_thm =
+ let
+ val typedef_set = (snd o dest_comb o HOLogic.dest_Trueprop o prop_of) typedef_thm
+ val (quot_thm, equivp_thm) = (case typedef_set of
+ Const ("Orderings.top_class.top", _) =>
+ (typedef_thm RS @{thm copy_type_to_Quotient},
+ typedef_thm RS @{thm copy_type_to_equivp})
+ | Const (@{const_name "Collect"}, _) $ Abs (_, _, _ $ Bound 0) =>
+ (typedef_thm RS @{thm invariant_type_to_Quotient},
+ typedef_thm RS @{thm invariant_type_to_part_equivp})
+ | _ => raise SETUP_LIFT_TYPE "unsupported typedef theorem")
+ in
+ init_quotient_infr quot_thm equivp_thm
+ end
+
+fun setup_lift_type_aux xthm lthy = setup_lift_type (singleton (Attrib.eval_thms lthy) xthm) lthy
+
+val _ =
+ Outer_Syntax.local_theory @{command_spec "setup_lifting"}
+ "Setup lifting infrastracture"
+ (Parse_Spec.xthm >> (fn xthm => setup_lift_type_aux xthm))
end;
--- a/src/HOL/Unix/Unix.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/Unix/Unix.thy Fri Mar 23 16:16:35 2012 +0000
@@ -843,7 +843,9 @@
neither owned nor writable by @{term user\<^isub>1}.
*}
-definition
+
+
+definition invariant where
"invariant root path =
(\<exists>att dir.
access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
--- a/src/HOL/ex/Executable_Relation.thy Fri Mar 23 16:16:15 2012 +0000
+++ b/src/HOL/ex/Executable_Relation.thy Fri Mar 23 16:16:35 2012 +0000
@@ -12,6 +12,7 @@
"(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
unfolding rel_raw_def by auto
+
lemma Id_raw:
"Id = rel_raw UNIV {}"
unfolding rel_raw_def by auto
@@ -74,36 +75,34 @@
lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
-definition rel :: "'a set => ('a * 'a) set => 'a rel"
-where
- "rel X R = rel_of_set (rel_raw X R)"
+quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
subsubsection {* Constant definitions on relations *}
hide_const (open) converse rel_comp rtrancl Image
quotient_definition member :: "'a * 'a => 'a rel => bool" where
- "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
+ "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
quotient_definition converse :: "'a rel => 'a rel"
where
- "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"
+ "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
quotient_definition union :: "'a rel => 'a rel => 'a rel"
where
- "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
+ "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
where
- "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
+ "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
quotient_definition rtrancl :: "'a rel => 'a rel"
where
- "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
+ "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
quotient_definition Image :: "'a rel => 'a set => 'a set"
where
- "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"
+ "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
subsubsection {* Code generation *}
@@ -111,33 +110,27 @@
lemma [code]:
"member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
-unfolding rel_def member_def
-by (simp add: member_raw)
+by (lifting member_raw)
lemma [code]:
"converse (rel X R) = rel X (R^-1)"
-unfolding rel_def converse_def
-by (simp add: converse_raw)
+by (lifting converse_raw)
lemma [code]:
"union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
-unfolding rel_def union_def
-by (simp add: union_raw)
+by (lifting union_raw)
lemma [code]:
"rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
-unfolding rel_def rel_comp_def
-by (simp add: rel_comp_raw)
+by (lifting rel_comp_raw)
lemma [code]:
"rtrancl (rel X R) = rel UNIV (R^+)"
-unfolding rel_def rtrancl_def
-by (simp add: rtrancl_raw)
+by (lifting rtrancl_raw)
lemma [code]:
"Image (rel X R) S = (X Int S) Un (R `` S)"
-unfolding rel_def Image_def
-by (simp add: Image_raw)
+by (lifting Image_raw)
quickcheck_generator rel constructors: rel