QuotMain.thy
changeset 390 1dd6a21cdd1c
parent 388 aa452130ae7f
child 391 58947b7232ef
equal deleted inserted replaced
388:aa452130ae7f 390:1dd6a21cdd1c
   472  - Ball (Respects ?E) ?P = All ?P
   472  - Ball (Respects ?E) ?P = All ?P
   473  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
   473  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
   474 
   474 
   475 *)
   475 *)
   476 
   476 
   477 lemma my_equiv_res_forall2:
   477 lemma my_equiv_res_forallR:
   478   fixes P::"'a \<Rightarrow> bool"
   478   fixes P::"'a \<Rightarrow> bool"
   479   fixes Q::"'b \<Rightarrow> bool"
   479   fixes Q::"'b \<Rightarrow> bool"
   480   assumes a: "(All Q) \<longrightarrow> (All P)"
   480   assumes b: "(All Q) \<longrightarrow> (All P)"
   481   shows "(All Q) \<longrightarrow> Ball (Respects E) P"
   481   shows "(All Q) \<longrightarrow> Ball (Respects E) P"
   482 using a by auto
   482 using b by auto
   483 
   483 
   484 lemma my_equiv_res_exists:
   484 lemma my_equiv_res_forallL:
       
   485   fixes P::"'a \<Rightarrow> bool"
       
   486   fixes Q::"'b \<Rightarrow> bool"
       
   487   assumes a: "EQUIV E"
       
   488   assumes b: "(All Q) \<longrightarrow> (All P)"
       
   489   shows "Ball (Respects E) P \<longrightarrow> (All P)"
       
   490 using a b
       
   491 unfolding EQUIV_def
       
   492 by (metis IN_RESPECTS)
       
   493 
       
   494 lemma my_equiv_res_existsR:
   485   fixes P::"'a \<Rightarrow> bool"
   495   fixes P::"'a \<Rightarrow> bool"
   486   fixes Q::"'b \<Rightarrow> bool"
   496   fixes Q::"'b \<Rightarrow> bool"
   487   assumes a: "EQUIV E"
   497   assumes a: "EQUIV E"
   488   and     b: "(Ex Q) \<longrightarrow> (Ex P)"
   498   and     b: "(Ex Q) \<longrightarrow> (Ex P)"
   489   shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
   499   shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
   490 apply(subst equiv_res_exists)
   500 using a b
   491 apply(rule a)
   501 unfolding EQUIV_def
   492 apply(rule b)
   502 by (metis IN_RESPECTS)
   493 done
   503 
       
   504 lemma my_equiv_res_existsL:
       
   505   fixes P::"'a \<Rightarrow> bool"
       
   506   fixes Q::"'b \<Rightarrow> bool"
       
   507   assumes b: "(Ex Q) \<longrightarrow> (Ex P)"
       
   508   shows "Bex (Respects E) Q \<longrightarrow> (Ex P)"
       
   509 using b
       
   510 by (auto)
   494 
   511 
   495 lemma universal_twice:
   512 lemma universal_twice:
   496   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
   513   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
   497   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
   514   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
   498 using * by auto
   515 using * by auto
   499 
   516 
   500 lemma implication_twice:
   517 lemma implication_twice:
   501   assumes a: "c \<longrightarrow> a"
   518   assumes a: "c \<longrightarrow> a"
   502   assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
   519   assumes b: "b \<longrightarrow> d"
   503   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
   520   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
   504 using a b by auto
   521 using a b by auto
   505 
       
   506 ML {*
       
   507 (* FIXME: get_rid of rel_refl rel_eqv *)
       
   508 fun REGULARIZE_tac lthy rel_refl rel_eqv =
       
   509    (REPEAT1 o FIRST1) 
       
   510      [rtac rel_refl,
       
   511       atac,
       
   512       rtac @{thm universal_twice},
       
   513       rtac @{thm impI} THEN' atac,
       
   514       rtac @{thm implication_twice},
       
   515       rtac @{thm my_equiv_res_forall2},
       
   516       rtac (rel_eqv RS @{thm my_equiv_res_exists}),
       
   517       (* For a = b \<longrightarrow> a \<approx> b *)
       
   518       rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
       
   519       rtac @{thm RIGHT_RES_FORALL_REGULAR}]
       
   520 *}
       
   521 
   522 
   522 (* version of REGULARIZE_tac including debugging information *)
   523 (* version of REGULARIZE_tac including debugging information *)
   523 ML {*
   524 ML {*
   524 fun my_print_tac ctxt s thm =
   525 fun my_print_tac ctxt s thm =
   525 let
   526 let
   541       DT lthy "1" (rtac rel_refl),
   542       DT lthy "1" (rtac rel_refl),
   542       DT lthy "2" atac,
   543       DT lthy "2" atac,
   543       DT lthy "3" (rtac @{thm universal_twice}),
   544       DT lthy "3" (rtac @{thm universal_twice}),
   544       DT lthy "4" (rtac @{thm impI} THEN' atac),
   545       DT lthy "4" (rtac @{thm impI} THEN' atac),
   545       DT lthy "5" (rtac @{thm implication_twice}),
   546       DT lthy "5" (rtac @{thm implication_twice}),
   546       DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
   547       DT lthy "6" (rtac @{thm my_equiv_res_forallR}),
   547       DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
   548       DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})),
   548       (* For a = b \<longrightarrow> a \<approx> b *)
   549       (* For a = b \<longrightarrow> a \<approx> b *)
   549       DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
   550       DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
   550       DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
   551       DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
   551 *}
   552 *}
   552 
   553 
   555   (ObjectLogic.full_atomize_tac) THEN'
   556   (ObjectLogic.full_atomize_tac) THEN'
   556   REPEAT_ALL_NEW (FIRST' [
   557   REPEAT_ALL_NEW (FIRST' [
   557     rtac rel_refl,
   558     rtac rel_refl,
   558     atac,
   559     atac,
   559     rtac @{thm universal_twice},
   560     rtac @{thm universal_twice},
   560     (rtac @{thm impI} THEN' atac),
   561     rtac @{thm impI} THEN' atac,
   561     rtac @{thm implication_twice},
   562     rtac @{thm implication_twice},
   562     EqSubst.eqsubst_tac ctxt [0]
   563     EqSubst.eqsubst_tac ctxt [0]
   563       [(@{thm equiv_res_forall} OF [rel_eqv]),
   564       [(@{thm equiv_res_forall} OF [rel_eqv]),
   564        (@{thm equiv_res_exists} OF [rel_eqv])],
   565        (@{thm equiv_res_exists} OF [rel_eqv])],
   565     (* For a = b \<longrightarrow> a \<approx> b *)
   566     (* For a = b \<longrightarrow> a \<approx> b *)
   566     (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
   567     (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
   567     (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   568     (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   568   ]);
   569   ]);
   569 *}
   570 *}
   570 
   571 
       
   572 ML {*
       
   573 fun regularize_tac ctxt rel_eqv rel_refl =
       
   574   (ObjectLogic.full_atomize_tac) THEN'
       
   575   REPEAT_ALL_NEW (FIRST' 
       
   576    [(K (print_tac "start")) THEN' (K no_tac), 
       
   577     DT ctxt "1" (rtac rel_refl),
       
   578     DT ctxt "2" atac,
       
   579     DT ctxt "3" (rtac @{thm universal_twice}),
       
   580     DT ctxt "4" (rtac @{thm impI} THEN' atac),
       
   581     DT ctxt "5" (rtac @{thm implication_twice}),
       
   582     DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
       
   583       [(@{thm equiv_res_forall} OF [rel_eqv]),
       
   584        (@{thm equiv_res_exists} OF [rel_eqv])]),
       
   585     (* For a = b \<longrightarrow> a \<approx> b *)
       
   586     DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
       
   587     DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR})
       
   588   ]);
       
   589 *}
       
   590 
       
   591 thm RIGHT_RES_FORALL_REGULAR
       
   592 
       
   593 section {* Injections of REP and ABSes *}
   571 
   594 
   572 (*
   595 (*
   573 Injections of REP and Abses
       
   574 ***************************
       
   575 
       
   576 Injecting REPABS means:
   596 Injecting REPABS means:
   577 
   597 
   578   For abstractions:
   598   For abstractions:
   579   * If the type of the abstraction doesn't need lifting we recurse.
   599   * If the type of the abstraction doesn't need lifting we recurse.
   580   * If it does we add RepAbs around the whole term and check if the
   600   * If it does we add RepAbs around the whole term and check if the