524 

   524 (* Mention why equivalence *)

   525 

   526 text {*

   527 

   528   A user of our quotient package first needs to define an equivalence relation:

   529 

   530   @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}

   531 

   532   Then the user defines a quotient type:

   533 

   534   @{text "quotient_type int = (nat \<times> nat) / \<approx>"}

   535 

   536   Which leaves a proof obligation that the relation is an equivalence relation,

   537   that can be solved with the automatic tactic with two definitions.

   538 

   539   The user can then specify the constants on the quotient type:

   540 

   541   @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}

   542   @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}

   543   @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}

   544 

   545   Lets first take a simple theorem about addition on the raw level:

   546 

   547   @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}

   548 

   549   When the user tries to lift a theorem about integer addition, the respectfulness

   550   proof obligation is left, so let us prove it first:

   551   

   552   @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}

   553 

   554   Can be proved automatically by the system just by unfolding the definition

   555   of @{term "op \<Longrightarrow>"}.

   556 

   557   Now the user can either prove a lifted lemma explicitely:

   558 

   559   @{text "lemma 0 + i = i by lifting plus_zero_raw"}

   560 

   561   Or in this simple case use the automated translation mechanism:

   562 

   563   @{text "thm plus_zero_raw[quot_lifted]"}

   564 

   565   obtaining the same result.

   566 *}