kuncar@47308: (* Title: HOL/Lifting.thy kuncar@47308: Author: Brian Huffman and Ondrej Kuncar kuncar@47308: Author: Cezary Kaliszyk and Christian Urban kuncar@47308: *) kuncar@47308: kuncar@47308: header {* Lifting package *} kuncar@47308: kuncar@47308: theory Lifting huffman@47325: imports Plain Equiv_Relations Transfer kuncar@47308: keywords kuncar@47308: "print_quotmaps" "print_quotients" :: diag and kuncar@47308: "lift_definition" :: thy_goal and kuncar@47308: "setup_lifting" :: thy_decl kuncar@47308: begin kuncar@47308: huffman@47325: subsection {* Function map *} kuncar@47308: kuncar@47308: notation map_fun (infixr "--->" 55) kuncar@47308: kuncar@47308: lemma map_fun_id: kuncar@47308: "(id ---> id) = id" kuncar@47308: by (simp add: fun_eq_iff) kuncar@47308: kuncar@47308: subsection {* Quotient Predicate *} kuncar@47308: kuncar@47308: definition kuncar@47308: "Quotient R Abs Rep T \ kuncar@47308: (\a. Abs (Rep a) = a) \ kuncar@47308: (\a. R (Rep a) (Rep a)) \ kuncar@47308: (\r s. R r s \ R r r \ R s s \ Abs r = Abs s) \ kuncar@47308: T = (\x y. R x x \ Abs x = y)" kuncar@47308: kuncar@47308: lemma QuotientI: kuncar@47308: assumes "\a. Abs (Rep a) = a" kuncar@47308: and "\a. R (Rep a) (Rep a)" kuncar@47308: and "\r s. R r s \ R r r \ R s s \ Abs r = Abs s" kuncar@47308: and "T = (\x y. R x x \ Abs x = y)" kuncar@47308: shows "Quotient R Abs Rep T" kuncar@47308: using assms unfolding Quotient_def by blast kuncar@47308: huffman@47536: context huffman@47536: fixes R Abs Rep T kuncar@47308: assumes a: "Quotient R Abs Rep T" huffman@47536: begin huffman@47536: huffman@47536: lemma Quotient_abs_rep: "Abs (Rep a) = a" huffman@47536: using a unfolding Quotient_def kuncar@47308: by simp kuncar@47308: huffman@47536: lemma Quotient_rep_reflp: "R (Rep a) (Rep a)" huffman@47536: using a unfolding Quotient_def kuncar@47308: by blast kuncar@47308: kuncar@47308: lemma Quotient_rel: huffman@47536: "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} huffman@47536: using a unfolding Quotient_def kuncar@47308: by blast kuncar@47308: huffman@47536: lemma Quotient_cr_rel: "T = (\x y. R x x \ Abs x = y)" kuncar@47308: using a unfolding Quotient_def kuncar@47308: by blast kuncar@47308: huffman@47536: lemma Quotient_refl1: "R r s \ R r r" huffman@47536: using a unfolding Quotient_def huffman@47536: by fast huffman@47536: huffman@47536: lemma Quotient_refl2: "R r s \ R s s" huffman@47536: using a unfolding Quotient_def huffman@47536: by fast huffman@47536: huffman@47536: lemma Quotient_rel_rep: "R (Rep a) (Rep b) \ a = b" huffman@47536: using a unfolding Quotient_def huffman@47536: by metis huffman@47536: huffman@47536: lemma Quotient_rep_abs: "R r r \ R (Rep (Abs r)) r" kuncar@47308: using a unfolding Quotient_def kuncar@47308: by blast kuncar@47308: kuncar@47937: lemma Quotient_rep_abs_fold_unmap: kuncar@47937: assumes "x' \ Abs x" and "R x x" and "Rep x' \ Rep' x'" kuncar@47937: shows "R (Rep' x') x" kuncar@47937: proof - kuncar@47937: have "R (Rep x') x" using assms(1-2) Quotient_rep_abs by auto kuncar@47937: then show ?thesis using assms(3) by simp kuncar@47937: qed kuncar@47937: kuncar@47937: lemma Quotient_Rep_eq: kuncar@47937: assumes "x' \ Abs x" kuncar@47937: shows "Rep x' \ Rep x'" kuncar@47937: by simp kuncar@47937: huffman@47536: lemma Quotient_rel_abs: "R r s \ Abs r = Abs s" huffman@47536: using a unfolding Quotient_def huffman@47536: by blast huffman@47536: kuncar@47937: lemma Quotient_rel_abs2: kuncar@47937: assumes "R (Rep x) y" kuncar@47937: shows "x = Abs y" kuncar@47937: proof - kuncar@47937: from assms have "Abs (Rep x) = Abs y" by (auto intro: Quotient_rel_abs) kuncar@47937: then show ?thesis using assms(1) by (simp add: Quotient_abs_rep) kuncar@47937: qed kuncar@47937: huffman@47536: lemma Quotient_symp: "symp R" kuncar@47308: using a unfolding Quotient_def using sympI by (metis (full_types)) kuncar@47308: huffman@47536: lemma Quotient_transp: "transp R" kuncar@47308: using a unfolding Quotient_def using transpI by (metis (full_types)) kuncar@47308: huffman@47536: lemma Quotient_part_equivp: "part_equivp R" huffman@47536: by (metis Quotient_rep_reflp Quotient_symp Quotient_transp part_equivpI) huffman@47536: huffman@47536: end kuncar@47308: kuncar@47308: lemma identity_quotient: "Quotient (op =) id id (op =)" kuncar@47308: unfolding Quotient_def by simp kuncar@47308: huffman@47652: text {* TODO: Use one of these alternatives as the real definition. *} huffman@47652: kuncar@47308: lemma Quotient_alt_def: kuncar@47308: "Quotient R Abs Rep T \ kuncar@47308: (\a b. T a b \ Abs a = b) \ kuncar@47308: (\b. T (Rep b) b) \ kuncar@47308: (\x y. R x y \ T x (Abs x) \ T y (Abs y) \ Abs x = Abs y)" kuncar@47308: apply safe kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (simp (no_asm_use) only: Quotient_def, fast) kuncar@47308: apply (rule QuotientI) kuncar@47308: apply simp kuncar@47308: apply metis kuncar@47308: apply simp kuncar@47308: apply (rule ext, rule ext, metis) kuncar@47308: done kuncar@47308: kuncar@47308: lemma Quotient_alt_def2: kuncar@47308: "Quotient R Abs Rep T \ kuncar@47308: (\a b. T a b \ Abs a = b) \ kuncar@47308: (\b. T (Rep b) b) \ kuncar@47308: (\x y. R x y \ T x (Abs y) \ T y (Abs x))" kuncar@47308: unfolding Quotient_alt_def by (safe, metis+) kuncar@47308: huffman@47652: lemma Quotient_alt_def3: huffman@47652: "Quotient R Abs Rep T \ huffman@47652: (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ huffman@47652: (\x y. R x y \ (\z. T x z \ T y z))" huffman@47652: unfolding Quotient_alt_def2 by (safe, metis+) huffman@47652: huffman@47652: lemma Quotient_alt_def4: huffman@47652: "Quotient R Abs Rep T \ huffman@47652: (\a b. T a b \ Abs a = b) \ (\b. T (Rep b) b) \ R = T OO conversep T" huffman@47652: unfolding Quotient_alt_def3 fun_eq_iff by auto huffman@47652: kuncar@47308: lemma fun_quotient: kuncar@47308: assumes 1: "Quotient R1 abs1 rep1 T1" kuncar@47308: assumes 2: "Quotient R2 abs2 rep2 T2" kuncar@47308: shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2) (T1 ===> T2)" kuncar@47308: using assms unfolding Quotient_alt_def2 kuncar@47308: unfolding fun_rel_def fun_eq_iff map_fun_apply kuncar@47308: by (safe, metis+) kuncar@47308: kuncar@47308: lemma apply_rsp: kuncar@47308: fixes f g::"'a \ 'c" kuncar@47308: assumes q: "Quotient R1 Abs1 Rep1 T1" kuncar@47308: and a: "(R1 ===> R2) f g" "R1 x y" kuncar@47308: shows "R2 (f x) (g y)" kuncar@47308: using a by (auto elim: fun_relE) kuncar@47308: kuncar@47308: lemma apply_rsp': kuncar@47308: assumes a: "(R1 ===> R2) f g" "R1 x y" kuncar@47308: shows "R2 (f x) (g y)" kuncar@47308: using a by (auto elim: fun_relE) kuncar@47308: kuncar@47308: lemma apply_rsp'': kuncar@47308: assumes "Quotient R Abs Rep T" kuncar@47308: and "(R ===> S) f f" kuncar@47308: shows "S (f (Rep x)) (f (Rep x))" kuncar@47308: proof - kuncar@47308: from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient_rep_reflp) kuncar@47308: then show ?thesis using assms(2) by (auto intro: apply_rsp') kuncar@47308: qed kuncar@47308: kuncar@47308: subsection {* Quotient composition *} kuncar@47308: kuncar@47308: lemma Quotient_compose: kuncar@47308: assumes 1: "Quotient R1 Abs1 Rep1 T1" kuncar@47308: assumes 2: "Quotient R2 Abs2 Rep2 T2" kuncar@47308: shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \ Abs1) (Rep1 \ Rep2) (T1 OO T2)" huffman@47652: using assms unfolding Quotient_alt_def4 by (auto intro!: ext) kuncar@47308: kuncar@47521: lemma equivp_reflp2: kuncar@47521: "equivp R \ reflp R" kuncar@47521: by (erule equivpE) kuncar@47521: huffman@47544: subsection {* Respects predicate *} huffman@47544: huffman@47544: definition Respects :: "('a \ 'a \ bool) \ 'a set" huffman@47544: where "Respects R = {x. R x x}" huffman@47544: huffman@47544: lemma in_respects: "x \ Respects R \ R x x" huffman@47544: unfolding Respects_def by simp huffman@47544: kuncar@47308: subsection {* Invariant *} kuncar@47308: kuncar@47308: definition invariant :: "('a \ bool) \ 'a \ 'a \ bool" kuncar@47308: where "invariant R = (\x y. R x \ x = y)" kuncar@47308: kuncar@47308: lemma invariant_to_eq: kuncar@47308: assumes "invariant P x y" kuncar@47308: shows "x = y" kuncar@47308: using assms by (simp add: invariant_def) kuncar@47308: kuncar@47308: lemma fun_rel_eq_invariant: kuncar@47308: shows "((invariant R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" kuncar@47308: by (auto simp add: invariant_def fun_rel_def) kuncar@47308: kuncar@47308: lemma invariant_same_args: kuncar@47308: shows "invariant P x x \ P x" kuncar@47308: using assms by (auto simp add: invariant_def) kuncar@47308: kuncar@47361: lemma UNIV_typedef_to_Quotient: kuncar@47308: assumes "type_definition Rep Abs UNIV" kuncar@47361: and T_def: "T \ (\x y. x = Rep y)" kuncar@47308: shows "Quotient (op =) Abs Rep T" kuncar@47308: proof - kuncar@47308: interpret type_definition Rep Abs UNIV by fact kuncar@47361: from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis kuncar@47361: by (fastforce intro!: QuotientI fun_eq_iff) kuncar@47308: qed kuncar@47308: kuncar@47361: lemma UNIV_typedef_to_equivp: kuncar@47308: fixes Abs :: "'a \ 'b" kuncar@47308: and Rep :: "'b \ 'a" kuncar@47308: assumes "type_definition Rep Abs (UNIV::'a set)" kuncar@47308: shows "equivp (op=::'a\'a\bool)" kuncar@47308: by (rule identity_equivp) kuncar@47308: huffman@47354: lemma typedef_to_Quotient: kuncar@47361: assumes "type_definition Rep Abs S" kuncar@47361: and T_def: "T \ (\x y. x = Rep y)" kuncar@47501: shows "Quotient (invariant (\x. x \ S)) Abs Rep T" kuncar@47361: proof - kuncar@47361: interpret type_definition Rep Abs S by fact kuncar@47361: from Rep Abs_inject Rep_inverse Abs_inverse T_def show ?thesis kuncar@47361: by (auto intro!: QuotientI simp: invariant_def fun_eq_iff) kuncar@47361: qed kuncar@47361: kuncar@47361: lemma typedef_to_part_equivp: kuncar@47361: assumes "type_definition Rep Abs S" kuncar@47501: shows "part_equivp (invariant (\x. x \ S))" kuncar@47361: proof (intro part_equivpI) kuncar@47361: interpret type_definition Rep Abs S by fact kuncar@47501: show "\x. invariant (\x. x \ S) x x" using Rep by (auto simp: invariant_def) kuncar@47361: next kuncar@47501: show "symp (invariant (\x. x \ S))" by (auto intro: sympI simp: invariant_def) kuncar@47361: next kuncar@47501: show "transp (invariant (\x. x \ S))" by (auto intro: transpI simp: invariant_def) kuncar@47361: qed kuncar@47361: kuncar@47361: lemma open_typedef_to_Quotient: kuncar@47308: assumes "type_definition Rep Abs {x. P x}" huffman@47354: and T_def: "T \ (\x y. x = Rep y)" kuncar@47308: shows "Quotient (invariant P) Abs Rep T" huffman@47651: using typedef_to_Quotient [OF assms] by simp kuncar@47308: kuncar@47361: lemma open_typedef_to_part_equivp: kuncar@47308: assumes "type_definition Rep Abs {x. P x}" kuncar@47308: shows "part_equivp (invariant P)" huffman@47651: using typedef_to_part_equivp [OF assms] by simp kuncar@47308: huffman@47376: text {* Generating transfer rules for quotients. *} huffman@47376: huffman@47537: context huffman@47537: fixes R Abs Rep T huffman@47537: assumes 1: "Quotient R Abs Rep T" huffman@47537: begin huffman@47376: huffman@47537: lemma Quotient_right_unique: "right_unique T" huffman@47537: using 1 unfolding Quotient_alt_def right_unique_def by metis huffman@47537: huffman@47537: lemma Quotient_right_total: "right_total T" huffman@47537: using 1 unfolding Quotient_alt_def right_total_def by metis huffman@47537: huffman@47537: lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)" huffman@47537: using 1 unfolding Quotient_alt_def fun_rel_def by simp huffman@47376: huffman@47538: lemma Quotient_abs_induct: huffman@47538: assumes "\y. R y y \ P (Abs y)" shows "P x" huffman@47538: using 1 assms unfolding Quotient_def by metis huffman@47538: huffman@47544: lemma Quotient_All_transfer: huffman@47544: "((T ===> op =) ===> op =) (Ball (Respects R)) All" huffman@47544: unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] huffman@47544: by (auto, metis Quotient_abs_induct) huffman@47544: huffman@47544: lemma Quotient_Ex_transfer: huffman@47544: "((T ===> op =) ===> op =) (Bex (Respects R)) Ex" huffman@47544: unfolding fun_rel_def Respects_def Quotient_cr_rel [OF 1] huffman@47544: by (auto, metis Quotient_rep_reflp [OF 1] Quotient_abs_rep [OF 1]) huffman@47544: huffman@47544: lemma Quotient_forall_transfer: huffman@47544: "((T ===> op =) ===> op =) (transfer_bforall (\x. R x x)) transfer_forall" huffman@47544: using Quotient_All_transfer huffman@47544: unfolding transfer_forall_def transfer_bforall_def huffman@47544: Ball_def [abs_def] in_respects . huffman@47544: huffman@47537: end huffman@47537: huffman@47537: text {* Generating transfer rules for total quotients. *} huffman@47376: huffman@47537: context huffman@47537: fixes R Abs Rep T huffman@47537: assumes 1: "Quotient R Abs Rep T" and 2: "reflp R" huffman@47537: begin huffman@47376: huffman@47537: lemma Quotient_bi_total: "bi_total T" huffman@47537: using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto huffman@47537: huffman@47537: lemma Quotient_id_abs_transfer: "(op = ===> T) (\x. x) Abs" huffman@47537: using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp huffman@47537: huffman@47575: lemma Quotient_total_abs_induct: "(\y. P (Abs y)) \ P x" huffman@47575: using 1 2 assms unfolding Quotient_alt_def reflp_def by metis huffman@47575: huffman@47889: lemma Quotient_total_abs_eq_iff: "Abs x = Abs y \ R x y" huffman@47889: using Quotient_rel [OF 1] 2 unfolding reflp_def by simp huffman@47889: huffman@47537: end huffman@47376: huffman@47368: text {* Generating transfer rules for a type defined with @{text "typedef"}. *} huffman@47368: huffman@47534: context huffman@47534: fixes Rep Abs A T huffman@47368: assumes type: "type_definition Rep Abs A" huffman@47534: assumes T_def: "T \ (\(x::'a) (y::'b). x = Rep y)" huffman@47534: begin huffman@47534: huffman@47534: lemma typedef_bi_unique: "bi_unique T" huffman@47368: unfolding bi_unique_def T_def huffman@47368: by (simp add: type_definition.Rep_inject [OF type]) huffman@47368: huffman@47535: lemma typedef_rep_transfer: "(T ===> op =) (\x. x) Rep" huffman@47535: unfolding fun_rel_def T_def by simp huffman@47535: kuncar@47545: lemma typedef_All_transfer: "((T ===> op =) ===> op =) (Ball A) All" huffman@47534: unfolding T_def fun_rel_def huffman@47534: by (metis type_definition.Rep [OF type] huffman@47534: type_definition.Abs_inverse [OF type]) huffman@47534: kuncar@47545: lemma typedef_Ex_transfer: "((T ===> op =) ===> op =) (Bex A) Ex" kuncar@47545: unfolding T_def fun_rel_def kuncar@47545: by (metis type_definition.Rep [OF type] kuncar@47545: type_definition.Abs_inverse [OF type]) kuncar@47545: kuncar@47545: lemma typedef_forall_transfer: huffman@47534: "((T ===> op =) ===> op =) huffman@47534: (transfer_bforall (\x. x \ A)) transfer_forall" huffman@47534: unfolding transfer_bforall_def transfer_forall_def Ball_def [symmetric] kuncar@47545: by (rule typedef_All_transfer) huffman@47534: huffman@47534: end huffman@47534: huffman@47368: text {* Generating the correspondence rule for a constant defined with huffman@47368: @{text "lift_definition"}. *} huffman@47368: huffman@47351: lemma Quotient_to_transfer: huffman@47351: assumes "Quotient R Abs Rep T" and "R c c" and "c' \ Abs c" huffman@47351: shows "T c c'" huffman@47351: using assms by (auto dest: Quotient_cr_rel) huffman@47351: kuncar@47982: text {* Proving reflexivity *} kuncar@47982: kuncar@47982: definition left_total :: "('a \ 'b \ bool) \ bool" kuncar@47982: where "left_total R \ (\x. \y. R x y)" kuncar@47982: kuncar@47982: lemma left_totalI: kuncar@47982: "(\x. \y. R x y) \ left_total R" kuncar@47982: unfolding left_total_def by blast kuncar@47982: kuncar@47982: lemma left_totalE: kuncar@47982: assumes "left_total R" kuncar@47982: obtains "(\x. \y. R x y)" kuncar@47982: using assms unfolding left_total_def by blast kuncar@47982: kuncar@47982: lemma Quotient_to_left_total: kuncar@47982: assumes q: "Quotient R Abs Rep T" kuncar@47982: and r_R: "reflp R" kuncar@47982: shows "left_total T" kuncar@47982: using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE) kuncar@47982: kuncar@47982: lemma reflp_Quotient_composition: kuncar@47982: assumes lt_R1: "left_total R1" kuncar@47982: and r_R2: "reflp R2" kuncar@47982: shows "reflp (R1 OO R2 OO R1\\)" kuncar@47982: using assms kuncar@47982: proof - kuncar@47982: { kuncar@47982: fix x kuncar@47982: from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast kuncar@47982: moreover then have "R1\\ y x" by simp kuncar@47982: moreover have "R2 y y" using r_R2 by (auto elim: reflpE) kuncar@47982: ultimately have "(R1 OO R2 OO R1\\) x x" by auto kuncar@47982: } kuncar@47982: then show ?thesis by (auto intro: reflpI) kuncar@47982: qed kuncar@47982: kuncar@47982: lemma reflp_equality: "reflp (op =)" kuncar@47982: by (auto intro: reflpI) kuncar@47982: kuncar@47308: subsection {* ML setup *} kuncar@47308: wenzelm@48891: ML_file "Tools/Lifting/lifting_util.ML" kuncar@47308: wenzelm@48891: ML_file "Tools/Lifting/lifting_info.ML" kuncar@47308: setup Lifting_Info.setup kuncar@47308: kuncar@47777: declare fun_quotient[quot_map] kuncar@47982: lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition kuncar@47308: wenzelm@48891: ML_file "Tools/Lifting/lifting_term.ML" kuncar@47308: wenzelm@48891: ML_file "Tools/Lifting/lifting_def.ML" kuncar@47308: wenzelm@48891: ML_file "Tools/Lifting/lifting_setup.ML" kuncar@47308: kuncar@47308: hide_const (open) invariant kuncar@47308: kuncar@47308: end