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 432 9c33c0809733
parent 427 5a3965aa4d80
child 433 1c245f6911dd
equal deleted inserted replaced
427:5a3965aa4d80 432:9c33c0809733 
   486  - Ball (Respects ?E) ?P = All ?P
 
   486  - Ball (Respects ?E) ?P = All ?P
 
   487  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
   487  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
   488 
   488 
   489 *)
 
   489 *)
 
   490 
   490 
   491 lemma universal_twice:
 
       
   492   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
 
       
   493   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
 
       
   494 using * by auto
 
       
   495 
       
   496 lemma implication_twice:
 
       
   497   assumes a: "c \<longrightarrow> a"
 
       
   498   assumes b: "b \<longrightarrow> d"
 
       
   499   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
       
   500 using a b by auto
 
       
   501 
       
   502 (* version of regularize_tac including debugging information *)
 
       
   503 ML {*
 
       
   504 fun regularize_tac ctxt rel_eqv rel_refl =
 
       
   505   (ObjectLogic.full_atomize_tac) THEN'
 
       
   506   REPEAT_ALL_NEW (FIRST'
 
       
   507    [(K (print_tac "start")) THEN' (K no_tac),
 
       
   508     DT ctxt "1" (resolve_tac rel_refl),
 
       
   509     DT ctxt "2" atac,
 
       
   510     DT ctxt "3" (rtac @{thm universal_twice}),
 
       
   511     DT ctxt "4" (rtac @{thm impI} THEN' atac),
 
       
   512     DT ctxt "5" (rtac @{thm implication_twice}),
 
       
   513     DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0]
 
       
   514       [(@{thm ball_reg_eqv} OF [rel_eqv]),
 
       
   515        (@{thm ball_reg_eqv} OF [rel_eqv])]),
 
       
   516     (* For a = b \<longrightarrow> a \<approx> b *)
 
       
   517     DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl)),
 
       
   518     DT ctxt "8" (rtac @{thm ball_reg_right})
 
       
   519   ]);
 
       
   520 *}
 
       
   521 
       
   522 lemma move_forall: 
       
   523   "(\<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))"
 
       
   524 by auto
 
       
   525 
       
   526 lemma move_exists: 
       
   527   "((\<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))"
 
       
   528 by auto
 
       
   529 
       
   530 lemma [mono]: 
   491 lemma [mono]: 
   531   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 
   492   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 
   532 by blast
 
   493 by blast
 
   533 
   494 
   534 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 
   495 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 
   542      rtac @{thm IDENTITY_EQUIV},
 
   503      rtac @{thm IDENTITY_EQUIV},
 
   543      rtac @{thm LIST_EQUIV}])
 
   504      rtac @{thm LIST_EQUIV}])
 
   544 *}
 
   505 *}
 
   545 
   506 
   546 ML {*
 
   507 ML {*
 
   547 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 
   508 fun ball_reg_eqv_simproc rel_eqvs ss redex =
 
   548 *}
 
   509   let
 
   549 
   510     val ctxt = Simplifier.the_context ss
 
   550 (*
 
   511     val thy = ProofContext.theory_of ctxt
 
   551 ML {*
 
   512   in
 
   552 fun regularize_tac ctxt rel_eqvs rel_refl =
 
   513   case redex of
 
   553   let
 
   514       (ogl as ((Const (@{const_name "Ball"}, _)) $
 
   554     val subs1 = map (fn x => @{thm equiv_res_forall} OF [x]) rel_eqvs
 
   515         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 
   555     val subs2 = map (fn x => @{thm equiv_res_exists} OF [x]) rel_eqvs
 
   516       (let
 
   556     val subs = map (fn x => @{thm eq_reflection} OF [x]) (subs1 @ subs2)
 
   517         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
 
   557   in
 
   518         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
   558   (ObjectLogic.full_atomize_tac) THEN'
 
   519         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
 
   559   (simp_tac ((Simplifier.context ctxt empty_ss) addsimps subs))
 
   520         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
 
   560   THEN'
 
   521 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 
   561   REPEAT_ALL_NEW (FIRST' 
   522       in
 
   562     [(rtac @{thm RIGHT_RES_FORALL_REGULAR}),
 
   523         SOME thm
 
   563      (rtac @{thm LEFT_RES_EXISTS_REGULAR}),
 
   524       end
 
   564      (resolve_tac (Inductive.get_monos ctxt)),
 
   525       handle _ => NONE
 
   565      (rtac @{thm ball_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
 
   526       )
 
   566      (rtac @{thm bex_respects_refl} THEN' (RANGE [SOLVES' (equiv_tac rel_eqvs)])),
 
   527   | _ => NONE
 
   567      rtac @{thm move_forall},
 
   528   end
 
   568      rtac @{thm move_exists},
 
   529 *}
 
   569      (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' (resolve_tac rel_refl))])
 
   530 
   570   end
 
   531 ML {*
 
   571 *}
 
   532 fun bex_reg_eqv_simproc rel_eqvs ss redex =
 
   572 *)
 
   533   let
 
       
   534     val ctxt = Simplifier.the_context ss
 
       
   535     val thy = ProofContext.theory_of ctxt
 
       
   536   in
 
       
   537   case redex of
 
       
   538       (ogl as ((Const (@{const_name "Bex"}, _)) $
 
       
   539         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 
       
   540       (let
 
       
   541         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R;
 
       
   542         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   543         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
 
       
   544         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
 
       
   545 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 
       
   546       in
 
       
   547         SOME thm
 
       
   548       end
 
       
   549       handle _ => NONE
 
       
   550       )
 
       
   551   | _ => NONE
 
       
   552   end
 
       
   553 *}
 
       
   554 
       
   555 ML {*
 
       
   556 fun prep_trm thy (x, (T, t)) =
 
       
   557   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
       
   558 
       
   559 fun prep_ty thy (x, (S, ty)) =
 
       
   560   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)
 
       
   561 *}
 
       
   562 
       
   563 ML {*
 
       
   564 fun matching_prs thy pat trm =
 
       
   565 let
 
       
   566   val univ = Unify.matchers thy [(pat, trm)]
 
       
   567   val SOME (env, _) = Seq.pull univ
 
       
   568   val tenv = Vartab.dest (Envir.term_env env)
 
       
   569   val tyenv = Vartab.dest (Envir.type_env env)
 
       
   570 in
 
       
   571   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 
       
   572 end
 
       
   573 *}
 
       
   574 
       
   575 ML {*
 
       
   576 fun ball_reg_eqv_range_simproc rel_eqvs ss redex =
 
       
   577   let
 
       
   578     val ctxt = Simplifier.the_context ss
 
       
   579     val thy = ProofContext.theory_of ctxt
 
       
   580   in
 
       
   581   case redex of
 
       
   582       (ogl as ((Const (@{const_name "Ball"}, _)) $
 
       
   583         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
 
       
   584       (let
 
       
   585         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
 
       
   586         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   587         val _ = tracing (Syntax.string_of_term ctxt glc);
 
       
   588         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
 
       
   589         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
 
       
   590         val R1c = cterm_of thy R1;
 
       
   591         val thmi = Drule.instantiate' [] [SOME R1c] thm;
 
       
   592 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
 
       
   593         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 
       
   594         val _ = tracing "AAA";
 
       
   595         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
 
       
   596         val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
 
       
   597       in
 
       
   598         SOME thm2
 
       
   599       end
 
       
   600       handle _ => NONE
 
       
   601 
       
   602       )
 
       
   603   | _ => NONE
 
       
   604   end
 
       
   605 *}
 
       
   606 
       
   607 ML {*
 
       
   608 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
 
       
   609   let
 
       
   610     val ctxt = Simplifier.the_context ss
 
       
   611     val thy = ProofContext.theory_of ctxt
 
       
   612   in
 
       
   613   case redex of
 
       
   614       (ogl as ((Const (@{const_name "Bex"}, _)) $
 
       
   615         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "FUN_REL"}, _)) $ R1 $ R2)) $ _)) =>
 
       
   616       (let
 
       
   617         val gl = Const (@{const_name "EQUIV"}, dummyT) $ R2;
 
       
   618         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   619         val _ = tracing (Syntax.string_of_term ctxt glc);
 
       
   620         val eqv = Goal.prove ctxt [] [] glc (fn _ => equiv_tac rel_eqvs 1);
 
       
   621         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
 
       
   622         val R1c = cterm_of thy R1;
 
       
   623         val thmi = Drule.instantiate' [] [SOME R1c] thm;
 
       
   624 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
 
       
   625         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 
       
   626         val _ = tracing "AAA";
 
       
   627         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
 
       
   628         val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));
 
       
   629       in
 
       
   630         SOME thm2
 
       
   631       end
 
       
   632       handle _ => NONE
 
       
   633 
       
   634       )
 
       
   635   | _ => NONE
 
       
   636   end
 
       
   637 *}
 
       
   638 
       
   639 lemma eq_imp_rel: "EQUIV R \<Longrightarrow> a = b \<longrightarrow> R a b"
 
       
   640 by (simp add: EQUIV_REFL)
 
       
   641 
       
   642 ML {*
 
       
   643 fun regularize_tac ctxt rel_eqvs =
 
       
   644   let
 
       
   645     val pat1 = [@{term "Ball (Respects R) P"}];
 
       
   646     val pat2 = [@{term "Bex (Respects R) P"}];
 
       
   647     val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
 
       
   648     val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
 
       
   649     val thy = ProofContext.theory_of ctxt
 
       
   650     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc rel_eqvs))
 
       
   651     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc rel_eqvs))
 
       
   652     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
 
       
   653     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
 
       
   654     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
 
       
   655     (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
 
       
   656     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
 
       
   657   in
 
       
   658   ObjectLogic.full_atomize_tac THEN'
 
       
   659   simp_tac simp_ctxt THEN'
 
       
   660   REPEAT_ALL_NEW (FIRST' [
 
       
   661     rtac @{thm ball_reg_right},
 
       
   662     rtac @{thm bex_reg_left},
 
       
   663     resolve_tac (Inductive.get_monos ctxt),
 
       
   664     rtac @{thm ball_all_comm},
 
       
   665     rtac @{thm bex_ex_comm},
 
       
   666     resolve_tac eq_eqvs,
 
       
   667     simp_tac simp_ctxt
 
       
   668   ])
 
       
   669   end
 
       
   670 *}
 
   573 
   671 
   574 section {* Injections of REP and ABSes *}
 
   672 section {* Injections of REP and ABSes *}
 
   575 
   673 
   576 (*
 
   674 (*
 
   577 Injecting REPABS means:
 
   675 Injecting REPABS means:
 
   739       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
   837       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
   740   | _ => false
 
   838   | _ => false
 
   741 
   839 
   742 *}
 
   840 *}
 
   743 
   841 
   744 ML {*
 
   842 (* Doesn't work *)
 
   745 fun APPLY_RSP_TAC rty = 
   843 ML {*
 
   746   CSUBGOAL (fn (concl, i) =>
 
   844 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
 
   747   let
 
   845   let
 
   748     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
 
   846     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
 
   749     val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
 
   847     val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
 
   750     val insts = Thm.match (pat, concl)
 
   848     val insts = Thm.match (pat, concl)
 
   751   in
 
   849   in
 
   752     if needs_lift rty (type_of f) 
   850     if needs_lift rty (type_of f) then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
 
   753     then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i
 
       
   754     else no_tac
 
   851     else no_tac
 
   755   end
 
   852   end
 
   756   handle _ => no_tac)
 
   853   handle _ => no_tac)
 
   757 *}
 
   854 *}
 
   758 
   855 
   759 ML {*
 
   856 
   760 val ball_rsp_tac = 
   857 
   761   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 
   858 ML {*
 
       
   859 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 
   762   let
 
   860   let
 
   763     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
 
   861     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
 
   764                  (Const (@{const_name Ball}, _) $ _)) = term_of concl
 
   862                  (Const (@{const_name Ball}, _) $ _)) = term_of concl
 
   765   in
 
   863   in
 
   766     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 
   864     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 
   770   end
 
   868   end
 
   771   handle _ => no_tac)
 
   869   handle _ => no_tac)
 
   772 *}
 
   870 *}
 
   773 
   871 
   774 ML {*
 
   872 ML {*
 
   775 val bex_rsp_tac = 
   873 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 
   776   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
 
       
   777   let
 
   874   let
 
   778     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
 
   875     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
 
   779                  (Const (@{const_name Bex}, _) $ _)) = term_of concl
 
   876                  (Const (@{const_name Bex}, _) $ _)) = term_of concl
 
   780   in
 
   877   in
 
   781     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 
   878     ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
 
   782     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
 
   879     THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
 
   783     THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
 
   880     THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
 
   784     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
 
   881     (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
 
   785   end
 
   882   end
 
   786   handle _ => no_tac)
 
   883   handle _ => no_tac)
 
       
   884 *}
 
       
   885 
       
   886 ML {*
 
       
   887 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 
   787 *}
 
   888 *}
 
   788 
   889 
   789 ML {*
 
   890 ML {*
 
   790 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
 
   891 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
 
   791   (FIRST' [resolve_tac trans2,
 
   892   (FIRST' [resolve_tac trans2,
 
   794            ball_rsp_tac ctxt,
 
   895            ball_rsp_tac ctxt,
 
   795            rtac @{thm RES_EXISTS_RSP},
 
   896            rtac @{thm RES_EXISTS_RSP},
 
   796            bex_rsp_tac ctxt,
 
   897            bex_rsp_tac ctxt,
 
   797            resolve_tac rsp_thms,
 
   898            resolve_tac rsp_thms,
 
   798            rtac @{thm refl},
 
   899            rtac @{thm refl},
 
   799            (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
   900            (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN'
 
   800               (RANGE [SOLVES' (quotient_tac quot_thms)])),
 
   901               (RANGE [SOLVES' (quotient_tac quot_thms)])),
 
   801            (APPLY_RSP_TAC rty THEN' 
   902            (APPLY_RSP_TAC rty ctxt THEN'
 
   802               (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
 
   903               (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
 
   803            Cong_Tac.cong_tac @{thm cong},
 
   904            Cong_Tac.cong_tac @{thm cong},
 
   804            rtac @{thm ext},
 
   905            rtac @{thm ext},
 
   805            resolve_tac rel_refl,
 
   906            resolve_tac rel_refl,
 
   806            atac,
 
   907            atac,
 
   860     (* reflexivity of operators arising from Cong_tac *)
 
   961     (* reflexivity of operators arising from Cong_tac *)
 
   861     DT ctxt "8" (rtac @{thm refl}),
 
   962     DT ctxt "8" (rtac @{thm refl}),
 
   862 
   963 
   863     (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
 
   964     (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
 
   864     (* observe ---> *) 
   965     (* observe ---> *) 
   865     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
   966     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
 
   866                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
   967                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
   867 
   968 
   868     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
 
   969     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
 
   869     DT ctxt "A" ((APPLY_RSP_TAC rty THEN' 
   970     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
 
   870                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
   971                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
   871 
   972 
   872     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
 
   973     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
 
   873     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
   974     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
   874 
   975 
   961 
  1062 
   962 ML {*
 
  1063 ML {*
 
   963 fun allex_prs_tac lthy quot =
 
  1064 fun allex_prs_tac lthy quot =
 
   964   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
 
  1065   (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
 
   965   THEN' (quotient_tac quot)
 
  1066   THEN' (quotient_tac quot)
 
   966 *}
 
       
   967 
       
   968 ML {* 
       
   969 fun prep_trm thy (x, (T, t)) = 
       
   970   (cterm_of thy (Var (x, T)), cterm_of thy t) 
       
   971 
       
   972 fun prep_ty thy (x, (S, ty)) = 
       
   973   (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) 
       
   974 *}
 
       
   975 
       
   976 ML {*
 
       
   977 fun matching_prs thy pat trm = 
       
   978 let
 
       
   979   val univ = Unify.matchers thy [(pat, trm)] 
       
   980   val SOME (env, _) = Seq.pull univ
 
       
   981   val tenv = Vartab.dest (Envir.term_env env)
 
       
   982   val tyenv = Vartab.dest (Envir.type_env env)
 
       
   983 in
 
       
   984   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 
       
   985 end 
       
   986 *}
 
  1067 *}
 
   987 
  1068 
   988 (* Rewrites the term with LAMBDA_PRS thm.
 
  1069 (* Rewrites the term with LAMBDA_PRS thm.
 
   989 
  1070 
   990 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
 
  1071 Replaces: (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))
 
  1168       val rule = procedure_inst context (prop_of rthm') (term_of concl)
 
  1249       val rule = procedure_inst context (prop_of rthm') (term_of concl)
 
  1169       val aps = find_aps (prop_of rthm') (term_of concl)
 
  1250       val aps = find_aps (prop_of rthm') (term_of concl)
 
  1170       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
 
  1251       val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) rel_eqv
 
  1171       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
 
  1252       val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) rel_eqv
 
  1172     in
 
  1253     in
 
  1173       EVERY1 
  1254       EVERY1
 
  1174        [rtac rule, 
  1255        [rtac rule,
 
  1175         RANGE [rtac rthm',
 
  1256         RANGE [rtac rthm',
 
  1176                regularize_tac lthy (hd rel_eqv) rel_refl, (* temporary hd *)
 
  1257                regularize_tac lthy rel_eqv,
 
  1177                REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
 
  1258                REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
 
  1178                clean_tac lthy quot defs aps]] 
  1259                clean_tac lthy quot defs aps]]
 
  1179     end) lthy
 
  1260     end) lthy
 
  1180 *}
 
  1261 *}
 
  1181 
  1262 
  1182 end
 
  1263 end
 
  1183 
  1264
nominal2