nominal2: comparison Quotient-Paper/Paper.thy

equal deleted inserted replaced

-:ea7c3f21d6df
+:b0b2198040d7
+(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
 (*<*)
 theory Paper
 imports "Quotient"
 "LaTeXsugar"
 "../Nominal/FSet"
 begin
+print_syntax
 notation (latex output)
 rel_conj ("_ OOO _" [53, 53] 52)
 and
-fun_map ("_ ---> _" [51, 51] 50)
+"op -->" (infix "\<rightarrow>" 100)
 and
-fun_rel ("_ ===> _" [51, 51] 50)
+"==>" (infix "\<Rightarrow>" 100)
+and
+fun_map (infix "\<longrightarrow>" 51)
+and
+fun_rel (infix "\<Longrightarrow>" 51)
 and
 list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
 \begin{itemize}
 \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
 \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
 \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
 \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
-\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+\item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
-\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) ---> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
+\item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
 \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
 \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
 \end{itemize}
 Apart from the last 2 points the definition is same as the one implemented in
-in Homeier's HOL package, below is the definition of @{term fconcat}
+in Homeier's HOL package. Adding composition in last two cases is necessary
-that shows the last points:
+for compositional quotients. We ilustrate the different behaviour of the
+definition by showing the derived definition of @{term fconcat}:
 @{thm fconcat_def[no_vars]}
 The aggregate @{term Abs} function takes a finite set of finite sets
 and applies @{term "map rep_fset"} composed with @{term rep_fset} to
 can be stated as:
 @{thm [display] append_rsp[no_vars]}
 \noindent
-Which after unfolding @{term "op ===>"} is equivalent to:
+Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
 @{thm [display] append_rsp_unfolded[no_vars]}
 An aggregate relation is defined in terms of relation composition,
 so we define it first:
 implementation.
 We first define the statement of the regularized theorem based
 on the original theorem and the goal theorem. Then we define
 the statement of the injected theorem, based on the regularized
-theorem and the goal. We then show the 3 proofs as all three
+theorem and the goal. We then show the 3 proofs, as all three
 can be performed independently from each other.
 *}
 subsection {* Regularization and Injection statements *}
 For existential quantifiers and unique existential quantifiers it is
 defined similarily to the universal one.
 *}
-subsection {* Proof of Regularization *}
+subsection {* Proof procedure *}
-text {*
+(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
-Example of non-regularizable theorem ($0 = 1$).
+present in a paper a version with typed-variables it is not necessary *)
+text {*
+With the above definitions of @{text "REG"} and @{text "INJ"} we can show
+how the proof is performed. The first step is always the application of
+of the following lemma:
+@{term "[|A; A --> B; B = C; C = D|] ==> D"}
+With @{text A} instantiated to the original raw theorem,
+@{text B} instantiated to @{text "REG(A)"},
+@{text C} instantiated to @{text "INJ(REG(A))"},
+and @{text D} instantiated to the statement of the lifted theorem.
+The first assumption can be immediately discharged using the original
+theorem and the three left subgoals are exactly the subgoals of regularization,
+injection and cleaning. The three can be proved independently by the
+framework and in case there are non-solved subgoals they can be left
+to the user.
+The injection and cleaning subgoals are always solved if the appropriate
+respectfulness and preservation theorems are given. It is not the case
+with regularization; sometimes a theorem given by the user does not
+imply a regularized version and a stronger one needs to be proved. This
+is outside of the scope of the quotient package, so the user is then left
+with such obligations. As an example lets see the simplest possible
+non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
+on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
+only shows that particular items in the equivalence classes are not equal,
+a more general statement saying that the classes are not equal is necessary.
+*}
+subsection {* Proving Regularization *}
+text {*
+Isabelle provides
 Separtion of regularization from injection thanks to the following 2 lemmas:
 \begin{lemma}
 If @{term R2} is an equivalence relation, then:

changeset 2208	b0b2198040d7
parent 2207	ea7c3f21d6df
child 2209	5952b0f28261