# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259263953 -3600
# Node ID 7ef153ded7e2e2077cb6dbff32e20bcea4f0e8ab
# Parent  fafcc54e531d030ba4a1f50b6d2ae7d20a9d9005
Merged

diff -r fafcc54e531d -r 7ef153ded7e2 FSet.thy
--- a/FSet.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/FSet.thy	Thu Nov 26 20:32:33 2009 +0100
@@ -341,9 +341,6 @@
 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *}
-ML {* val app_prs_thms = map (applic_prs_old @{context} rty qty absrep) aps *}
-
 lemma cheat: "P" sorry
 
 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
@@ -352,6 +349,7 @@
 prefer 2
 apply(rule cheat)
 apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms 1*})
+sorry
 
 quotient_def
   fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
@@ -407,7 +405,7 @@
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
-apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply (tactic {* regularize_tac @{context} [rel_eqv] rel_refl 1 *})
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})
 apply (rule FUN_QUOTIENT)
 apply (rule FUN_QUOTIENT)
diff -r fafcc54e531d -r 7ef153ded7e2 LFex.thy
--- a/LFex.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/LFex.thy	Thu Nov 26 20:32:33 2009 +0100
@@ -180,15 +180,6 @@
 where
   "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)"
 
-
-
-
-
-
-
-
-
-
 ML {* val defs =
   @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
     FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
@@ -197,78 +188,97 @@
 
 thm akind_aty_atrm.induct
 
+lemma left_ball_regular:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
+apply (rule LEFT_RES_FORALL_REGULAR)
+using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
+apply (simp)
+done
+
+lemma right_bex_regular:
+  assumes a: "EQUIV R"
+  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
+apply (rule RIGHT_RES_EXISTS_REGULAR)
+using Respects_def[of "R"] a EQUIV_REFL_SYM_TRANS[of "R"] REFL_def[of "R"]
+apply (simp)
+done
+
+lemma ball_respects_refl:
+  fixes P::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
+apply(rule iffI)
+apply(rule allI)
+apply(drule_tac x="\<lambda>y. f x" in bspec)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+apply(simp)
+apply(simp)
+done
+
 ML {*
-fun regularize_monos_tac lthy eqvs =
-  let 
-    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) eqvs
-    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) eqvs
+fun ball_simproc rel_eqvs ss redex =
+  let
+    val ctxt = Simplifier.the_context ss
+    val thy = ProofContext.theory_of ctxt
   in
-    REPEAT_ALL_NEW (FIRST' [
-      (rtac @{thm impI} THEN' atac),
-      (rtac @{thm my_equiv_res_forallR}),
-      (rtac @{thm my_equiv_res_forallL}),
-      (rtac @{thm Set.imp_mono}),
-      (resolve_tac (Inductive.get_monos lthy)),
-      (EqSubst.eqsubst_tac lthy [0] (subs1 @ subs2))
-    ])
+  case redex of
+      (ogl as ((Const (@{const_name "Ball"}, _)) $
+        ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ P1)) =>
+      (let
+        val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
+        val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
+        val _ = tracing (Syntax.string_of_term ctxt glc);
+        val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
+        val thm = (@{thm eq_reflection} OF [@{thm ball_respects_refl} OF [eqv]]);
+        val R1c = cterm_of @{theory} R1;
+        val thmi = Drule.instantiate' [] [SOME R1c] thm;
+        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));
+        val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
+        val _ = tracing "AAA";
+        val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
+        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
+      in
+        SOME thm2
+      end
+      handle _ => NONE
+
+      )
+  | _ => NONE
   end
 *}
 
 ML {*
-  val subs1 = map (fn x => @{thm eq_reflection} OF [@{thm equiv_res_forall} OF [x]]) @{thms alpha_EQUIVs}
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqvs rel_refls =
-  let 
-    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs
-    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs
+fun regularize_tac ctxt rel_eqvs =
+  let
+    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs;
+    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs;
+    val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2);
+    val pat = [@{term "Ball (Respects (R1 ===> R2)) P"}];
+    val thy = ProofContext.theory_of ctxt
+    val simproc = Simplifier.simproc_i thy "" pat (K (ball_simproc rel_eqvs))
   in
   (ObjectLogic.full_atomize_tac) THEN'
+  (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) 
+  THEN'
   REPEAT_ALL_NEW (FIRST' [
-    FIRST' (map rtac rel_refls),
-    atac,
-    rtac @{thm universal_twice},
-    rtac @{thm impI} THEN' atac,
-    rtac @{thm implication_twice},
-    EqSubst.eqsubst_tac ctxt [0] (subs1 @ subs2),
-    (* For a = b \<longrightarrow> a \<approx> b *)
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
+    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+    (rtac @{thm left_ball_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (rtac @{thm right_bex_regular} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (resolve_tac (Inductive.get_monos ctxt)),
+    rtac @{thm move_forall},
+    rtac @{thm move_exists}
   ])
   end
 *}
-thm RIGHT_RES_FORALL_REGULAR
-thm my_equiv_res_forallR
 
-(*
-lemma "\<And>i j xb\<Colon>trm \<Rightarrow> trm \<Rightarrow> bool. Respects (atrm ===> atrm ===> op =) xb \<Longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm\<in>Respects (atrm ===> atrm). xb (Const i) (m (Const j))) \<longrightarrow> (\<forall>m\<Colon>trm \<Rightarrow> trm. xb (Const i) (m (Const j)))"
-apply (simp add: Ball_def IN_RESPECTS Respects_def)
-apply (metis COMBK_def al_refl(3))
-*)
-
-lemma move_quant: "((\<forall>y. \<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>y. \<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
-by auto
-
-lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
-apply(auto)
-done
-
-lemma test: 
-  fixes P Q::"'a \<Rightarrow> bool"  
-  and x::"'a"
-  assumes a: "REFL R2"
-  and     b: "\<And>f. Q (f x) \<longrightarrow> P (f x)" 
-  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
-apply(rule impI)
-apply(rule allI)
-apply(drule_tac x="\<lambda>y. f x" in bspec)
-apply(simp add: Respects_def IN_RESPECTS)
-apply(rule impI)
-using a
-apply(simp add: REFL_def)
-using b
-apply(simp)
-done
 
 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K');
  \<And>A A' K x x' K'.
@@ -289,12 +299,15 @@
 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and>
    ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
+apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
+apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})
+
+apply(rule LEFT_RES_FORALL_REGULAR)
 apply(tactic {* (simp_tac ((Simplifier.context @{context} empty_ss) addsimps (subs1))) 1 *})
 apply(atomize (full))
 apply(rule RIGHT_RES_FORALL_REGULAR)
 apply(rule RIGHT_RES_FORALL_REGULAR)
 apply(rule RIGHT_RES_FORALL_REGULAR)
-apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
 apply(rule test)
 defer
 apply(tactic {* resolve_tac (Inductive.get_monos @{context}) 1 *})+
diff -r fafcc54e531d -r 7ef153ded7e2 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 26 19:51:31 2009 +0100
+++ b/QuotMain.thy	Thu Nov 26 20:32:33 2009 +0100
@@ -474,41 +474,6 @@
 
 *)
 
-lemma my_equiv_res_forallR:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes b: "(All Q) \<longrightarrow> (All P)"
-  shows "(All Q) \<longrightarrow> Ball (Respects E) P"
-using b by auto
-
-lemma my_equiv_res_forallL:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  assumes b: "(All Q) \<longrightarrow> (All P)"
-  shows "Ball (Respects E) P \<longrightarrow> (All P)"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsR:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes a: "EQUIV E"
-  and     b: "(Ex Q) \<longrightarrow> (Ex P)"
-  shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
-using a b
-unfolding EQUIV_def
-by (metis IN_RESPECTS)
-
-lemma my_equiv_res_existsL:
-  fixes P::"'a \<Rightarrow> bool"
-  fixes Q::"'b \<Rightarrow> bool"
-  assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
-  shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
-using b
-by (auto)
-
 lemma universal_twice:
   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
@@ -531,49 +496,15 @@
 in
   Seq.single thm
 end
- 
+
 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
 *}
 
 ML {*
-fun REGULARIZE_tac' lthy rel_refl rel_eqv =
-   (REPEAT1 o FIRST1) 
-     [(K (print_tac "start")) THEN' (K no_tac), 
-      DT lthy "1" (rtac rel_refl),
-      DT lthy "2" atac,
-      DT lthy "3" (rtac @{thm universal_twice}),
-      DT lthy "4" (rtac @{thm impI} THEN' atac),
-      DT lthy "5" (rtac @{thm implication_twice}),
-      DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
-      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
-      (* For a = b \<longrightarrow> a \<approx> b *)
-      DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-      DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
-*}
-
-ML {*
 fun regularize_tac ctxt rel_eqv rel_refl =
   (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST' [
-    rtac rel_refl,
-    atac,
-    rtac @{thm universal_twice},
-    rtac @{thm impI} THEN' atac,
-    rtac @{thm implication_twice},
-    EqSubst.eqsubst_tac ctxt [0]
-      [(@{thm equiv_res_forall} OF [rel_eqv]),
-       (@{thm equiv_res_exists} OF [rel_eqv])],
-    (* For a = b \<longrightarrow> a \<approx> b *)
-    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
-    (rtac @{thm RIGHT_RES_FORALL_REGULAR})
-  ]);
-*}
-
-ML {*
-fun regularize_tac ctxt rel_eqv rel_refl =
-  (ObjectLogic.full_atomize_tac) THEN'
-  REPEAT_ALL_NEW (FIRST' 
-   [(K (print_tac "start")) THEN' (K no_tac), 
+  REPEAT_ALL_NEW (FIRST'
+   [(K (print_tac "start")) THEN' (K no_tac),
     DT ctxt "1" (rtac rel_refl),
     DT ctxt "2" atac,
     DT ctxt "3" (rtac @{thm universal_twice}),
@@ -588,7 +519,89 @@
   ]);
 *}
 
-thm RIGHT_RES_FORALL_REGULAR
+lemma move_forall: "(\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)) \<Longrightarrow> ((\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y))"
+by auto
+
+lemma move_exists: "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
+by auto
+
+lemma [mono]: "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
+by blast
+
+lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
+by auto
+
+lemma ball_respects_refl:
+  fixes P Q::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  and     b: "\<And>f. Q (f x) \<longrightarrow> P (f x)"
+  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)) \<longrightarrow> All (\<lambda>f. P (f x)))"
+apply(rule impI)
+apply(rule allI)
+apply(drule_tac x="\<lambda>y. f x" in bspec)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+using b
+apply(simp)
+done
+
+lemma bex_respects_refl:
+  fixes P Q::"'a \<Rightarrow> bool"
+  and x::"'a"
+  assumes a: "EQUIV R2"
+  and     b: "\<And>f. P (f x) \<longrightarrow> Q (f x)"
+  shows   "(Ex (\<lambda>f. P (f x))) \<longrightarrow> (Bex (Respects (R1 ===> R2)) (\<lambda>f. Q (f x)))"
+apply(rule impI)
+apply(erule exE)
+thm bexI
+apply(rule_tac x="\<lambda>y. f x" in bexI)
+using b
+apply(simp)
+apply(simp add: Respects_def IN_RESPECTS)
+apply(rule impI)
+using a EQUIV_REFL_SYM_TRANS[of "R2"]
+apply(simp add: REFL_def)
+done
+
+(* FIXME: OPTION_EQUIV, PAIR_EQUIV, ... *)
+ML {*
+fun equiv_tac rel_eqvs =
+  REPEAT_ALL_NEW(FIRST' [
+    FIRST' (map rtac rel_eqvs),
+    rtac @{thm IDENTITY_EQUIV},
+    rtac @{thm LIST_EQUIV}
+  ])
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+fun regularize_tac ctxt rel_eqvs rel_refl =
+  let
+    val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs
+    val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs
+    val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2)
+  in
+  (ObjectLogic.full_atomize_tac) THEN'
+  (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
+  THEN'
+  REPEAT_ALL_NEW (FIRST' [
+    (rtac @{thm RIGHT_RES_FORALL_REGULAR}),
+    (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
+    (resolve_tac (Inductive.get_monos ctxt)),
+    (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
+    rtac @{thm move_forall},
+    rtac @{thm move_exists},
+    (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl)
+  ])
+  end
+*}
 
 section {* Injections of REP and ABSes *}
 
@@ -808,10 +821,6 @@
 *}
 
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
-ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (FIRST' [
     rtac trans_thm,
@@ -1285,7 +1294,7 @@
     in
       rtac rule THEN' RANGE [
         rtac rthm',
-        regularize_tac lthy rel_eqv rel_refl,
+        regularize_tac lthy [rel_eqv] rel_refl,
         REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
         clean_tac lthy quot defs reps_same absrep aps
       ]