# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255595123 -7200
# Node ID 4da7147046114f8c2b6972508450b1381557abc8
# Parent  8c3a35da45608ea241ff6943d6ffefcd950256ff
A number of lemmas for REGULARIZE_TAC and regularizing card1.

diff -r 8c3a35da4560 -r 4da714704611 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 14 18:13:16 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 10:25:23 2009 +0200
@@ -427,7 +427,7 @@
         val rec_term = regularise t' rty rel lthy2;
         val lam_term = Term.lambda_name (x, v) rec_term
       in
-        Const(@{const_name "All"}, at) $ lam_term
+        Const(@{const_name "Ex"}, at) $ lam_term
       end
   | ((Const (@{const_name "Ex"}, at)) $ P) =>
       let
@@ -1147,21 +1147,6 @@
 
 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:
-  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
-  shows "All P ==> Ball R Q"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
-
-lemma LEFT_RES_FORALL_REGULAR:
-  assumes a: "!x. (R x \<and> (Q x --> P x))"
-  shows "Ball R Q ==> All P"
-  using a
-  apply (metis COMBC_def Collect_def Collect_mem_eq a)
-  done
-
 prove {*
  Logic.mk_implies
    ((prop_of li),
@@ -1177,6 +1162,19 @@
   apply (assumption)
   done
 
+ML {* val li = Thm.freezeT (atomize_thm @{thm card1_suc}) *}
+
+prove card1_suc_r: {*
+ Logic.mk_implies
+   ((prop_of li),
+   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+  apply (simp only: equiv_res_forall[OF equiv_list_eq])
+  apply (simp only: equiv_res_exists[OF equiv_list_eq])
+  done
+
+thm card1_suc
+ML {* @{thm card1_suc_r} OF [li] *}
+
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}
@@ -1234,8 +1232,9 @@
 local_setup {* lift_theorem_fset @{binding "leqi4_lift"} @{thm list_eq.intros(4)} *}
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
-(*ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} @{context}) *}
-local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
+thm card1_suc_r
+ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}
+(*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm m1_lift
 thm leqi4_lift
diff -r 8c3a35da4560 -r 4da714704611 QuotScript.thy
--- a/QuotScript.thy	Wed Oct 14 18:13:16 2009 +0200
+++ b/QuotScript.thy	Thu Oct 15 10:25:23 2009 +0200
@@ -403,6 +403,9 @@
 using a1 a2 unfolding o_def expand_fun_eq
 by (auto)
 
+
+(* TODO: Put the following lemmas in proper places *)
+
 lemma equiv_res_forall:
   fixes P :: "'a \<Rightarrow> bool"
   assumes a: "EQUIV E"
@@ -415,5 +418,53 @@
   shows "Bex (Respects E) P = (Ex P)"
   using a by (metis EQUIV_def IN_RESPECTS a)
 
+lemma FORALL_REGULAR:
+  assumes a: "!x :: 'a. (P x --> Q x)"
+  and     b: "All P"
+  shows "All Q"
+  using a b by (metis)
+
+lemma EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (P x --> Q x)"
+  and     b: "Ex P"
+  shows "Ex Q"
+  using a b by (metis)
+
+lemma RES_FORALL_REGULAR:
+  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  and     b: "Ball R P"
+  shows "Ball R Q"
+  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma RES_EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  and     b: "Bex R P"
+  shows "Bex R Q"
+  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma LEFT_RES_FORALL_REGULAR:
+  assumes a: "!x. (R x \<and> (Q x --> P x))"
+  shows "Ball R Q ==> All P"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
+lemma RIGHT_RES_FORALL_REGULAR:
+  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
+  shows "All P ==> Ball R Q"
+  using a
+  apply (metis COMBC_def Collect_def Collect_mem_eq a)
+  done
+
+lemma LEFT_RES_EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (R x --> Q x --> P x)"
+  shows "Bex R Q ==> Ex P"
+  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
+lemma RIGHT_RES_EXISTS_REGULAR:
+  assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))"
+  shows "Ex P \<Longrightarrow> Bex R Q"
+  using a by (metis COMBC_def Collect_def Collect_mem_eq)
+
 end