# HG changeset patch # User Cezary Kaliszyk # Date 1277275484 -7200 # Node ID 2377d246a631114aeeae0f1d64c1c3068f373025 # Parent ab36b1a50ca8f5e087f156cb7c1303b41d8f8fdb Quotient package now uses Partial Equivalence instead place of equivalence diff -r ab36b1a50ca8 -r 2377d246a631 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Wed Jun 23 08:42:41 2010 +0200 +++ b/src/HOL/Quotient.thy Wed Jun 23 08:44:44 2010 +0200 @@ -59,7 +59,7 @@ unfolding equivp_def by auto -text {* Partial equivalences: not yet used anywhere *} +text {* Partial equivalences *} definition "part_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" @@ -71,6 +71,23 @@ unfolding equivp_def part_equivp_def by auto +lemma part_equivp_symp: + assumes e: "part_equivp R" + and a: "R x y" + shows "R y x" + using e[simplified part_equivp_def] a + by (metis) + +lemma part_equivp_typedef: + shows "part_equivp R \ \d. d \ (\c. \x. R x x \ c = R x)" + unfolding part_equivp_def mem_def + apply clarify + apply (intro exI) + apply (rule conjI) + apply assumption + apply (rule refl) + done + text {* Composition of Relations *} abbreviation @@ -630,10 +647,10 @@ fixes R :: "'a \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" and Rep :: "'b \ ('a \ bool)" - assumes equivp: "equivp R" - and rep_prop: "\y. \x. Rep y = R x" + assumes equivp: "part_equivp R" + and rep_prop: "\y. \x. R x x \ Rep y = R x" and rep_inverse: "\x. Abs (Rep x) = x" - and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and abs_inverse: "\c. (\x. ((R x x) \ (c = R x))) \ (Rep (Abs c)) = c" and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" begin @@ -647,64 +664,46 @@ where "rep a = Eps (Rep a)" -lemma homeier_lem9: - shows "R (Eps (R x)) = R x" -proof - - have a: "R x x" using equivp 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 equivp unfolding equivp_def by simp -qed - -theorem homeier_thm10: - shows "abs (rep a) = a" - unfolding abs_def rep_def -proof - - from rep_prop - obtain x where eq: "Rep a = R x" by auto - have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp - also have "\ = Abs (R x)" using homeier_lem9 by simp - also have "\ = Abs (Rep a)" using eq by simp - also have "\ = a" using rep_inverse by simp - finally - show "Abs (R (Eps (Rep a))) = a" by simp -qed +lemma homeier5: + assumes a: "R r r" + shows "Rep (Abs (R r)) = R r" + apply (subst abs_inverse) + using a by auto -lemma homeier_lem7: - shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS") -proof - - have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject) - also have "\ = ?LHS" by (simp add: abs_inverse) - finally show "?LHS = ?RHS" by simp -qed +theorem homeier6: + assumes a: "R r r" + and b: "R s s" + shows "Abs (R r) = Abs (R s) \ R r = R s" + by (metis a b homeier5) -theorem homeier_thm11: - shows "R r r' = (abs r = abs r')" - unfolding abs_def - by (simp only: equivp[simplified equivp_def] homeier_lem7) - -lemma rep_refl: - shows "R (rep a) (rep a)" - unfolding rep_def - by (simp add: equivp[simplified equivp_def]) - - -lemma rep_abs_rsp: - shows "R f (rep (abs g)) = R f g" - and "R (rep (abs g)) f = R g f" - by (simp_all add: homeier_thm10 homeier_thm11) +theorem homeier8: + assumes "R r r" + shows "R (Eps (R r)) = R r" + using assms equivp[simplified part_equivp_def] + apply clarify + by (metis assms exE_some) lemma Quotient: shows "Quotient R abs rep" - unfolding Quotient_def - apply(simp add: homeier_thm10) - apply(simp add: rep_refl) - apply(subst homeier_thm11[symmetric]) - apply(simp add: equivp[simplified equivp_def]) - done + unfolding Quotient_def abs_def rep_def + proof (intro conjI allI) + fix a r s + show "Abs (R (Eps (Rep a))) = a" + by (metis equivp exE_some part_equivp_def rep_inverse rep_prop) + show "R r s \ R r r \ R s s \ (Abs (R r) = Abs (R s))" + by (metis homeier6 equivp[simplified part_equivp_def]) + show "R (Eps (Rep a)) (Eps (Rep a))" proof - + obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto + have "R (Eps (R x)) x" using homeier8 r by simp + then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast + then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp + then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp + qed + qed end + subsection {* ML setup *} text {* Auxiliary data for the quotient package *} diff -r ab36b1a50ca8 -r 2377d246a631 src/HOL/Tools/Quotient/quotient_tacs.ML --- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 23 08:42:41 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jun 23 08:44:44 2010 +0200 @@ -147,6 +147,14 @@ finally jump back to 1 *) +fun reflp_get ctxt = + map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE + handle THM _ => NONE) (equiv_rules_get ctxt) + +val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} + +fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt) + fun regularize_tac ctxt = let val thy = ProofContext.theory_of ctxt @@ -157,8 +165,7 @@ addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} addsimprocs [simproc] addSolver equiv_solver addSolver quotient_solver - val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)} - val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt) + val eq_eqvs = eq_imp_rel_get ctxt in simp_tac simpset THEN' REPEAT_ALL_NEW (CHANGED o FIRST' @@ -254,7 +261,7 @@ val inst_thm = Drule.instantiate' ty_inst ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp} in - (rtac inst_thm THEN' quotient_tac context) 1 + (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1 end | _ => no_tac end) @@ -406,7 +413,7 @@ fun injection_tac ctxt = let - val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt) + val rel_refl = reflp_get ctxt in injection_step_tac ctxt rel_refl end diff -r ab36b1a50ca8 -r 2377d246a631 src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Wed Jun 23 08:42:41 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Wed Jun 23 08:44:44 2010 +0200 @@ -7,13 +7,13 @@ signature QUOTIENT_TYPE = sig - val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm + val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm -> Proof.context -> (thm * thm) * local_theory - val quotient_type: ((string list * binding * mixfix) * (typ * term)) list + val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list -> Proof.context -> Proof.state - val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list + val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list -> Proof.context -> Proof.state end; @@ -64,15 +64,15 @@ |> map Free in lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_eq (c, (rel $ x)))) + lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x)))))) end (* makes the new type definitions and proves non-emptyness *) -fun typedef_make (vs, qty_name, mx, rel, rty) lthy = +fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = let val typedef_tac = - EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) + EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) in (* FIXME: purely local typedef causes at the moment problems with type variables @@ -93,14 +93,14 @@ let val rep_thm = #Rep typedef_info RS mem_def1 val rep_inv = #Rep_inverse typedef_info - val abs_inv = mem_def2 RS #Abs_inverse typedef_info + val abs_inv = #Abs_inverse typedef_info val rep_inj = #Rep_inject typedef_info in (rtac @{thm quot_type.intro} THEN' RANGE [ rtac equiv_thm, rtac rep_thm, rtac rep_inv, - EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]), + rtac abs_inv THEN' rtac mem_def2 THEN' atac, rtac rep_inj]) 1 end @@ -137,10 +137,12 @@ (* main function for constructing a quotient type *) -fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy = +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = let + val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp} + (* generates the typedef *) - val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy + val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy (* abs and rep functions from the typedef *) val Abs_ty = #abs_type (#1 typedef_info) @@ -162,7 +164,7 @@ val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2 (* quot_type theorem *) - val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3 + val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3 (* quotient theorem *) val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3 @@ -179,12 +181,12 @@ in lthy4 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) - ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) + ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) end (* sanity checks for the quotient type specifications *) -fun sanity_check ((vs, qty_name, _), (rty, rel)) = +fun sanity_check ((vs, qty_name, _), (rty, rel, _)) = let val rty_tfreesT = map fst (Term.add_tfreesT rty []) val rel_tfrees = map fst (Term.add_tfrees rel []) @@ -223,7 +225,7 @@ end (* check for existence of map functions *) -fun map_check ctxt (_, (rty, _)) = +fun map_check ctxt (_, (rty, _, _)) = let val thy = ProofContext.theory_of ctxt @@ -263,11 +265,12 @@ val _ = List.app sanity_check quot_list val _ = List.app (map_check lthy) quot_list - fun mk_goal (rty, rel) = + fun mk_goal (rty, rel, partial) = let val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} + val const = if partial then @{const_name part_equivp} else @{const_name equivp} in - HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel) + HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) end val goals = map (mk_goal o snd) quot_list @@ -280,7 +283,7 @@ fun quotient_type_cmd specs lthy = let - fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy = + fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy = let val rty = Syntax.read_typ lthy rty_str val lthy1 = Variable.declare_typ rty lthy @@ -290,7 +293,7 @@ |> Syntax.check_term lthy1 val lthy2 = Variable.declare_term rel lthy1 in - (((vs, qty_name, mx), (rty, rel)), lthy2) + (((vs, qty_name, mx), (rty, rel, partial)), lthy2) end val (spec', lthy') = fold_map parse_spec specs lthy @@ -298,11 +301,13 @@ quotient_type spec' lthy' end +val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false + val quotspec_parser = - Parse.and_list1 - ((Parse.type_args -- Parse.binding) -- - Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- - (Parse.$$$ "/" |-- Parse.term)) + Parse.and_list1 + ((Parse.type_args -- Parse.binding) -- + Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- + (Parse.$$$ "/" |-- (partial -- Parse.term))) val _ = Keyword.keyword "/"