--- a/IntEx.thy	Thu Dec 03 14:02:05 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 15:03:31 2009 +0100
@@ -13,6 +13,8 @@
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
+thm quotient_thm
+
 thm my_int_equiv
 
 print_theorems
@@ -129,7 +131,7 @@
   apply(auto)
   done
 
-lemma ho_plus_rsp[quot_rsp]:
+lemma ho_plus_rsp[quotient_rsp]:
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
@@ -139,17 +141,17 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] *}
 
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
 
 
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
 apply(tactic {* inj_repabs_tac_intex @{context} 1*})
@@ -187,7 +189,7 @@
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"
@@ -234,12 +236,12 @@
   apply (induct t)
 by (simp_all add: QUOTIENT_ABS_REP[OF a])
 
-lemma cons_rsp[quot_rsp]:
+lemma cons_rsp[quotient_rsp]:
   "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
 by simp
 
 (* I believe it's true. *)
-lemma foldl_rsp[quot_rsp]:
+lemma foldl_rsp[quotient_rsp]:
   "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
 apply (simp only: FUN_REL.simps)
 apply (rule allI)
@@ -254,37 +256,17 @@
 apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
-lemma nil_listrel_rsp[quot_rsp]:
+lemma nil_listrel_rsp[quotient_rsp]:
   "(LIST_REL R) [] []"
 by simp
 
-thm LAMBDA_PRS[no_vars]
-thm all_prs[no_vars]
-
-lemma test_all_prs:
-  "\<lbrakk>QUOTIENT R absf repf; f = g\<rbrakk> \<Longrightarrow> Ball (Respects R) ((absf ---> id) f) = All g"
-apply(drule all_prs)
-apply(simp)
-done
-
-lemma test:
-  "\<lbrakk>QUOTIENT R1 Abs1 Rep1; QUOTIENT R2 Abs2 Rep2; 
-    (\<lambda>x. Rep2 (f (Abs1 x))) = lhs \<rbrakk> \<Longrightarrow> (Rep1 ---> Abs2) lhs = f"
-apply -
-thm LAMBDA_PRS
-apply(drule LAMBDA_PRS)
-apply(assumption)
-apply(auto)
-done
-
-
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 done
 
 lemma ho_tst2: "foldl my_plus x (h # t) \<approx> my_plus h (foldl my_plus x t)"
@@ -296,6 +278,6 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: cons_prs[OF QUOTIENT_my_int])
-apply(tactic {* clean_tac @{context} [quot] 1 *})
+apply(tactic {* clean_tac @{context} 1 *})
 done