# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260078112 -3600
# Node ID 06e54c862a390afd36e481cf803b33e526792a68
# Parent  14682786c3564f20104c3a7b6fd4c2d933f2321d# Parent  a68c51dd85b3de96f429cd3935b4ac1bc58c1287
merge

diff -r 14682786c356 -r 06e54c862a39 IntEx.thy
--- a/IntEx.thy	Sun Dec 06 06:39:32 2009 +0100
+++ b/IntEx.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -147,12 +147,37 @@
 apply(rule refl)
 done
 
-abbreviation 
-  "Abs \<equiv> ABS_my_int"
-abbreviation 
-  "Rep \<equiv> REP_my_int"
-abbreviation 
-  "Resp \<equiv> Respects"
+
+(*
+lemma yy:
+  "(REP_my_int ---> id)
+ (\<lambda>x. Ball (Respects op \<approx>)
+       ((ABS_my_int ---> id)
+         ((REP_my_int ---> id)
+           (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
+                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)) \<approx>
+                (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+                 ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus)
+                 (REP_my_int (ABS_my_int x)) (REP_my_int (ABS_my_int b)))))) =
+(\<lambda>x. Ball (Respects op \<approx>)
+     ((ABS_my_int ---> id)
+       ((REP_my_int ---> id)
+         (\<lambda>b. (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
+               (REP_my_int (ABS_my_int b)) \<approx>
+              (ABS_my_int ---> ABS_my_int ---> REP_my_int)
+               ((REP_my_int ---> REP_my_int ---> ABS_my_int) my_plus) (REP_my_int x)
+               (REP_my_int (ABS_my_int b))))))"
+apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [lambda_prs2 @{theory}]) 1*})
+
+apply(rule lambda_prs)
+apply(tactic {* quotient_tac @{context} 1 *})
+apply(simp add: id_simps)
+apply(tactic {* quotient_tac @{context} 1 *})
+done
+*)
+
 
 
 lemma "PLUS a b = PLUS a b"
diff -r 14682786c356 -r 06e54c862a39 IntEx2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IntEx2.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -0,0 +1,460 @@
+theory IntEx2
+imports QuotMain
+uses
+  ("Tools/numeral.ML")
+  ("Tools/numeral_syntax.ML")
+  ("Tools/int_arith.ML")
+begin
+
+fun
+  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+  "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient int = "nat \<times> nat" / intrel
+  apply(unfold equivp_def)
+  apply(auto simp add: mem_def expand_fun_eq)
+  done
+
+instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}"
+begin
+
+quotient_def 
+  zero_qnt::"int"
+where
+  "zero_qnt \<equiv> (0::nat, 0::nat)"
+
+definition  Zero_int_def[code del]: 
+  "0 = zero_qnt"
+
+quotient_def 
+  one_qnt::"int"
+where
+  "one_qnt \<equiv> (1::nat, 0::nat)"
+
+definition One_int_def[code del]:
+  "1 = one_qnt"
+
+fun
+  plus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "plus_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_def 
+  plus_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+  "plus_qnt \<equiv> plus_raw"
+
+definition add_int_def[code del]:
+  "z + w = plus_qnt z w"
+
+fun
+  minus_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "minus_raw (x, y) = (y, x)"
+
+quotient_def 
+  minus_qnt::"int \<Rightarrow> int"
+where
+  "minus_qnt \<equiv> minus_raw"
+
+definition minus_int_def [code del]:
+    "- z = minus_qnt z"
+
+definition
+  diff_int_def [code del]:  "z - w = z + (-w::int)"
+
+fun
+  mult_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_def 
+  mult_qnt::"int \<Rightarrow> int \<Rightarrow> int"
+where
+  "mult_qnt \<equiv> mult_raw"
+
+definition
+  mult_int_def [code del]: "z * w = mult_qnt z w"
+
+fun
+  le_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+  "le_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_def 
+  le_qnt :: "int \<Rightarrow> int \<Rightarrow> bool"
+where
+  "le_qnt \<equiv> le_raw"
+
+definition
+  le_int_def [code del]:
+   "z \<le> w = le_qnt z w"
+
+definition
+  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+  zsgn_def: "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+
+instance ..
+
+end
+
+thm add_assoc
+
+lemma plus_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_raw plus_raw"
+by auto
+
+lemma mult_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) mult_raw mult_raw"
+apply(auto)
+apply(simp add: mult algebra_simps)
+sorry
+
+lemma le_raw_rsp[quotient_rsp]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) le_raw le_raw"
+by auto
+
+lemma plus_assoc_raw:
+  shows "plus_raw (plus_raw i j) k \<approx> plus_raw i (plus_raw j k)"
+by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+  shows "plus_raw i j \<approx> plus_raw j i"
+by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+  shows "plus_raw  (0, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+  shows "plus_raw (minus_raw i) i \<approx> (0, 0)"
+by (cases i) (simp)
+
+lemma mult_assoc_raw:
+  shows "mult_raw (mult_raw i j) k \<approx> mult_raw i (mult_raw j k)"
+by (cases i, cases j, cases k) 
+   (simp add: mult algebra_simps)
+
+lemma mult_sym_raw:
+  shows "mult_raw i j \<approx> mult_raw j i"
+by (cases i, cases j) (simp)
+
+lemma mult_one_raw:
+  shows "mult_raw  (1, 0) i \<approx> i"
+by (cases i) (simp)
+
+lemma mult_plus_comm_raw:
+  shows "mult_raw (plus_raw i j) k \<approx> plus_raw (mult_raw i k) (mult_raw j k)"
+by (cases i, cases j, cases k) 
+   (simp add: mult algebra_simps)
+
+lemma one_zero_distinct:
+  shows "(0, 0) \<noteq> ((1::nat), (0::nat))"
+  by simp
+  
+text{*The integers form a @{text comm_ring_1}*}
+
+
+ML {* val qty = @{typ "int"} *}
+ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
+ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
+
+instance int :: comm_ring_1
+proof
+  fix i j k :: int
+  show "(i + j) + k = i + (j + k)"
+    unfolding add_int_def
+    apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i + j = j + i" 
+    unfolding add_int_def
+    apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "0 + i = (i::int)"
+    unfolding add_int_def Zero_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm plus_zero_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "- i + i = 0"
+    unfolding add_int_def minus_int_def Zero_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm plus_minus_zero_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "i - j = i + - j"
+    by (simp add: diff_int_def)
+  show "(i * j) * k = i * (j * k)"
+    unfolding mult_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm mult_assoc_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "i * j = j * i"
+    unfolding mult_int_def 
+    apply(tactic {* procedure_tac @{context} @{thm mult_sym_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "1 * i = i"
+    unfolding mult_int_def One_int_def
+    apply(tactic {* procedure_tac @{context} @{thm mult_one_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "(i + j) * k = i * k + j * k"
+    unfolding mult_int_def add_int_def
+    apply(tactic {* procedure_tac @{context} @{thm mult_plus_comm_raw} 1 *})
+    apply(tactic {* regularize_tac @{context} [@{thm int_equivp}] 1 *})
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "0 \<noteq> (1::int)"
+    unfolding Zero_int_def One_int_def
+    apply(tactic {* procedure_tac @{context} @{thm one_zero_distinct} 1 *})
+    defer
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+qed
+
+term of_nat
+thm of_nat_def
+
+lemma int_def: "of_nat m = ABS_int (m, 0)"
+apply(induct m) 
+apply(simp add: Zero_int_def zero_qnt_def)
+apply(simp)
+apply(simp add: add_int_def One_int_def)
+apply(simp add: plus_qnt_def one_qnt_def)
+oops
+
+lemma le_antisym_raw:
+  shows "le_raw i j \<Longrightarrow> le_raw j i \<Longrightarrow> i \<approx> j"
+by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+  shows "le_raw i i"
+by (cases i) (simp)
+
+lemma le_trans_raw:
+  shows "le_raw i j \<Longrightarrow> le_raw j k \<Longrightarrow> le_raw i k"
+by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+  shows "le_raw i j \<or> le_raw j i"
+by (cases i, cases j) 
+   (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+  fix i j k :: int
+  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+    by (auto simp add: less_int_def dest: antisym) 
+  show "i \<le> i"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_refl_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_trans_raw} [@{thm int_equivp}] 1 *})
+    done
+  show "i \<le> j \<or> j \<le> i"
+    unfolding le_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_cases_raw} [@{thm int_equivp}] 1 *})
+    done
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+  by intro_classes
+    (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_raw:
+  shows "le_raw i j \<Longrightarrow> le_raw (plus_raw k i) (plus_raw k j)"
+by (cases i, cases j, cases k) (simp)
+
+
+instance int :: pordered_cancel_ab_semigroup_add
+proof
+  fix i j k :: int
+  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+    unfolding le_int_def add_int_def
+    apply(tactic {* lift_tac @{context} @{thm le_plus_raw} [@{thm int_equivp}] 1 *})
+    done
+qed
+
+lemma test:
+  "\<lbrakk>le_raw i j \<and> i \<noteq> j; le_raw (0, 0) k \<and> (0, 0) \<noteq> k\<rbrakk>
+    \<Longrightarrow> le_raw (mult_raw k i) (mult_raw k j) \<and> mult_raw k i \<noteq> mult_raw k j"
+apply(cases i, cases j, cases k)
+apply(auto simp add: mult algebra_simps)
+sorry
+
+
+text{*The integers form an ordered integral domain*}
+instance int :: ordered_idom
+proof
+  fix i j k :: int
+  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+    unfolding mult_int_def le_int_def less_int_def Zero_int_def
+    apply(tactic {* procedure_tac @{context} @{thm test} 1 *})
+    defer
+    apply(tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+    defer
+    apply(tactic {* clean_tac @{context} 1*})
+    sorry
+  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+    by (simp only: zabs_def)
+  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+    by (simp only: zsgn_def)
+qed
+
+instance int :: lordered_ring
+proof  
+  fix k :: int
+  show "abs k = sup k (- k)"
+    by (auto simp add: sup_int_def zabs_def less_minus_self_iff [symmetric])
+qed
+
+lemmas int_distrib =
+  left_distrib [of "z1::int" "z2" "w", standard]
+  right_distrib [of "w::int" "z1" "z2", standard]
+  left_diff_distrib [of "z1::int" "z2" "w", standard]
+  right_diff_distrib [of "w::int" "z1" "z2", standard]
+
+
+subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
+
+(*
+context ring_1
+begin
+
+ 
+definition 
+  of_int :: "int \<Rightarrow> 'a" 
+where
+  "of_int 
+*)
+
+
+subsection {* Binary representation *}
+
+text {*
+  This formalization defines binary arithmetic in terms of the integers
+  rather than using a datatype. This avoids multiple representations (leading
+  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
+  int_of_binary}, for the numerical interpretation.
+
+  The representation expects that @{text "(m mod 2)"} is 0 or 1,
+  even if m is negative;
+  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+  @{text "-5 = (-3)*2 + 1"}.
+  
+  This two's complement binary representation derives from the paper 
+  "An Efficient Representation of Arithmetic for Term Rewriting" by
+  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
+  Springer LNCS 488 (240-251), 1991.
+*}
+
+subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}
+
+definition
+  Pls :: int where
+  [code del]: "Pls = 0"
+
+definition
+  Min :: int where
+  [code del]: "Min = - 1"
+
+definition
+  Bit0 :: "int \<Rightarrow> int" where
+  [code del]: "Bit0 k = k + k"
+
+definition
+  Bit1 :: "int \<Rightarrow> int" where
+  [code del]: "Bit1 k = 1 + k + k"
+
+class number = -- {* for numeric types: nat, int, real, \dots *}
+  fixes number_of :: "int \<Rightarrow> 'a"
+
+use "~~/src/HOL/Tools/numeral.ML"
+
+syntax
+  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
+
+use "~~/src/HOL/Tools/numeral_syntax.ML"
+setup NumeralSyntax.setup
+
+abbreviation
+  "Numeral0 \<equiv> number_of Pls"
+
+abbreviation
+  "Numeral1 \<equiv> number_of (Bit1 Pls)"
+
+lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
+  -- {* Unfold all @{text let}s involving constants *}
+  unfolding Let_def ..
+
+definition
+  succ :: "int \<Rightarrow> int" where
+  [code del]: "succ k = k + 1"
+
+definition
+  pred :: "int \<Rightarrow> int" where
+  [code del]: "pred k = k - 1"
+
+lemmas
+  max_number_of [simp] = max_def
+    [of "number_of u" "number_of v", standard, simp]
+and
+  min_number_of [simp] = min_def 
+    [of "number_of u" "number_of v", standard, simp]
+  -- {* unfolding @{text minx} and @{text max} on numerals *}
+
+lemmas numeral_simps = 
+  succ_def pred_def Pls_def Min_def Bit0_def Bit1_def
+
+text {* Removal of leading zeroes *}
+
+lemma Bit0_Pls [simp, code_post]:
+  "Bit0 Pls = Pls"
+  unfolding numeral_simps by simp
+
+lemma Bit1_Min [simp, code_post]:
+  "Bit1 Min = Min"
+  unfolding numeral_simps by simp
+
+lemmas normalize_bin_simps =
+  Bit0_Pls Bit1_Min
diff -r 14682786c356 -r 06e54c862a39 LamEx.thy
--- a/LamEx.thy	Sun Dec 06 06:39:32 2009 +0100
+++ b/LamEx.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -80,6 +80,35 @@
 where
   "fv \<equiv> rfv"
 
+ML {*
+local
+   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
+   fun pp_list xs = Pretty.list "[" "]" xs
+   fun pp_str s   = Pretty.str s
+   fun pp_qstr s = Pretty.quote (pp_str s)
+   fun pp_int i   = pp_str (string_of_int i)
+   fun pp_sort S = pp_list (map pp_qstr S)
+   fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
+in
+fun raw_pp_typ (TVar ((a, i), S)) =
+       pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
+   | raw_pp_typ (TFree (a, S)) =
+       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
+   | raw_pp_typ (Type (a, tys)) =
+       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
+end *}
+
+ML {*
+PolyML.addPrettyPrinter
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)
+
+*}
+
+typ "name set" 
+typ "name => bool"
+
+ML {* @{typ "name set"} *}
+
 thm fv_def
 
 (* definition of overloaded permutation function *)
diff -r 14682786c356 -r 06e54c862a39 QuotMain.thy
--- a/QuotMain.thy	Sun Dec 06 06:39:32 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 06:41:52 2009 +0100
@@ -740,12 +740,17 @@
         then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
-  | (Const (_, T), Const (_, T')) =>
-        if T = T'                    
+  | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+    (* FIXME: check here that rtrm is the corresponding definition for teh const *)
+  | (_, Const (_, T')) =>
+      let
+        val rty = fastype_of rtrm
+      in 
+        if rty = T'                    
         then rtrm
-        else mk_repabs lthy (T, T') rtrm
-  
-  | (_, Const (@{const_name "op ="}, _)) => rtrm
+        else mk_repabs lthy (rty, T') rtrm
+      end   
   
   | _ => raise (LIFT_MATCH "injection")
 *}
@@ -773,6 +778,12 @@
      resolve_tac (quotient_rules_get ctxt)])
 *}
 
+(* solver for the simplifier *)
+ML {*
+fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
+val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
+*}
+
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -1041,92 +1052,77 @@
 *}
 
 ML {*
-fun lambda_allex_prs_simple_conv ctxt ctrm =
+fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
-    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
-    let
-      val (ty_b, ty_a) = dest_fun_type (fastype_of r1);
-      val (ty_c, ty_d) = dest_fun_type (fastype_of a2);
-      val thy = ProofContext.theory_of ctxt;
-      val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
-      val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
-      val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs};
-      val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
-      val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
-      val tl = Thm.lhs_of ts;
-      val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
-      val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
-    in
-      Conv.rewr_conv ti ctrm
-    end
+   ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
+     let
+       val thy = ProofContext.theory_of ctxt
+       val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
+       val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+       val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
+       val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
+       val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
+       val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
+       val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+       val tl = Thm.lhs_of ts
+       val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
+       val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
+        (*val _ = tracing "lambda_prs"
+          val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
+          val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
+     in
+       Conv.rewr_conv ti ctrm
+     end
   | _ => Conv.all_conv ctrm
 *}
 
 ML {*
-val lambda_allex_prs_conv =
-  More_Conv.top_conv lambda_allex_prs_simple_conv
+val lambda_prs_conv =
+  More_Conv.top_conv lambda_prs_simple_conv
 
-fun lambda_allex_prs_tac ctxt = CONVERSION (lambda_allex_prs_conv ctxt)
+fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
 (*
- Cleaning the theorem consists of 6 kinds of rewrites.
+ Cleaning the theorem consists of three rewriting steps.
  The first two need to be done before fun_map is unfolded
 
- - lambda_prs:
+ 1) lambda_prs:
      (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f
 
- - all_prs (and the same for exists: ex_prs)
-     \<forall>x\<in>Respects R. (abs ---> id) f  ---->  \<forall>x. f
-
- - Rewriting with definitions from the argument defs
-     NewConst  ---->  (rep ---> abs) oldConst
+    Implemented as conversion since it is not a pattern.
 
- - Quotient_rel_rep:
-     Rel (Rep x) (Rep y)  ---->  x = y
+ 2) all_prs (the same for exists):
+     Ball (Respects R) ((abs ---> id) f)  ---->  All f
 
- - ABS_REP
-     Abs (Rep x)  ---->  x
+    Rewriting with definitions from the argument defs
+     (rep ---> abs) oldConst ----> newconst
 
- - id_simps; fun_map.simps
+ 3) Quotient_rel_rep:
+      Rel (Rep x) (Rep y)  ---->  x = y
 
- The first one is implemented as a conversion (fast).
- The second one is an EqSubst (slow).
- The rest are a simp_tac and are fast.
+    Quotient_abs_rep:
+      Abs (Rep x)  ---->  x
+
+    id_simps; fun_map.simps
 *)
 
 ML {*
-fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
-val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
-*}
-
-ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
+      (* FIXME: shouldn't the definitions already be varified? *)
     val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
-    fun simp_ctxt thms = HOL_basic_ss addsimps thms addSolver quotient_solver
-    (* FIXME: use of someting smaller than HOL_basic_ss *)
+    fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
+      (* FIXME: use of someting smaller than HOL_basic_ss *)
   in
-    EVERY' [
-      (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x)))  ---->  f *)
-      NDT lthy "a" (TRY o lambda_allex_prs_tac lthy),
-
-      (* Ball (Respects R) ((abs ---> id) f)  ---->  All f *)
-      NDT lthy "b" (simp_tac (simp_ctxt thms1)),
-
-      (* NewConst  ----->  (rep ---> abs) oldConst *)
-      (* abs (rep x)  ----->  x                    *)
-      (* R (Rep x) (Rep y) -----> x = y            *)
-      (* id_simps; fun_map.simps                   *)
-      NDT lthy "c" (simp_tac (simp_ctxt thms2)),
-
-      (* final step *)
-      NDT lthy "d" (TRY o rtac refl)
-    ]
+    EVERY' [lambda_prs_tac lthy,
+            simp_tac (simps thms1),
+            simp_tac (simps thms2),
+            TRY o rtac refl]
   end
 *}