connect the Quotient package to the Lifting package
authorkuncar
Wed Apr 04 19:20:52 2012 +0200 (2012-04-04)
changeset 47362b1f099bdfbba
parent 47361 87c0eaf04bad
child 47365 7b09206bb74b
connect the Quotient package to the Lifting package
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Quotient.thy	Wed Apr 04 17:51:12 2012 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Wed Apr 04 19:20:52 2012 +0200
     1.3 @@ -772,6 +772,32 @@
     1.4  using assms
     1.5  by (rule OOO_quotient3) auto
     1.6  
     1.7 +subsection {* Quotient3 to Quotient *}
     1.8 +
     1.9 +lemma Quotient3_to_Quotient:
    1.10 +assumes "Quotient3 R Abs Rep"
    1.11 +and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
    1.12 +shows "Quotient R Abs Rep T"
    1.13 +using assms unfolding Quotient3_def by (intro QuotientI) blast+
    1.14 +
    1.15 +lemma Quotient3_to_Quotient_equivp:
    1.16 +assumes q: "Quotient3 R Abs Rep"
    1.17 +and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
    1.18 +and eR: "equivp R"
    1.19 +shows "Quotient R Abs Rep T"
    1.20 +proof (intro QuotientI)
    1.21 +  fix a
    1.22 +  show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
    1.23 +next
    1.24 +  fix a
    1.25 +  show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
    1.26 +next
    1.27 +  fix r s
    1.28 +  show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
    1.29 +next
    1.30 +  show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
    1.31 +qed
    1.32 +
    1.33  subsection {* ML setup *}
    1.34  
    1.35  text {* Auxiliary data for the quotient package *}
     2.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 04 17:51:12 2012 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Wed Apr 04 19:20:52 2012 +0200
     2.3 @@ -99,6 +99,54 @@
     2.4    else
     2.5      lthy
     2.6  
     2.7 +infix 0 MRSL
     2.8 +
     2.9 +fun ants MRSL thm = fold (fn rl => fn thm => rl RS thm) ants thm
    2.10 +
    2.11 +fun define_cr_rel equiv_thm abs_fun lthy =
    2.12 +  let
    2.13 +    fun force_type_of_rel rel forced_ty =
    2.14 +      let
    2.15 +        val thy = Proof_Context.theory_of lthy
    2.16 +        val rel_ty = (domain_type o fastype_of) rel
    2.17 +        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
    2.18 +      in
    2.19 +        Envir.subst_term_types ty_inst rel
    2.20 +      end
    2.21 +  
    2.22 +    val (rty, qty) = (dest_funT o fastype_of) abs_fun
    2.23 +    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
    2.24 +    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
    2.25 +      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
    2.26 +      | Const (@{const_name part_equivp}, _) $ rel => 
    2.27 +        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
    2.28 +      | _ => error "unsupported equivalence theorem"
    2.29 +      )
    2.30 +    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
    2.31 +    val qty_name = (fst o dest_Type) qty
    2.32 +    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
    2.33 +    val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
    2.34 +    val ((_, (_ , def_thm)), lthy'') =
    2.35 +      Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
    2.36 +  in
    2.37 +    (def_thm, lthy'')
    2.38 +  end;
    2.39 +
    2.40 +fun setup_lifting_package quot3_thm equiv_thm lthy =
    2.41 +  let
    2.42 +    val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
    2.43 +    val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
    2.44 +    val quot_thm = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
    2.45 +      Const (@{const_name equivp}, _) $ _ => 
    2.46 +        [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp}
    2.47 +      | Const (@{const_name part_equivp}, _) $ _ => 
    2.48 +        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient}
    2.49 +      | _ => error "unsupported equivalence theorem"
    2.50 +      )
    2.51 +  in
    2.52 +    Lifting_Setup.setup_lifting_infr quot_thm equiv_thm lthy'
    2.53 +  end
    2.54 +
    2.55  fun init_quotient_infr quot_thm equiv_thm lthy =
    2.56    let
    2.57      val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
    2.58 @@ -115,6 +163,7 @@
    2.59          (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
    2.60            #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
    2.61        |> define_abs_type quot_thm
    2.62 +      |> setup_lifting_package quot_thm equiv_thm
    2.63    end
    2.64  
    2.65  (* main function for constructing a quotient type *)