Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 583 7414f6cb5398
parent 582 a082e2d138ab
child 586 cdc6ae1a4ed2
equal deleted inserted replaced
582:a082e2d138ab 583:7414f6cb5398 
   501   REPEAT_ALL_NEW (FIRST' 
   501   REPEAT_ALL_NEW (FIRST' 
   502     [resolve_tac (equiv_rules_get ctxt)])
 
   502     [resolve_tac (equiv_rules_get ctxt)])
 
   503 *}
 
   503 *}
 
   504 
   504 
   505 ML {*
 
   505 ML {*
 
       
   506 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 
       
   507 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
       
   508 *}
 
       
   509 
       
   510 ML {*
 
   506 fun ball_reg_eqv_simproc ss redex =
 
   511 fun ball_reg_eqv_simproc ss redex =
 
   507   let
 
   512   let
 
   508     val ctxt = Simplifier.the_context ss
 
   513     val ctxt = Simplifier.the_context ss
 
   509     val thy = ProofContext.theory_of ctxt
 
   514     val thy = ProofContext.theory_of ctxt
 
   510   in
 
   515   in
 
   599       )
 
   604       )
 
   600   | _ => NONE
 
   605   | _ => NONE
 
   601   end
 
   606   end
 
   602 *}
 
   607 *}
 
   603 
   608 
   604 thm ball_reg_eqv_range
 
   609 
   605 thm bex_reg_eqv_range
 
   610 thm bex_reg_eqv_range
 
       
   611 thm ball_reg_eqv
 
       
   612 thm bex_reg_eqv
 
   606 
   613 
   607 ML {*
 
   614 ML {*
 
   608 fun bex_reg_eqv_range_simproc ss redex =
 
   615 fun bex_reg_eqv_range_simproc ss redex =
 
   609   let
 
   616   let
 
   610     val ctxt = Simplifier.the_context ss
 
   617     val ctxt = Simplifier.the_context ss
 
   636 *}
 
   643 *}
 
   637 
   644 
   638 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 
   645 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 
   639 by (simp add: equivp_reflp)
 
   646 by (simp add: equivp_reflp)
 
   640 
   647 
       
   648 (* does not work yet
 
   641 ML {*
 
   649 ML {*
 
   642 fun regularize_tac ctxt =
 
   650 fun regularize_tac ctxt =
 
   643   let
 
   651   let
 
   644     val pat1 = [@{term "Ball (Respects R) P"}];
 
   652     val pat1 = [@{term "Ball (Respects R) P"}];
 
   645     val pat2 = [@{term "Bex (Respects R) P"}];
 
   653     val pat2 = [@{term "Bex (Respects R) P"}];
 
   648     val thy = ProofContext.theory_of ctxt
 
   656     val thy = ProofContext.theory_of ctxt
 
   649     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
 
   657     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
 
   650     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
 
   658     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
 
   651     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
 
   659     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
 
   652     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
 
   660     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
 
   653     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
 
   661     val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
 
   654     (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
 
   662                                  addsimprocs [simproc3, simproc4]
 
       
   663                                  addSolver equiv_solver
 
       
   664     * TODO: Make sure that there are no list_rel, pair_rel etc involved *
 
   655     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 
   665     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 
   656   in
 
   666   in
 
   657   ObjectLogic.full_atomize_tac THEN'
 
   667   ObjectLogic.full_atomize_tac THEN'
 
   658   simp_tac simp_ctxt THEN'
 
   668   simp_tac simp_set THEN'
 
   659   REPEAT_ALL_NEW (FIRST' [
 
   669   REPEAT_ALL_NEW (FIRST' [
 
   660     rtac @{thm ball_reg_right},
 
   670     rtac @{thm ball_reg_right},
 
   661     rtac @{thm bex_reg_left},
 
   671     rtac @{thm bex_reg_left},
 
   662     resolve_tac (Inductive.get_monos ctxt),
 
   672     resolve_tac (Inductive.get_monos ctxt),
 
   663     rtac @{thm ball_all_comm},
 
   673     rtac @{thm ball_all_comm},
 
   664     rtac @{thm bex_ex_comm},
 
   674     rtac @{thm bex_ex_comm},
 
   665     resolve_tac eq_eqvs,
 
   675     resolve_tac eq_eqvs,
 
   666     simp_tac simp_ctxt
 
   676     simp_tac simp_set
 
   667   ])
 
   677   ])
 
   668   end
 
   678   end
 
       
   679 *}*)
 
       
   680 
       
   681 ML {*
 
       
   682 fun regularize_tac ctxt =
 
       
   683 let
 
       
   684   val pat1 = [@{term "Ball (Respects R) P"}];
 
       
   685   val pat2 = [@{term "Bex (Respects R) P"}];
 
       
   686   val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
 
       
   687   val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
 
       
   688   val thy = ProofContext.theory_of ctxt
 
       
   689   val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
 
       
   690   val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
 
       
   691   val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
 
       
   692   val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
 
       
   693   val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
 
       
   694   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
 
       
   695   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 
       
   696 in
 
       
   697   ObjectLogic.full_atomize_tac THEN'
 
       
   698   simp_tac simp_ctxt THEN'
 
       
   699   REPEAT_ALL_NEW (FIRST' [
 
       
   700      rtac @{thm ball_reg_right},
 
       
   701      rtac @{thm bex_reg_left},
 
       
   702      resolve_tac (Inductive.get_monos ctxt),
 
       
   703      rtac @{thm ball_all_comm},
 
       
   704      rtac @{thm bex_ex_comm},
 
       
   705      resolve_tac eq_eqvs,
 
       
   706      simp_tac simp_ctxt])
 
       
   707 end
 
   669 *}
 
   708 *}
 
   670 
   709 
   671 section {* Injections of rep and abses *}
 
   710 section {* Injections of rep and abses *}
 
   672 
   711 
   673 (*
 
   712 (*
nominal2