diff -r bd602eb894ab -r c9633254a4ec Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Fri Feb 03 15:51:55 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Thu Feb 09 14:47:24 2012 +0100
@@ -37,7 +37,7 @@
   concat_fset ("\<Union>") and
   Quotient ("Quot _ _ _")
 
-
+declare [[show_question_marks = false]]
 
 ML {*
 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
@@ -58,43 +58,6 @@
   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 
-lemma insert_preserve2:
-  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
-         (id ---> rep_fset ---> abs_fset) op #"
-  by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
-
-lemma list_all2_symp:
-  assumes a: "equivp R"
-  and b: "list_all2 R xs ys"
-  shows "list_all2 R ys xs"
-using list_all2_lengthD[OF b] b
-apply(induct xs ys rule: list_induct2)
-apply(auto intro: equivp_symp[OF a])
-done
-
-lemma concat_rsp_unfolded:
-  "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)"
-proof -
-  fix a b ba bb
-  assume a: "list_all2 list_eq a ba"
-  assume b: "list_eq ba bb"
-  assume c: "list_all2 list_eq bb b"
-  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
-    fix x
-    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof
-      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
-      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
-    next
-      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
-      have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a])
-      have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b])
-      have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c])
-      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
-    qed
-  qed
-  then show "list_eq (concat a) (concat b)" by auto
-qed
-
 (*>*)
 
 
@@ -275,7 +238,7 @@
 
   \begin{isabelle}\ \ \ \ \ %%%
   @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm}
-  @{thm concat.simps(2)[THEN eq_reflection, no_vars]}
+  @{thm concat.simps(2)[THEN eq_reflection]}
   \end{isabelle}
 
   \noindent
@@ -285,8 +248,8 @@
   builds finite unions of finite sets:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm}
-  @{thm concat_insert_fset[THEN eq_reflection, no_vars]}
+  @{thm concat_empty_fset[THEN eq_reflection]}\hspace{10mm}
+  @{thm concat_insert_fset[THEN eq_reflection]}
   \end{isabelle}
 
   \noindent
@@ -325,7 +288,7 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}}
+  {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}}
 
   In addition we are able to clearly specify what is involved
   in the lifting process (this was only hinted at in \cite{Homeier05} and
@@ -383,7 +346,7 @@
   also the following map for function types
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm map_fun_def[no_vars, THEN eq_reflection]}
+  @{thm map_fun_def[THEN eq_reflection]}
   \end{isabelle}
 
   \noindent
@@ -423,7 +386,7 @@
   relations over function types
   %
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]}
+  @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", THEN eq_reflection]}
   \hfill\numbered{relfun}
   \end{isabelle}
 
@@ -449,9 +412,9 @@
   holds if and only if
   \begin{isabelle}\ \ \ \ \ %%%%
   \begin{tabular}{rl}
-  (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\
-  (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\
-  (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\
+  (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R"]}\end{isa}\\
+  (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R"]}\end{isa}\\
+  (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R"]}\end{isa}\\
   \end{tabular}
   \end{isabelle}
   \end{definition}
@@ -918,7 +881,7 @@
   with @{text "nat \<times> nat"} and we also quotient this type to yield integers,
   then we need to show this preservation property.
 
-  %%%@ {thm [display, indent=10] insert_preserve2[no_vars]}
+  %%%@ {thm [display, indent=10] Cons_prs2}
 
   %Given two quotients, one of which quotients a container, and the
   %other quotients the type in the container, we can write the
@@ -1132,7 +1095,7 @@
 %%% should include a proof sketch?
 
   %\begin{isabelle}\ \ \ \ \ %%%
-  %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]}
+  %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2]}
   %\end{isabelle}
 
   %\noindent
@@ -1183,7 +1146,7 @@
   %@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have:
 
   %\begin{isabelle}\ \ \ \ \ %%%
-  %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]}
+  %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2"]}
   %\end{isabelle}
 
   %\noindent
@@ -1192,7 +1155,7 @@
   %which has been shown by Homeier~\cite{Homeier05}:
 
   %\begin{isabelle}\ \ \ \ \ %%%
-  %@{thm (concl) Quotient_rel_rep[no_vars]}
+  %@{thm (concl) Quotient_rel_rep}
   %\end{isabelle}