# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256426103 -7200
# Node ID 6acf9e001038e670b0439473f3cf52eb2b76794a
# Parent  c7eff9882bd8236662f35ff608054c83e9042826
proved the two lemmas in QuotScript (reformulated them without leading forall)

diff -r c7eff9882bd8 -r 6acf9e001038 FSet.thy
--- a/FSet.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/FSet.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -590,7 +590,7 @@
 ML {* val ind_r_l3 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l2 *}
 ML {* val ind_r_l4 = eqsubst_thm @{context} @{thms app_prs_for_induct} ind_r_l3 *}
 ML {* val ind_r_a = simp_allex_prs @{context} ind_r_l4 *}
-ML {* val thm = @{thm spec[OF FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT]],symmetric]} *}
+ML {* val thm = @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT], symmetric]} *}
 ML {* val ind_r_a1 = eqsubst_thm @{context} [thm] ind_r_a *}
 ML {* val ind_r_d = MetaSimplifier.rewrite_rule fset_defs_sym ind_r_a1 *}
 ML {* val ind_r_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} ind_r_d *}
@@ -625,6 +625,7 @@
 (*notation ( output) "prop" ("#_" [1000] 1000) *)
 notation ( output) "Trueprop" ("#_" [1000] 1000)
 
+(*
 ML {*
   fun lift_theorem_fset_aux thm lthy =
     let
@@ -641,7 +642,9 @@
       nthm3
     end
 *}
+*)
 
+(*
 ML {* lift_theorem_fset_aux @{thm m1} @{context} *}
 ML {*
   fun lift_theorem_fset name thm lthy =
@@ -652,6 +655,7 @@
       lthy2
     end;
 *}
+*)
 
 (* These do not work without proper definitions to rewrite back *)
 local_setup {* lift_theorem_fset @{binding "m1_lift"} @{thm m1} *}
diff -r c7eff9882bd8 -r 6acf9e001038 Prove.thy
--- a/Prove.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/Prove.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -3,7 +3,7 @@
 begin
 
 ML {*
-val r = ref (NONE:(unit -> term) option)
+val r = Unsynchronized.ref (NONE:(unit -> term) option)
 *}
 
 ML {*
diff -r c7eff9882bd8 -r 6acf9e001038 QuotScript.thy
--- a/QuotScript.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/QuotScript.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -501,21 +501,25 @@
 *)
 lemma FORALL_PRS:
   assumes a: "QUOTIENT R absf repf"
-  shows "!f. All f = Ball (Respects R) ((absf ---> id) f)"
-  sorry
+  shows "All f = Ball (Respects R) ((absf ---> id) f)"
+  using a
+  unfolding QUOTIENT_def
+  by (metis IN_RESPECTS fun_map.simps id_apply)
 
 lemma EXISTS_PRS:
   assumes a: "QUOTIENT R absf repf"
-  shows "!f. Ex f = Bex (Respects R) ((absf ---> id) f)"
-  sorry
+  shows "Ex f = Bex (Respects R) ((absf ---> id) f)"
+  using a
+  unfolding QUOTIENT_def
+  by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def)
+   
+lemma ho_all_prs: 
+  shows "op = ===> op = ===> op = All All"
+  by auto
 
-lemma ho_all_prs: "op = ===> op = ===> op = All All"
-  apply (auto)
-  done
-
-lemma ho_ex_prs: "op = ===> op = ===> op = Ex Ex"
-  apply (auto)
-  done
+lemma ho_ex_prs: 
+  shows "op = ===> op = ===> op = Ex Ex"
+  by auto
 
 end