src/HOL/Quotient.thy
 changeset 35294 0e1adc24722f parent 35236 fd8231b16203 child 35827 f552152d7747
```--- a/src/HOL/Quotient.thy	Mon Feb 22 21:47:21 2010 -0800
+++ b/src/HOL/Quotient.thy	Mon Feb 22 21:48:20 2010 -0800
@@ -2,6 +2,8 @@
Author:     Cezary Kaliszyk and Christian Urban
*)

+header {* Definition of Quotient Types *}
+
theory Quotient
uses
@@ -80,7 +82,7 @@
shows "((op =) OOO R) = R"

-section {* Respects predicate *}
+subsection {* Respects predicate *}

definition
Respects
@@ -92,7 +94,7 @@
unfolding mem_def Respects_def
by simp

-section {* Function map and function relation *}
+subsection {* Function map and function relation *}

definition
fun_map (infixr "--->" 55)
@@ -124,7 +126,7 @@
using a by auto

-section {* Quotient Predicate *}
+subsection {* Quotient Predicate *}

definition
"Quotient E Abs Rep \<equiv>
@@ -285,7 +287,7 @@
shows "R2 (f x) (g y)"
using a by simp

-section {* lemmas for regularisation of ball and bex *}
+subsection {* lemmas for regularisation of ball and bex *}

lemma ball_reg_eqv:
fixes P :: "'a \<Rightarrow> bool"
@@ -387,7 +389,7 @@
shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
using assms by auto

-section {* Bounded abstraction *}
+subsection {* Bounded abstraction *}

definition
Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
@@ -465,7 +467,7 @@
using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
by metis

-section {* @{text Bex1_rel} quantifier *}
+subsection {* @{text Bex1_rel} quantifier *}

definition
Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
@@ -569,7 +571,7 @@
apply auto
done

-section {* Various respects and preserve lemmas *}
+subsection {* Various respects and preserve lemmas *}

lemma quot_rel_rsp:
assumes a: "Quotient R Abs Rep"
@@ -706,7 +708,7 @@

end

-section {* ML setup *}
+subsection {* ML setup *}

text {* Auxiliary data for the quotient package *}

@@ -762,7 +764,7 @@
text {* Tactics for proving the lifted theorems *}
use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"

-section {* Methods / Interface *}
+subsection {* Methods / Interface *}

method_setup lifting =
{* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}```