diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Quotient.thy --- a/src/HOL/Quotient.thy Sat Jul 18 21:44:18 2015 +0200 +++ b/src/HOL/Quotient.thy Sat Jul 18 22:58:50 2015 +0200 @@ -2,7 +2,7 @@ Author: Cezary Kaliszyk and Christian Urban *) -section {* Definition of Quotient Types *} +section \Definition of Quotient Types\ theory Quotient imports Lifting @@ -12,12 +12,12 @@ "quotient_definition" :: thy_goal begin -text {* +text \ Basic definition for equivalence relations that are represented by predicates. -*} +\ -text {* Composition of Relations *} +text \Composition of Relations\ abbreviation rel_conj :: "('a \ 'b \ bool) \ ('b \ 'a \ bool) \ 'a \ 'b \ bool" (infixr "OOO" 75) @@ -32,7 +32,7 @@ begin interpretation lifting_syntax . -subsection {* Quotient Predicate *} +subsection \Quotient Predicate\ definition "Quotient3 R Abs Rep \ @@ -64,7 +64,7 @@ by blast lemma Quotient3_rel: - "R r r \ R s s \ Abs r = Abs s \ R r s" -- {* orientation does not loop on rewriting *} + "R r r \ R s s \ Abs r = Abs s \ R r s" -- \orientation does not loop on rewriting\ using a unfolding Quotient3_def by blast @@ -192,12 +192,12 @@ using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] by simp -text{* +text\ In the following theorem R1 can be instantiated with anything, but we know some of the types of the Rep and Abs functions; so by solving Quotient assumptions we can get a unique R1 that will be provable; which is why we need to use @{text apply_rsp} and - not the primed version *} + not the primed version\ lemma apply_rspQ3: fixes f g::"'a \ 'c" @@ -215,7 +215,7 @@ then show ?thesis using assms(2) by (auto intro: apply_rsp') qed -subsection {* lemmas for regularisation of ball and bex *} +subsection \lemmas for regularisation of ball and bex\ lemma ball_reg_eqv: fixes P :: "'a \ bool" @@ -315,7 +315,7 @@ shows "(\x. \y. A x y) \ (\x\P. \y. B x y)" using assms by auto -subsection {* Bounded abstraction *} +subsection \Bounded abstraction\ definition Babs :: "'a set \ ('a \ 'b) \ 'a \ 'b" @@ -392,7 +392,7 @@ using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def by metis -subsection {* @{text Bex1_rel} quantifier *} +subsection \@{text Bex1_rel} quantifier\ definition Bex1_rel :: "('a \ 'a \ bool) \ ('a \ bool) \ bool" @@ -506,7 +506,7 @@ apply simp done -subsection {* Various respects and preserve lemmas *} +subsection \Various respects and preserve lemmas\ lemma quot_rel_rsp: assumes a: "Quotient3 R Abs Rep" @@ -605,7 +605,7 @@ have "R (SOME x. x \ Rep a) x" using r rep some_collect by metis then have "R x (SOME x. x \ Rep a)" using part_equivp_symp[OF equivp] by fast then show "R (SOME x. x \ Rep a) (SOME x. x \ Rep a)" - using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \ Rep a) x`) + using part_equivp_transp[OF equivp] by (metis \R (SOME x. x \ Rep a) x\) qed have "Collect (R (SOME x. x \ Rep a)) = (Rep a)" by (metis some_collect rep_prop) then show "Abs (Collect (R (SOME x. x \ Rep a))) = a" using rep_inverse by auto @@ -624,7 +624,7 @@ end -subsection {* Quotient composition *} +subsection \Quotient composition\ lemma OOO_quotient3: fixes R1 :: "'a \ 'a \ bool" @@ -718,7 +718,7 @@ using assms by (rule OOO_quotient3) auto -subsection {* Quotient3 to Quotient *} +subsection \Quotient3 to Quotient\ lemma Quotient3_to_Quotient: assumes "Quotient3 R Abs Rep" @@ -744,9 +744,9 @@ show "T = (\x y. R x x \ Abs x = y)" using T_def equivp_reflp[OF eR] by simp qed -subsection {* ML setup *} +subsection \ML setup\ -text {* Auxiliary data for the quotient package *} +text \Auxiliary data for the quotient package\ named_theorems quot_equiv "equivalence relation theorems" and quot_respect "respectfulness theorems" @@ -763,7 +763,7 @@ lemmas [quot_equiv] = identity_equivp -text {* Lemmas about simplifying id's. *} +text \Lemmas about simplifying id's.\ lemmas [id_simps] = id_def[symmetric] map_fun_id @@ -773,22 +773,22 @@ eq_comp_r vimage_id -text {* Translation functions for the lifting process. *} +text \Translation functions for the lifting process.\ ML_file "Tools/Quotient/quotient_term.ML" -text {* Definitions of the quotient types. *} +text \Definitions of the quotient types.\ ML_file "Tools/Quotient/quotient_type.ML" -text {* Definitions for quotient constants. *} +text \Definitions for quotient constants.\ ML_file "Tools/Quotient/quotient_def.ML" -text {* +text \ An auxiliary constant for recording some information about the lifted theorem in a tactic. -*} +\ definition Quot_True :: "'a \ bool" where @@ -809,55 +809,55 @@ begin interpretation lifting_syntax . -text {* Tactics for proving the lifted theorems *} +text \Tactics for proving the lifted theorems\ ML_file "Tools/Quotient/quotient_tacs.ML" end -subsection {* Methods / Interface *} +subsection \Methods / Interface\ method_setup lifting = - {* Attrib.thms >> (fn thms => fn ctxt => - SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *} - {* lift theorems to quotient types *} + \Attrib.thms >> (fn thms => fn ctxt => + SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\ + \lift theorems to quotient types\ method_setup lifting_setup = - {* Attrib.thm >> (fn thm => fn ctxt => - SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *} - {* set up the three goals for the quotient lifting procedure *} + \Attrib.thm >> (fn thm => fn ctxt => + SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\ + \set up the three goals for the quotient lifting procedure\ method_setup descending = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *} - {* decend theorems to the raw level *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\ + \decend theorems to the raw level\ method_setup descending_setup = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *} - {* set up the three goals for the decending theorems *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\ + \set up the three goals for the decending theorems\ method_setup partiality_descending = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *} - {* decend theorems to the raw level *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\ + \decend theorems to the raw level\ method_setup partiality_descending_setup = - {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *} - {* set up the three goals for the decending theorems *} + \Scan.succeed (fn ctxt => + SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\ + \set up the three goals for the decending theorems\ method_setup regularize = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *} - {* prove the regularization goals from the quotient lifting procedure *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\ + \prove the regularization goals from the quotient lifting procedure\ method_setup injection = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *} - {* prove the rep/abs injection goals from the quotient lifting procedure *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\ + \prove the rep/abs injection goals from the quotient lifting procedure\ method_setup cleaning = - {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *} - {* prove the cleaning goals from the quotient lifting procedure *} + \Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\ + \prove the cleaning goals from the quotient lifting procedure\ attribute_setup quot_lifted = - {* Scan.succeed Quotient_Tacs.lifted_attrib *} - {* lift theorems to quotient types *} + \Scan.succeed Quotient_Tacs.lifted_attrib\ + \lift theorems to quotient types\ no_notation rel_conj (infixr "OOO" 75)