# HG changeset patch # User Cezary Kaliszyk # Date 1264099966 -3600 # Node ID b1f55dd64481b212440a66ff829b1f556c9540ae # Parent aa960d16570fa6f01c3d4199cd1f2f62480aaee4 Changed fun_map and rel_map to definitions. diff -r aa960d16570f -r b1f55dd64481 Quot/Examples/IntEx2.thy --- a/Quot/Examples/IntEx2.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/Examples/IntEx2.thy Thu Jan 21 19:52:46 2010 +0100 @@ -108,7 +108,7 @@ lemma mult_raw_rsp[quot_respect]: shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" -apply(simp only: fun_rel.simps) +apply(simp only: fun_rel_def) apply(rule allI | rule impI)+ apply(rule equivp_transp[OF int_equivp]) apply(rule mult_raw_fst) diff -r aa960d16570f -r b1f55dd64481 Quot/Examples/LarryInt.thy --- a/Quot/Examples/LarryInt.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/Examples/LarryInt.thy Thu Jan 21 19:52:46 2010 +0100 @@ -178,7 +178,7 @@ lemma [quot_respect]: shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw" -apply(simp only: fun_rel.simps) +apply(simp only: fun_rel_def) apply(rule allI | rule impI)+ apply(rule equivp_transp[OF int_equivp]) apply(rule mult_raw_fst) diff -r aa960d16570f -r b1f55dd64481 Quot/QuotList.thy --- a/Quot/QuotList.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/QuotList.thy Thu Jan 21 19:52:46 2010 +0100 @@ -74,7 +74,7 @@ lemma cons_prs[quot_preserve]: assumes q: "Quotient R Abs Rep" shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)" -by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q]) +by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q]) (simp) lemma cons_rsp[quot_respect]: @@ -103,7 +103,7 @@ assumes a: "Quotient R1 abs1 rep1" and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map" -by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b]) +by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b]) (simp) @@ -129,7 +129,7 @@ assumes a: "Quotient R1 abs1 rep1" and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr" -by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b]) +by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b]) (simp) lemma foldl_prs_aux: @@ -143,7 +143,7 @@ assumes a: "Quotient R1 abs1 rep1" and b: "Quotient R2 abs2 rep2" shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl" -by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b]) +by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b]) (simp) lemma list_rel_empty: "list_rel R [] b \ length b = 0" diff -r aa960d16570f -r b1f55dd64481 Quot/QuotProd.thy --- a/Quot/QuotProd.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/QuotProd.thy Thu Jan 21 19:52:46 2010 +0100 @@ -46,7 +46,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" -apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2]) +apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2]) apply(simp) done diff -r aa960d16570f -r b1f55dd64481 Quot/QuotScript.thy --- a/Quot/QuotScript.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/QuotScript.thy Thu Jan 21 19:52:46 2010 +0100 @@ -126,30 +126,19 @@ using a unfolding Quotient_def transp_def by metis -fun - fun_map +definition + fun_map (infixr "--->" 55) where - "fun_map f g h x = g (h (f x))" - -abbreviation - fun_map_syn (infixr "--->" 55) -where - "f ---> g \ fun_map f g" +[simp]: "fun_map f g h x = g (h (f x))" lemma fun_map_id: shows "(id ---> id) = id" by (simp add: expand_fun_eq id_def) - -fun - fun_rel +definition + fun_rel (infixr "===>" 55) where - "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" - -abbreviation - fun_rel_syn (infixr "===>" 55) -where - "E1 ===> E2 \ fun_rel E1 E2" +[simp]: "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" lemma fun_rel_eq: "(op =) ===> (op =) \ (op =)" @@ -453,18 +442,18 @@ shows "equivp R \ Babs (Respects R) P = P" by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp) -(* 2 lemmas needed for cleaning of quantifiers *) +(* 3 lemmas needed for cleaning of quantifiers *) lemma all_prs: assumes a: "Quotient R absf repf" shows "Ball (Respects R) ((absf ---> id) f) = All f" - using a unfolding Quotient_def - by (metis in_respects fun_map.simps id_apply) + using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply +by metis lemma ex_prs: assumes a: "Quotient R absf repf" shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding Quotient_def - by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) + using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply + by metis lemma ex1_prs: assumes a: "Quotient R absf repf" @@ -639,8 +628,13 @@ and r2: "Respects (R1 ===> R2) g" shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\x y. R1 x y \ R2 (f x) (g y))" apply(rule_tac iffI) + apply(rule)+ + apply (rule apply_rsp'[of "R1" "R2"]) + apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]]) + apply auto using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def - apply(metis apply_rsp') + apply (metis let_rsp q1) + apply (metis fun_rel_eq_rel let_rsp q1 q2 r2) using r1 unfolding Respects_def expand_fun_eq apply(simp (no_asm_use)) apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) diff -r aa960d16570f -r b1f55dd64481 Quot/quotient_tacs.ML --- a/Quot/quotient_tacs.ML Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/quotient_tacs.ML Thu Jan 21 19:52:46 2010 +0100 @@ -431,7 +431,7 @@ ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => if (member (op=) xs h) then Conv.all_conv ctrm - else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm + else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm | _ => Conv.all_conv ctrm fun fun_map_conv xs ctxt ctrm =