# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259432052 -3600
# Node ID 24fa145fc2e325c61090a273659dd5390c9d63c5
# Parent  3e7ee6f5437d1dd8c9cd723a4bf2ff2564823238
improved pattern matching inside the inj_repabs_tacs

diff -r 3e7ee6f5437d -r 24fa145fc2e3 FSet.thy
--- a/FSet.thy	Sat Nov 28 18:49:39 2009 +0100
+++ b/FSet.thy	Sat Nov 28 19:14:12 2009 +0100
@@ -398,7 +398,6 @@
 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
 done
 
-
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
diff -r 3e7ee6f5437d -r 24fa145fc2e3 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 18:49:39 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 19:14:12 2009 +0100
@@ -178,7 +178,6 @@
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
-
 section {* ATOMIZE *}
 
 lemma atomize_eqv[atomize]:
@@ -771,28 +770,11 @@
 *}
 
 section {* RepAbs Injection Tactic *}
-(*
-To prove that the regularised theorem implies the abs/rep injected, we first
-atomize it and then try:
 
- 1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides (LAMBDA_RES_TAC)
- 3) remove Ball/Bex from the right hand side
- 4) use user-supplied RSP theorems
- 5) remove rep_abs from the right side
- 6) reflexivity of equality
- 7) split applications of lifted type (apply_rsp)
- 8) split applications of non-lifted type (cong_tac)
- 9) apply extentionality
-10) reflexivity of the relation
-11) assumption
-    (Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
-    (not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfullness
-
-*)
+ML {*
+fun stripped_term_of ct =
+  ct |> term_of |> HOLogic.dest_Trueprop
+*}
 
 ML {*
 fun instantiate_tac thm = 
@@ -826,43 +808,42 @@
 ML {*
 val lambda_res_tac =
   Subgoal.FOCUS (fn {concl, ...} =>
-    case (term_of concl) of
-       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
+    case (stripped_term_of concl) of
+       (_ $ (Abs _) $ (Abs _)) => rtac @{thm FUN_REL_I} 1
      | _ => no_tac)
 *}
 
 ML {*
 val weak_lambda_res_tac =
   Subgoal.FOCUS (fn {concl, ...} =>
-    case (term_of concl) of
-       (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
-     | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1
+    case (stripped_term_of concl) of
+       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1
+     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1
      | _ => no_tac)
 *}
 
 ML {*
 val ball_rsp_tac = 
   Subgoal.FOCUS (fn {concl, ...} =>
-     case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) 
-                $ (Const (@{const_name Ball}, _) $ _))) => rtac @{thm FUN_REL_I} 1
+     case (stripped_term_of concl) of
+        (_ $ (Const (@{const_name Ball}, _) $ _) 
+           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1
       |_ => no_tac)
 *}
 
 ML {*
 val bex_rsp_tac = 
   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-     case (term_of concl) of
-        (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) 
-                $ (Const (@{const_name Bex}, _) $ _))) => rtac @{thm FUN_REL_I} 1
+     case (stripped_term_of concl) of
+        (_ $ (Const (@{const_name Bex}, _) $ _) 
+           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1
       | _ => no_tac)
 *}
 
 ML {* (* Legacy *)
 fun needs_lift (rty as Type (rty_s, _)) ty =
   case ty of
-    Type (s, tys) =>
-      (s = rty_s) orelse (exists (needs_lift rty) tys)
+    Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys)
   | _ => false
 
 *}
@@ -870,8 +851,8 @@
 ML {*
 fun APPLY_RSP_TAC rty = 
   Subgoal.FOCUS (fn {concl, ...} =>
-    case (term_of concl) of
-       (_ $ (R $ (f $ _) $ (_ $ _))) =>
+    case (stripped_term_of concl) of
+       (_ $ (f $ _) $ (_ $ _)) =>
           let
             val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
             val insts = Thm.match (pat, concl)
@@ -921,10 +902,10 @@
     NDT ctxt "2" (lambda_res_tac ctxt),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 
     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
-    DT ctxt "4" (ball_rsp_tac ctxt),
+    NDT ctxt "4" (ball_rsp_tac ctxt),
 
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
@@ -964,7 +945,7 @@
     
     (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    NDT ctxt "G" (weak_lambda_res_tac ctxt),
+    (*NDT ctxt "G" (weak_lambda_res_tac ctxt),*)
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)