# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255536796 -7200
# Node ID 8c3a35da45608ea241ff6943d6ffefcd950256ff
# Parent  ecfc2e1fd15e3fa5dac1c7ff3445e9f687dd0774
Proving the proper RepAbs version

diff -r ecfc2e1fd15e -r 8c3a35da4560 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 14 16:23:49 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 18:13:16 2009 +0200
@@ -325,7 +325,11 @@
 *}
 
 definition
-  "(x : p) \<Longrightarrow> (Babs p m x = m x)"
+  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+
+(* Babs p m = \<lambda>x. if x \<in> p then m x else undefined *)
 
 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where
   "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*)
@@ -1141,19 +1145,7 @@
   apply (tactic {* foo_tac' @{context} 1 *})
   done
 
-thm list.induct
-lemma list_induct2:
-  shows "(P []) \<Longrightarrow> (\<forall> a list. ((P list) \<longrightarrow> (P (a # list)))) \<Longrightarrow> \<forall>l :: 'a list. (P l)"
-  apply (rule allI)
-  apply (rule list.induct)
-  apply (assumption)
-  apply (auto)
-  done
-
-ML {* ObjectLogic.atomize (cprop_of @{thm list_induct2}) *}
-ML {* (atomize_thm @{thm list_induct2}) *}
-
-ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct2}) *}
+ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *)
 lemma RIGHT_RES_FORALL_REGULAR:
@@ -1339,6 +1331,9 @@
    = Ball (Respects ((op \<approx>) ===> (op =)))
      (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
      (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
+thm APPLY_RSP
+thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"]
+apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
 thm LAMBDA_PRS1[symmetric]
 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
diff -r ecfc2e1fd15e -r 8c3a35da4560 QuotScript.thy
--- a/QuotScript.thy	Wed Oct 14 16:23:49 2009 +0200
+++ b/QuotScript.thy	Wed Oct 14 18:13:16 2009 +0200
@@ -416,3 +416,4 @@
   using a by (metis EQUIV_def IN_RESPECTS a)
 
 end
+