# HG changeset patch # User Cezary Kaliszyk # Date 1259936313 -3600 # Node ID 6348c2a57ec2e2168f246ba0fe2bffcfde965d45 # Parent f51e2b3e31490d36932615bebc689bdc6cef1c04 More name changes diff -r f51e2b3e3149 -r 6348c2a57ec2 FIXME-TODO --- a/FIXME-TODO Fri Dec 04 15:04:05 2009 +0100 +++ b/FIXME-TODO Fri Dec 04 15:18:33 2009 +0100 @@ -48,3 +48,5 @@ - Check all the places where we do "handle _" +- We shouldn't use the command 'quotient' as this shadows Larry's quotient. + Call it 'quotient_type' diff -r f51e2b3e3149 -r 6348c2a57ec2 FSet.thy --- a/FSet.thy Fri Dec 04 15:04:05 2009 +0100 +++ b/FSet.thy Fri Dec 04 15:18:33 2009 +0100 @@ -16,14 +16,14 @@ shows "xs \ xs" by (induct xs) (auto intro: list_eq.intros) -lemma equiv_list_eq: - shows "EQUIV list_eq" - unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def +lemma equivp_list_eq: + shows "equivp list_eq" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def apply(auto intro: list_eq.intros list_eq_refl) done quotient fset = "'a list" / "list_eq" - apply(rule equiv_list_eq) + apply(rule equivp_list_eq) done print_theorems @@ -59,7 +59,7 @@ term FUNION thm FUNION_def -thm QUOTIENT_fset +thm Quotient_fset thm QUOT_TYPE_I_fset.thm11 @@ -418,7 +418,7 @@ done quotient fset2 = "'a list" / "list_eq" - apply(rule equiv_list_eq) + apply(rule equivp_list_eq) done quotient_def @@ -431,7 +431,7 @@ where "INSERT2 \ op #" -ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *} +ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] *} diff -r f51e2b3e3149 -r 6348c2a57ec2 IntEx.thy --- a/IntEx.thy Fri Dec 04 15:04:05 2009 +0100 +++ b/IntEx.thy Fri Dec 04 15:18:33 2009 +0100 @@ -9,13 +9,13 @@ "intrel (x, y) (u, v) = (x + v = u + y)" quotient my_int = "nat \ nat" / intrel - apply(unfold EQUIV_def) + apply(unfold equivp_def) apply(auto simp add: mem_def expand_fun_eq) done thm quotient_thm -thm my_int_equiv +thm my_int_equivp print_theorems print_quotients @@ -198,30 +198,30 @@ lemma foldr_prs: - assumes a: "QUOTIENT R1 abs1 rep1" - and b: "QUOTIENT R2 abs2 rep2" + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" apply (induct l) -apply (simp add: QUOTIENT_ABS_REP[OF b]) -apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +apply (simp add: Quotient_ABS_REP[OF b]) +apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) done lemma foldl_prs: - assumes a: "QUOTIENT R1 abs1 rep1" - and b: "QUOTIENT R2 abs2 rep2" + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" apply (induct l arbitrary:e) -apply (simp add: QUOTIENT_ABS_REP[OF a]) -apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +apply (simp add: Quotient_ABS_REP[OF a]) +apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) done lemma map_prs: - assumes a: "QUOTIENT R1 abs1 rep1" - and b: "QUOTIENT R2 abs2 rep2" + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" apply (induct l) apply (simp) -apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b]) +apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b]) done @@ -231,10 +231,10 @@ by simp lemma cons_prs: - assumes a: "QUOTIENT R1 abs1 rep1" + assumes a: "Quotient R1 abs1 rep1" shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t" apply (induct t) -by (simp_all add: QUOTIENT_ABS_REP[OF a]) +by (simp_all add: Quotient_ABS_REP[OF a]) lemma cons_rsp[quotient_rsp]: "(op \ ===> LIST_REL op \ ===> LIST_REL op \) op # op #" @@ -264,7 +264,7 @@ apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) +apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) apply(simp only: nil_prs) apply(tactic {* clean_tac @{context} 1 *}) done @@ -276,8 +276,8 @@ apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int]) -apply(simp only: cons_prs[OF QUOTIENT_my_int]) +apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int]) +apply(simp only: cons_prs[OF Quotient_my_int]) apply(tactic {* clean_tac @{context} 1 *}) done diff -r f51e2b3e3149 -r 6348c2a57ec2 QuotList.thy --- a/QuotList.thy Fri Dec 04 15:04:05 2009 +0100 +++ b/QuotList.thy Fri Dec 04 15:18:33 2009 +0100 @@ -2,7 +2,7 @@ imports QuotScript begin -lemma LIST_map_I: +lemma LIST_map_id: shows "map (\x. x) = (\x. x)" by simp @@ -28,10 +28,10 @@ shows "LIST_REL R x x" by (induct x) (auto simp add: a) -lemma LIST_EQUIV: - assumes a: "EQUIV R" - shows "EQUIV (LIST_REL R)" -unfolding EQUIV_def +lemma LIST_equivp: + assumes a: "equivp R" + shows "equivp (LIST_REL R)" +unfolding equivp_def apply(rule allI)+ apply(induct_tac x y rule: list_induct2') apply(simp) @@ -46,70 +46,70 @@ apply(simp) apply(simp) using a -apply(unfold EQUIV_def) +apply(unfold equivp_def) apply(auto)[1] apply(metis LIST_REL.simps(4)) done lemma LIST_REL_REL: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "LIST_REL R r s = (LIST_REL R r r \ LIST_REL R s s \ (map Abs r = map Abs s))" apply(induct r s rule: list_induct2') apply(simp_all) -using QUOTIENT_REL[OF q] +using Quotient_REL[OF q] apply(metis) done -lemma LIST_QUOTIENT: - assumes q: "QUOTIENT R Abs Rep" - shows "QUOTIENT (LIST_REL R) (map Abs) (map Rep)" -unfolding QUOTIENT_def +lemma LIST_Quotient: + assumes q: "Quotient R Abs Rep" + shows "Quotient (LIST_REL R) (map Abs) (map Rep)" +unfolding Quotient_def apply(rule conjI) apply(rule allI) apply(induct_tac a) apply(simp) -apply(simp add: QUOTIENT_ABS_REP[OF q]) +apply(simp add: Quotient_ABS_REP[OF q]) apply(rule conjI) apply(rule allI) apply(induct_tac a) apply(simp) apply(simp) -apply(simp add: QUOTIENT_REP_REFL[OF q]) +apply(simp add: Quotient_REP_reflp[OF q]) apply(rule allI)+ apply(rule LIST_REL_REL[OF q]) done lemma CONS_PRS: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "(h#t) = (map Abs) ((Rep h)#(map Rep t))" -by (induct t) (simp_all add: QUOTIENT_ABS_REP[OF q]) +by (induct t) (simp_all add: Quotient_ABS_REP[OF q]) lemma CONS_RSP: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" and a: "R h1 h2" "LIST_REL R t1 t2" shows "LIST_REL R (h1#t1) (h2#t2)" using a by (auto) lemma NIL_PRS: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "[] = (map Abs [])" by (simp) lemma NIL_RSP: - assumes q: "QUOTIENT R Abs Rep" + assumes q: "Quotient R Abs Rep" shows "LIST_REL R [] []" by simp lemma MAP_PRS: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" shows "map f l = (map Abs2) (map ((Abs1 ---> Rep2) f) (map Rep1 l))" by (induct l) - (simp_all add: QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]) + (simp_all add: Quotient_ABS_REP[OF q1] Quotient_ABS_REP[OF q2]) lemma MAP_RSP: - assumes q1: "QUOTIENT R1 Abs1 Rep1" - and q2: "QUOTIENT R2 Abs2 Rep2" + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" and a: "(R1 ===> R2) f1 f2" and b: "LIST_REL R1 l1 l2" shows "LIST_REL R2 (map f1 l1) (map f2 l2)" diff -r f51e2b3e3149 -r 6348c2a57ec2 QuotMain.thy --- a/QuotMain.thy Fri Dec 04 15:04:05 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 15:18:33 2009 +0100 @@ -9,7 +9,7 @@ fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)" - assumes equiv: "EQUIV R" + assumes equiv: "equivp R" and rep_prop: "\y. \x. Rep y = R x" and rep_inverse: "\x. Abs (Rep x) = x" and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" @@ -29,10 +29,10 @@ lemma lem9: shows "R (Eps (R x)) = R x" proof - - have a: "R x x" using equiv by (simp add: EQUIV_REFL_SYM_TRANS REFL_def) + have a: "R x x" using equiv by (simp add: equivp_reflp_symp_transp reflp_def) then have "R x (Eps (R x))" by (rule someI) then show "R (Eps (R x)) = R x" - using equiv unfolding EQUIV_def by simp + using equiv unfolding equivp_def by simp qed theorem thm10: @@ -53,7 +53,7 @@ lemma REP_refl: shows "R (REP a) (REP a)" unfolding REP_def -by (simp add: equiv[simplified EQUIV_def]) +by (simp add: equiv[simplified equivp_def]) lemma lem7: shows "(R x = R y) = (Abs (R x) = Abs (R y))" @@ -66,7 +66,7 @@ theorem thm11: shows "R r r' = (ABS r = ABS r')" unfolding ABS_def -by (simp only: equiv[simplified EQUIV_def] lem7) +by (simp only: equiv[simplified equivp_def] lem7) lemma REP_ABS_rsp: @@ -74,13 +74,13 @@ and "R (REP (ABS g)) f = R g f" by (simp_all add: thm10 thm11) -lemma QUOTIENT: - "QUOTIENT R ABS REP" -apply(unfold QUOTIENT_def) +lemma Quotient: + "Quotient R ABS REP" +apply(unfold Quotient_def) apply(simp add: thm10) apply(simp add: REP_refl) apply(subst thm11[symmetric]) -apply(simp add: equiv[simplified EQUIV_def]) +apply(simp add: equiv[simplified equivp_def]) done lemma R_trans: @@ -88,18 +88,18 @@ and bc: "R b c" shows "R a c" proof - - have tr: "TRANS R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp + have tr: "transp R" using equiv equivp_reflp_symp_transp[of R] by simp moreover have ab: "R a b" by fact moreover have bc: "R b c" by fact - ultimately show "R a c" unfolding TRANS_def by blast + ultimately show "R a c" unfolding transp_def by blast qed lemma R_sym: assumes ab: "R a b" shows "R b a" proof - - have re: "SYM R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - then show "R b a" using ab unfolding SYM_def by blast + have re: "symp R" using equiv equivp_reflp_symp_transp[of R] by simp + then show "R b a" using ab unfolding symp_def by blast qed lemma R_trans2: @@ -128,8 +128,8 @@ then show "a = b" using rep_inverse by simp next assume ab: "a = b" - have "REFL R" using equiv EQUIV_REFL_SYM_TRANS[of R] by simp - then show "R (REP a) (REP b)" unfolding REFL_def using ab by auto + have "reflp R" using equiv equivp_reflp_symp_transp[of R] by simp + then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto qed then show "R (REP a) (REP b) \ (a = b)" by simp qed @@ -146,7 +146,7 @@ declare [[map "fun" = (fun_map, FUN_REL)]] lemmas [quotient_thm] = - FUN_QUOTIENT LIST_QUOTIENT + FUN_Quotient LIST_Quotient ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *} @@ -265,7 +265,7 @@ val rty = Logic.unvarifyT (#rtyp quotdata) val rel = #rel quotdata val rel_eqv = #equiv_thm quotdata - val rel_refl = @{thm EQUIV_REFL} OF [rel_eqv] + val rel_refl = @{thm equivp_reflp} OF [rel_eqv] in (rty, rel, rel_refl, rel_eqv) end @@ -278,7 +278,7 @@ val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") - val quot = PureThy.get_thm thy ("QUOTIENT_" ^ qty_name) + val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) in (trans2, reps_same, absrep, quot) end @@ -455,13 +455,13 @@ lemma [mono]: "P \ Q \ \Q \ \P" by auto -(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *) +(* FIXME: OPTION_equivp, PAIR_equivp, ... *) ML {* fun equiv_tac rel_eqvs = REPEAT_ALL_NEW (FIRST' [resolve_tac rel_eqvs, - rtac @{thm IDENTITY_EQUIV}, - rtac @{thm LIST_EQUIV}]) + rtac @{thm IDENTITY_equivp}, + rtac @{thm LIST_equivp}]) *} ML {* @@ -474,7 +474,7 @@ (ogl as ((Const (@{const_name "Ball"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; + val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); @@ -498,7 +498,7 @@ (ogl as ((Const (@{const_name "Bex"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R; + val gl = Const (@{const_name "equivp"}, dummyT) $ R; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); @@ -542,7 +542,7 @@ (ogl as ((Const (@{const_name "Ball"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; + val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc);*) val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); @@ -573,7 +573,7 @@ (ogl as ((Const (@{const_name "Bex"}, _)) $ ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) => (let - val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2; + val gl = Const (@{const_name "equivp"}, dummyT) $ R2; val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); (* val _ = tracing (Syntax.string_of_term ctxt glc); *) val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1); @@ -594,8 +594,8 @@ end *} -lemma eq_imp_rel: "EQUIV R \ a = b \ R a b" -by (simp add: EQUIV_REFL) +lemma eq_imp_rel: "equivp R \ a = b \ R a b" +by (simp add: equivp_reflp) ML {* fun regularize_tac ctxt rel_eqvs = @@ -724,7 +724,7 @@ ML {* fun quotient_tac ctxt = REPEAT_ALL_NEW (FIRST' - [rtac @{thm IDENTITY_QUOTIENT}, + [rtac @{thm IDENTITY_Quotient}, resolve_tac (quotient_rules_get ctxt)]) *} @@ -776,7 +776,7 @@ end *} -(* It proves the QUOTIENT assumptions by calling quotient_tac *) +(* It proves the Quotient assumptions by calling quotient_tac *) ML {* fun solve_quotient_assum i ctxt thm = let @@ -1088,7 +1088,7 @@ - Rewriting with definitions from the argument defs NewConst ----> (rep ---> abs) oldConst - - QUOTIENT_REL_REP: + - Quotient_REL_REP: Rel (Rep x) (Rep y) ----> x = y - ABS_REP @@ -1107,9 +1107,9 @@ val thy = ProofContext.theory_of lthy; val quotients = quotient_rules_get lthy val defs = map (Thm.varifyT o #def) (qconsts_dest thy); - val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quotients + val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep; - val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quotients + val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs) @@ -1237,7 +1237,7 @@ let val rthm' = atomize_thm rthm val rule = procedure_inst context (prop_of rthm') (term_of concl) - val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) rel_eqv val quotients = quotient_rules_get lthy val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb concl))] @{thm QUOT_TRUE_i} diff -r f51e2b3e3149 -r 6348c2a57ec2 quotient.ML --- a/quotient.ML Fri Dec 04 15:04:05 2009 +0100 +++ b/quotient.ML Fri Dec 04 15:18:33 2009 +0100 @@ -102,13 +102,13 @@ (* proves the quotient theorem *) fun typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_type_thm) lthy = let - val quotient_const = Const (@{const_name "QUOTIENT"}, dummyT) + val quotient_const = Const (@{const_name "Quotient"}, dummyT) val goal = HOLogic.mk_Trueprop (quotient_const $ rel $ abs $ rep) |> Syntax.check_term lthy val typedef_quotient_thm_tac = EVERY1 [K (rewrite_goals_tac [abs_def, rep_def]), - rtac @{thm QUOT_TYPE.QUOTIENT}, + rtac @{thm QUOT_TYPE.Quotient}, rtac quot_type_thm] in Goal.prove lthy [] [] goal @@ -146,7 +146,7 @@ (* quotient theorem *) val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2 - val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name + val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name (* storing the quot-info *) val qty_str = fst (Term.dest_Type abs_ty) @@ -157,7 +157,7 @@ (* FIXME: to recalculated in for example REGULARIZE *) (* storing of the equiv_thm under a name *) - val (_, lthy4) = note (Binding.suffix_name "_equiv" qty_name, equiv_thm, []) lthy3 + val (_, lthy4) = note (Binding.suffix_name "_equivp" qty_name, equiv_thm, []) lthy3 (* interpretation *) val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list)) @@ -205,9 +205,9 @@ let fun mk_goal (rty, rel) = let - val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} + val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} in - HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel) + HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) end val goals = map (mk_goal o snd) quot_list