# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259752074 -3600
# Node ID 7f97c52021c98f256255711cc9c25f160db6b2e2
# Parent  7fbbb2690bc585a8640eb71fd89560a058e87adb
Fixed unlam for non-abstractions and updated list_induct_part proof.

diff -r 7fbbb2690bc5 -r 7f97c52021c9 FSet.thy
--- a/FSet.thy	Wed Dec 02 11:30:40 2009 +0100
+++ b/FSet.thy	Wed Dec 02 12:07:54 2009 +0100
@@ -344,7 +344,6 @@
 lemma cheat: "P" sorry
 
 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
-ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] *}
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
@@ -352,49 +351,49 @@
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* D *) (* reflexivity of basic relations *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) 
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
 done
 
 quotient_def
@@ -459,14 +458,13 @@
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
 apply (rule IDENTITY_QUOTIENT)
+prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
+prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
-apply (rule IDENTITY_QUOTIENT)
-apply (rule IDENTITY_QUOTIENT)
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
@@ -482,6 +480,8 @@
 apply (rule FUN_QUOTIENT)
 apply (rule QUOTIENT_fset)
 apply (rule IDENTITY_QUOTIENT)
+prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
+prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
@@ -500,21 +500,39 @@
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
+prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply assumption
 apply (rule refl)
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply assumption
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
+prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
+apply assumption
+apply (rule refl)
 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
-apply (tactic {* instantiate_tac @{thm APPLY_RSP2} @{context} 1 *})
-apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP} @{context} THEN' (RANGE [quotient_tac [quot]])) 1 *})
+apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *})
+apply (rule IDENTITY_QUOTIENT)
+apply (rule FUN_QUOTIENT)
+apply (rule QUOTIENT_fset)
+apply (rule IDENTITY_QUOTIENT)
+prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*})
+prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*})
+apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *})
diff -r 7fbbb2690bc5 -r 7f97c52021c9 QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 11:30:40 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 12:07:54 2009 +0100
@@ -774,7 +774,7 @@
   Subgoal.FOCUS (fn {concl, ...} =>
   let
     val pat = Drule.strip_imp_concl (cprop_of thm)
-    val insts = Thm.match (pat, concl)
+    val insts = Thm.first_order_match (pat, concl)
   in
     rtac (Drule.instantiate insts thm) 1
   end
@@ -865,7 +865,7 @@
           let
             val (asmf, asma) = find_qt_asm (map term_of asms);
             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-            val insts = Thm.match (pat, concl)
+            val insts = Thm.first_order_match (pat, concl)
           in
             if (fastype_of asmf) = (fastype_of f)
             then no_tac
@@ -951,7 +951,12 @@
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
-ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
+(* TODO: Can this be done easier? *)
+ML {*
+fun unlam t =
+  case t of
+    (Abs a) => snd (Term.dest_abs a)
+  | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
 
 ML {*
 fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =