Quotient package now uses Partial Equivalence instead place of equivalence
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jun 23 08:44:44 2010 +0200 (2010-06-23)
changeset 374932377d246a631
parent 37492 ab36b1a50ca8
child 37494 6e9f48cf6adf
Quotient package now uses Partial Equivalence instead place of equivalence
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_typ.ML
     1.1 --- a/src/HOL/Quotient.thy	Wed Jun 23 08:42:41 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Jun 23 08:44:44 2010 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4    unfolding equivp_def
     1.5    by auto
     1.6  
     1.7 -text {* Partial equivalences: not yet used anywhere *}
     1.8 +text {* Partial equivalences *}
     1.9  
    1.10  definition
    1.11    "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
    1.12 @@ -71,6 +71,23 @@
    1.13    unfolding equivp_def part_equivp_def
    1.14    by auto
    1.15  
    1.16 +lemma part_equivp_symp:
    1.17 +  assumes e: "part_equivp R"
    1.18 +  and a: "R x y"
    1.19 +  shows "R y x"
    1.20 +  using e[simplified part_equivp_def] a
    1.21 +  by (metis)
    1.22 +
    1.23 +lemma part_equivp_typedef:
    1.24 +  shows "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
    1.25 +  unfolding part_equivp_def mem_def
    1.26 +  apply clarify
    1.27 +  apply (intro exI)
    1.28 +  apply (rule conjI)
    1.29 +  apply assumption
    1.30 +  apply (rule refl)
    1.31 +  done
    1.32 +
    1.33  text {* Composition of Relations *}
    1.34  
    1.35  abbreviation
    1.36 @@ -630,10 +647,10 @@
    1.37    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.38    and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
    1.39    and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
    1.40 -  assumes equivp: "equivp R"
    1.41 -  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
    1.42 +  assumes equivp: "part_equivp R"
    1.43 +  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
    1.44    and     rep_inverse: "\<And>x. Abs (Rep x) = x"
    1.45 -  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
    1.46 +  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
    1.47    and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
    1.48  begin
    1.49  
    1.50 @@ -647,64 +664,46 @@
    1.51  where
    1.52    "rep a = Eps (Rep a)"
    1.53  
    1.54 -lemma homeier_lem9:
    1.55 -  shows "R (Eps (R x)) = R x"
    1.56 -proof -
    1.57 -  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
    1.58 -  then have "R x (Eps (R x))" by (rule someI)
    1.59 -  then show "R (Eps (R x)) = R x"
    1.60 -    using equivp unfolding equivp_def by simp
    1.61 -qed
    1.62 -
    1.63 -theorem homeier_thm10:
    1.64 -  shows "abs (rep a) = a"
    1.65 -  unfolding abs_def rep_def
    1.66 -proof -
    1.67 -  from rep_prop
    1.68 -  obtain x where eq: "Rep a = R x" by auto
    1.69 -  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
    1.70 -  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
    1.71 -  also have "\<dots> = Abs (Rep a)" using eq by simp
    1.72 -  also have "\<dots> = a" using rep_inverse by simp
    1.73 -  finally
    1.74 -  show "Abs (R (Eps (Rep a))) = a" by simp
    1.75 -qed
    1.76 +lemma homeier5:
    1.77 +  assumes a: "R r r"
    1.78 +  shows "Rep (Abs (R r)) = R r"
    1.79 +  apply (subst abs_inverse)
    1.80 +  using a by auto
    1.81  
    1.82 -lemma homeier_lem7:
    1.83 -  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
    1.84 -proof -
    1.85 -  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
    1.86 -  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
    1.87 -  finally show "?LHS = ?RHS" by simp
    1.88 -qed
    1.89 +theorem homeier6:
    1.90 +  assumes a: "R r r"
    1.91 +  and b: "R s s"
    1.92 +  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
    1.93 +  by (metis a b homeier5)
    1.94  
    1.95 -theorem homeier_thm11:
    1.96 -  shows "R r r' = (abs r = abs r')"
    1.97 -  unfolding abs_def
    1.98 -  by (simp only: equivp[simplified equivp_def] homeier_lem7)
    1.99 -
   1.100 -lemma rep_refl:
   1.101 -  shows "R (rep a) (rep a)"
   1.102 -  unfolding rep_def
   1.103 -  by (simp add: equivp[simplified equivp_def])
   1.104 -
   1.105 -
   1.106 -lemma rep_abs_rsp:
   1.107 -  shows "R f (rep (abs g)) = R f g"
   1.108 -  and   "R (rep (abs g)) f = R g f"
   1.109 -  by (simp_all add: homeier_thm10 homeier_thm11)
   1.110 +theorem homeier8:
   1.111 +  assumes "R r r"
   1.112 +  shows "R (Eps (R r)) = R r"
   1.113 +  using assms equivp[simplified part_equivp_def]
   1.114 +  apply clarify
   1.115 +  by (metis assms exE_some)
   1.116  
   1.117  lemma Quotient:
   1.118    shows "Quotient R abs rep"
   1.119 -  unfolding Quotient_def
   1.120 -  apply(simp add: homeier_thm10)
   1.121 -  apply(simp add: rep_refl)
   1.122 -  apply(subst homeier_thm11[symmetric])
   1.123 -  apply(simp add: equivp[simplified equivp_def])
   1.124 -  done
   1.125 +  unfolding Quotient_def abs_def rep_def
   1.126 +  proof (intro conjI allI)
   1.127 +    fix a r s
   1.128 +    show "Abs (R (Eps (Rep a))) = a"
   1.129 +      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
   1.130 +    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
   1.131 +      by (metis homeier6 equivp[simplified part_equivp_def])
   1.132 +    show "R (Eps (Rep a)) (Eps (Rep a))" proof -
   1.133 +      obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
   1.134 +      have "R (Eps (R x)) x" using homeier8 r by simp
   1.135 +      then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
   1.136 +      then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
   1.137 +      then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
   1.138 +    qed
   1.139 +  qed
   1.140  
   1.141  end
   1.142  
   1.143 +
   1.144  subsection {* ML setup *}
   1.145  
   1.146  text {* Auxiliary data for the quotient package *}
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 23 08:42:41 2010 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jun 23 08:44:44 2010 +0200
     2.3 @@ -147,6 +147,14 @@
     2.4    finally jump back to 1
     2.5  *)
     2.6  
     2.7 +fun reflp_get ctxt =
     2.8 +  map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
     2.9 +    handle THM _ => NONE) (equiv_rules_get ctxt)
    2.10 +
    2.11 +val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
    2.12 +
    2.13 +fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
    2.14 +
    2.15  fun regularize_tac ctxt =
    2.16  let
    2.17    val thy = ProofContext.theory_of ctxt
    2.18 @@ -157,8 +165,7 @@
    2.19                         addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp}
    2.20                         addsimprocs [simproc]
    2.21                         addSolver equiv_solver addSolver quotient_solver
    2.22 -  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
    2.23 -  val eq_eqvs = map (OF1 eq_imp_rel) (equiv_rules_get ctxt)
    2.24 +  val eq_eqvs = eq_imp_rel_get ctxt
    2.25  in
    2.26    simp_tac simpset THEN'
    2.27    REPEAT_ALL_NEW (CHANGED o FIRST'
    2.28 @@ -254,7 +261,7 @@
    2.29               val inst_thm = Drule.instantiate' ty_inst
    2.30                 ([NONE, NONE, NONE] @ t_inst) @{thm apply_rsp}
    2.31             in
    2.32 -             (rtac inst_thm THEN' quotient_tac context) 1
    2.33 +             (rtac inst_thm THEN' SOLVED' (quotient_tac context)) 1
    2.34             end
    2.35      | _ => no_tac
    2.36    end)
    2.37 @@ -406,7 +413,7 @@
    2.38  
    2.39  fun injection_tac ctxt =
    2.40  let
    2.41 -  val rel_refl = map (OF1 @{thm equivp_reflp}) (equiv_rules_get ctxt)
    2.42 +  val rel_refl = reflp_get ctxt
    2.43  in
    2.44    injection_step_tac ctxt rel_refl
    2.45  end
     3.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Jun 23 08:42:41 2010 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Wed Jun 23 08:44:44 2010 +0200
     3.3 @@ -7,13 +7,13 @@
     3.4  
     3.5  signature QUOTIENT_TYPE =
     3.6  sig
     3.7 -  val add_quotient_type: ((string list * binding * mixfix) * (typ * term)) * thm
     3.8 +  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
     3.9      -> Proof.context -> (thm * thm) * local_theory
    3.10  
    3.11 -  val quotient_type: ((string list * binding * mixfix) * (typ * term)) list
    3.12 +  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
    3.13      -> Proof.context -> Proof.state
    3.14  
    3.15 -  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * string) list
    3.16 +  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list
    3.17      -> Proof.context -> Proof.state
    3.18  end;
    3.19  
    3.20 @@ -64,15 +64,15 @@
    3.21      |> map Free
    3.22  in
    3.23    lambda c (HOLogic.exists_const rty $
    3.24 -     lambda x (HOLogic.mk_eq (c, (rel $ x))))
    3.25 +     lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x))))))
    3.26  end
    3.27  
    3.28  
    3.29  (* makes the new type definitions and proves non-emptyness *)
    3.30 -fun typedef_make (vs, qty_name, mx, rel, rty) lthy =
    3.31 +fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
    3.32  let
    3.33    val typedef_tac =
    3.34 -    EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}])
    3.35 +    EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
    3.36  in
    3.37  (* FIXME: purely local typedef causes at the moment 
    3.38     problems with type variables
    3.39 @@ -93,14 +93,14 @@
    3.40  let
    3.41    val rep_thm = #Rep typedef_info RS mem_def1
    3.42    val rep_inv = #Rep_inverse typedef_info
    3.43 -  val abs_inv = mem_def2 RS #Abs_inverse typedef_info
    3.44 +  val abs_inv = #Abs_inverse typedef_info
    3.45    val rep_inj = #Rep_inject typedef_info
    3.46  in
    3.47    (rtac @{thm quot_type.intro} THEN' RANGE [
    3.48      rtac equiv_thm,
    3.49      rtac rep_thm,
    3.50      rtac rep_inv,
    3.51 -    EVERY' (map rtac [abs_inv, @{thm exI}, @{thm refl}]),
    3.52 +    rtac abs_inv THEN' rtac mem_def2 THEN' atac,
    3.53      rtac rep_inj]) 1
    3.54  end
    3.55  
    3.56 @@ -137,10 +137,12 @@
    3.57  
    3.58  
    3.59  (* main function for constructing a quotient type *)
    3.60 -fun add_quotient_type (((vs, qty_name, mx), (rty, rel)), equiv_thm) lthy =
    3.61 +fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
    3.62  let
    3.63 +  val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp}
    3.64 +
    3.65    (* generates the typedef *)
    3.66 -  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) lthy
    3.67 +  val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
    3.68  
    3.69    (* abs and rep functions from the typedef *)
    3.70    val Abs_ty = #abs_type (#1 typedef_info)
    3.71 @@ -162,7 +164,7 @@
    3.72    val ((rep, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
    3.73  
    3.74    (* quot_type theorem *)
    3.75 -  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, equiv_thm, typedef_info) lthy3
    3.76 +  val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
    3.77  
    3.78    (* quotient theorem *)
    3.79    val quotient_thm = typedef_quotient_thm (rel, abs, rep, abs_def, rep_def, quot_thm) lthy3
    3.80 @@ -179,12 +181,12 @@
    3.81  in
    3.82    lthy4
    3.83    |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
    3.84 -  ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add])
    3.85 +  ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
    3.86  end
    3.87  
    3.88  
    3.89  (* sanity checks for the quotient type specifications *)
    3.90 -fun sanity_check ((vs, qty_name, _), (rty, rel)) =
    3.91 +fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
    3.92  let
    3.93    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
    3.94    val rel_tfrees = map fst (Term.add_tfrees rel [])
    3.95 @@ -223,7 +225,7 @@
    3.96  end
    3.97  
    3.98  (* check for existence of map functions *)
    3.99 -fun map_check ctxt (_, (rty, _)) =
   3.100 +fun map_check ctxt (_, (rty, _, _)) =
   3.101  let
   3.102    val thy = ProofContext.theory_of ctxt
   3.103  
   3.104 @@ -263,11 +265,12 @@
   3.105    val _ = List.app sanity_check quot_list
   3.106    val _ = List.app (map_check lthy) quot_list
   3.107  
   3.108 -  fun mk_goal (rty, rel) =
   3.109 +  fun mk_goal (rty, rel, partial) =
   3.110    let
   3.111      val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   3.112 +    val const = if partial then @{const_name part_equivp} else @{const_name equivp}
   3.113    in
   3.114 -    HOLogic.mk_Trueprop (Const (@{const_name equivp}, equivp_ty) $ rel)
   3.115 +    HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
   3.116    end
   3.117  
   3.118    val goals = map (mk_goal o snd) quot_list
   3.119 @@ -280,7 +283,7 @@
   3.120  
   3.121  fun quotient_type_cmd specs lthy =
   3.122  let
   3.123 -  fun parse_spec ((((vs, qty_name), mx), rty_str), rel_str) lthy =
   3.124 +  fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
   3.125    let
   3.126      val rty = Syntax.read_typ lthy rty_str
   3.127      val lthy1 = Variable.declare_typ rty lthy
   3.128 @@ -290,7 +293,7 @@
   3.129        |> Syntax.check_term lthy1 
   3.130      val lthy2 = Variable.declare_term rel lthy1 
   3.131    in
   3.132 -    (((vs, qty_name, mx), (rty, rel)), lthy2)
   3.133 +    (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
   3.134    end
   3.135  
   3.136    val (spec', lthy') = fold_map parse_spec specs lthy
   3.137 @@ -298,11 +301,13 @@
   3.138    quotient_type spec' lthy'
   3.139  end
   3.140  
   3.141 +val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   3.142 +
   3.143  val quotspec_parser =
   3.144 -    Parse.and_list1
   3.145 -     ((Parse.type_args -- Parse.binding) --
   3.146 -        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   3.147 -         (Parse.$$$ "/" |-- Parse.term))
   3.148 +  Parse.and_list1
   3.149 +    ((Parse.type_args -- Parse.binding) --
   3.150 +      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   3.151 +        (Parse.$$$ "/" |-- (partial -- Parse.term)))
   3.152  
   3.153  val _ = Keyword.keyword "/"
   3.154