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 592 66f39908df95
parent 590 951681538e3f
child 593 18eac4596ef1
equal deleted inserted replaced
591:01a0da807f50 592:66f39908df95 
   168 
   168 
   169 
   169 
   170 (* lifting of constants *)
 
   170 (* lifting of constants *)
 
   171 use "quotient_def.ML"
 
   171 use "quotient_def.ML"
 
   172 
   172 
       
   173 section {* Bounded abstraction *}
 
       
   174 
   173 definition
 
   175 definition
 
   174   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   176   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
   175 where
 
   177 where
 
   176   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
   178   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
       
   179 
       
   180 section {* Simset setup *}
 
       
   181 
       
   182 (* since HOL_basic_ss is too "big", we need to set up *)
 
       
   183 (* our own minimal simpset                            *)
 
       
   184 ML {*
 
       
   185 fun  mk_minimal_ss ctxt =
 
       
   186   Simplifier.context ctxt empty_ss
 
       
   187     setsubgoaler asm_simp_tac
 
       
   188     setmksimps (mksimps [])
 
       
   189 *}
 
   177 
   190 
   178 section {* atomize *}
 
   191 section {* atomize *}
 
   179 
   192 
   180 lemma atomize_eqv[atomize]:
 
   193 lemma atomize_eqv[atomize]:
 
   181   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 
   194   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 
   479 
   492 
   480   | (rt, qt) =>
 
   493   | (rt, qt) =>
 
   481        raise (LIFT_MATCH "regularize (default)")
 
   494        raise (LIFT_MATCH "regularize (default)")
 
   482 *}
 
   495 *}
 
   483 
   496 
   484 (*
 
       
   485 FIXME / TODO: needs to be adapted
 
       
   486 
       
   487 To prove that the raw theorem implies the regularised one, 
       
   488 we try in order:
 
       
   489 
       
   490  - Reflexivity of the relation
 
       
   491  - Assumption
 
       
   492  - Elimnating quantifiers on both sides of toplevel implication
 
       
   493  - Simplifying implications on both sides of toplevel implication
 
       
   494  - Ball (Respects ?E) ?P = All ?P
 
       
   495  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
       
   496 
       
   497 *)
 
       
   498 
       
   499 ML {*
 
   497 ML {*
 
   500 fun equiv_tac ctxt =
 
   498 fun equiv_tac ctxt =
 
   501   REPEAT_ALL_NEW (FIRST' 
   499   REPEAT_ALL_NEW (FIRST' 
   502     [resolve_tac (equiv_rules_get ctxt)])
 
   500     [resolve_tac (equiv_rules_get ctxt)])
 
   503 *}
 
   501 *}
 
   504 
   502 
   505 ML {*
 
   503 ML {*
 
   506 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 
   504 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 
   507 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
   505 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
   508 *}
 
       
   509 
       
   510 ML {*
 
       
   511 fun ball_reg_eqv_simproc ss redex =
 
       
   512   let
 
       
   513     val ctxt = Simplifier.the_context ss
 
       
   514     val thy = ProofContext.theory_of ctxt
 
       
   515   in
 
       
   516   case redex of
 
       
   517       (ogl as ((Const (@{const_name "Ball"}, _)) $
 
       
   518         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 
       
   519       (let
 
       
   520         val gl = Const (@{const_name "equivp"}, dummyT) $ R;
 
       
   521         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   522         val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
 
       
   523         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]);
 
       
   524 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 
       
   525       in
 
       
   526         SOME thm
 
       
   527       end
 
       
   528       handle _ => NONE
 
       
   529       )
 
       
   530   | _ => NONE
 
       
   531   end
 
       
   532 *}
 
       
   533 
       
   534 ML {*
 
       
   535 fun bex_reg_eqv_simproc ss redex =
 
       
   536   let
 
       
   537     val ctxt = Simplifier.the_context ss
 
       
   538     val thy = ProofContext.theory_of ctxt
 
       
   539   in
 
       
   540   case redex of
 
       
   541       (ogl as ((Const (@{const_name "Bex"}, _)) $
 
       
   542         ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) =>
 
       
   543       (let
 
       
   544         val gl = Const (@{const_name "equivp"}, dummyT) $ R;
 
       
   545         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   546         val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
 
       
   547         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]);
 
       
   548 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *)
 
       
   549       in
 
       
   550         SOME thm
 
       
   551       end
 
       
   552       handle _ => NONE
 
       
   553       )
 
       
   554   | _ => NONE
 
       
   555   end
 
       
   556 *}
 
   506 *}
 
   557 
   507 
   558 ML {*
 
   508 ML {*
 
   559 fun prep_trm thy (x, (T, t)) =
 
   509 fun prep_trm thy (x, (T, t)) =
 
   560   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
   510   (cterm_of thy (Var (x, T)), cterm_of thy t)
 
   574   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 
   524   (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
 
   575 end
 
   525 end
 
   576 *}
 
   526 *}
 
   577 
   527 
   578 ML {*
 
   528 ML {*
 
   579 fun ball_reg_eqv_range_simproc ss redex =
 
   529 fun calculate_instance ctxt thm redex R1 R2 =
 
   580   let
 
   530 let
 
   581     val ctxt = Simplifier.the_context ss
 
   531   val thy = ProofContext.theory_of ctxt
 
   582     val thy = ProofContext.theory_of ctxt
 
   532   val goal = Const (@{const_name "equivp"}, dummyT) $ R2  
   583   in
 
   533              |> Syntax.check_term ctxt
 
   584   case redex of
 
   534              |> HOLogic.mk_Trueprop 
   585       (ogl as ((Const (@{const_name "Ball"}, _)) $
 
   535   val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
 
   586         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
 
   536   val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
 
   587       (let
 
   537   val R1c = cterm_of thy R1
 
   588         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
 
   538   val thmi = Drule.instantiate' [] [SOME R1c] thm
 
   589         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
   539   val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex
 
   590 (*        val _ = tracing (Syntax.string_of_term ctxt glc);*)
 
   540   val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi)
 
   591         val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
 
   541 in
 
   592         val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv_range} OF [eqv]]);
 
   542   SOME thm2
 
   593         val R1c = cterm_of thy R1;
 
   543 end
 
   594         val thmi = Drule.instantiate' [] [SOME R1c] thm;
 
   544 handle _ => NONE
 
   595 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi));*)
 
   545 (* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)
 
   596         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 
   546 *}
 
   597         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
 
   547 
   598 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2)); *)
 
   548 ML {*
 
   599       in
 
   549 fun ball_bex_range_simproc ss redex =
 
   600         SOME thm2
 
   550 let
 
   601       end
 
   551   val ctxt = Simplifier.the_context ss
 
   602       handle _ => NONE
 
   552 in 
   603 
   553  case redex of
 
   604       )
 
   554     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       
   555       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
 
       
   556         calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
 
       
   557   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       
   558       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  
       
   559         calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
 
   605   | _ => NONE
 
   560   | _ => NONE
 
   606   end
 
   561 end
 
   607 *}
 
   562 *}
 
   608 
   563 
   609 
   564 lemma eq_imp_rel: 
   610 thm bex_reg_eqv_range
 
   565   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 
   611 thm ball_reg_eqv
 
       
   612 thm bex_reg_eqv
 
       
   613 
       
   614 ML {*
 
       
   615 fun bex_reg_eqv_range_simproc ss redex =
 
       
   616   let
 
       
   617     val ctxt = Simplifier.the_context ss
 
       
   618     val thy = ProofContext.theory_of ctxt
 
       
   619   in
 
       
   620   case redex of
 
       
   621       (ogl as ((Const (@{const_name "Bex"}, _)) $
 
       
   622         ((Const (@{const_name "Respects"}, _)) $ ((Const (@{const_name "fun_rel"}, _)) $ R1 $ R2)) $ _)) =>
 
       
   623       (let
 
       
   624         val gl = Const (@{const_name "equivp"}, dummyT) $ R2;
 
       
   625         val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl);
 
       
   626 (*        val _ = tracing (Syntax.string_of_term ctxt glc); *)
 
       
   627         val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1)
 
       
   628         val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv_range} OF [eqv]]);
 
       
   629         val R1c = cterm_of thy R1;
 
       
   630         val thmi = Drule.instantiate' [] [SOME R1c] thm;
 
       
   631 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thmi)); *)
 
       
   632         val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) ogl
 
       
   633         val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi);
 
       
   634 (*        val _ = tracing (Syntax.string_of_term ctxt (prop_of thm2));*)
 
       
   635       in
 
       
   636         SOME thm2
 
       
   637       end
 
       
   638       handle _ => NONE
 
       
   639 
       
   640       )
 
       
   641   | _ => NONE
 
       
   642   end
 
       
   643 *}
 
       
   644 
       
   645 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
 
       
   646 by (simp add: equivp_reflp)
 
   566 by (simp add: equivp_reflp)
 
   647 
   567 
   648 (* does not work yet
 
   568 (* FIXME/TODO: How does regularizing work? *)
 
       
   569 (* FIXME/TODO: needs to be adapted
 
       
   570 
       
   571 To prove that the raw theorem implies the regularised one, 
       
   572 we try in order:
 
       
   573 
       
   574  - Reflexivity of the relation
 
       
   575  - Assumption
 
       
   576  - Elimnating quantifiers on both sides of toplevel implication
 
       
   577  - Simplifying implications on both sides of toplevel implication
 
       
   578  - Ball (Respects ?E) ?P = All ?P
 
       
   579  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
       
   580 
       
   581 *)
 
   649 ML {*
 
   582 ML {*
 
   650 fun regularize_tac ctxt =
 
   583 fun regularize_tac ctxt =
 
   651   let
 
   584 let
 
   652     val pat1 = [@{term "Ball (Respects R) P"}];
 
   585   val thy = ProofContext.theory_of ctxt
 
   653     val pat2 = [@{term "Bex (Respects R) P"}];
 
   586   val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"}
 
   654     val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}];
 
   587   val pat_bex  = @{term "Bex (Respects (R1 ===> R2)) P"}
 
   655     val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}];
 
   588   val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc))
 
   656     val thy = ProofContext.theory_of ctxt
 
   589   val simpset = (mk_minimal_ss ctxt) 
   657     val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc))
 
   590                        addsimps @{thms ball_reg_eqv bex_reg_eqv}
 
   658     val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc))
 
   591                        addsimprocs [simproc] addSolver equiv_solver
 
   659     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc))
 
   592   (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
 
   660     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc))
 
   593   val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 
   661     val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv}
 
   594 in
 
   662                                  addsimprocs [simproc3, simproc4]
 
       
   663                                  addSolver equiv_solver
 
       
   664     * TODO: Make sure that there are no list_rel, pair_rel etc involved *
 
       
   665     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt)
 
       
   666   in
 
       
   667   ObjectLogic.full_atomize_tac THEN'
 
   595   ObjectLogic.full_atomize_tac THEN'
 
   668   simp_tac simp_set THEN'
 
   596   simp_tac simpset THEN'
 
   669   REPEAT_ALL_NEW (FIRST' [
 
   597   REPEAT_ALL_NEW (FIRST' [
 
   670     rtac @{thm ball_reg_right},
 
   598     rtac @{thm ball_reg_right},
 
   671     rtac @{thm bex_reg_left},
 
   599     rtac @{thm bex_reg_left},
 
   672     resolve_tac (Inductive.get_monos ctxt),
 
   600     resolve_tac (Inductive.get_monos ctxt),
 
   673     rtac @{thm ball_all_comm},
 
   601     rtac @{thm ball_all_comm},
 
   674     rtac @{thm bex_ex_comm},
 
   602     rtac @{thm bex_ex_comm},
 
   675     resolve_tac eq_eqvs,
 
   603     resolve_tac eq_eqvs,
 
   676     simp_tac simp_set
 
   604     simp_tac simpset])
 
   677   ])
 
       
   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
 
   605 end
 
   708 *}
 
   606 *}
 
   709 
   607 
   710 section {* Injections of rep and abses *}
 
   608 section {* Injections of rep and abses *}
 
   711 
   609 
  1081 *}
 
   979 *}
 
  1082 
   980 
  1083 ML {*
 
   981 ML {*
 
  1084 fun lambda_prs_simple_conv ctxt ctrm =
 
   982 fun lambda_prs_simple_conv ctxt ctrm =
 
  1085   case (term_of ctrm) of
 
   983   case (term_of ctrm) of
 
  1086    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
 
   984    ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) =>
 
  1087      let
 
   985      let
 
  1088        val thy = ProofContext.theory_of ctxt
 
   986        val thy = ProofContext.theory_of ctxt
 
  1089        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
 
   987        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
 
  1090        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
 
   988        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
 
  1091        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
 
   989        val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
 
  1094        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
 
   992        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
 
  1095        val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
 
   993        val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
 
  1096        val tl = Thm.lhs_of ts
 
   994        val tl = Thm.lhs_of ts
 
  1097        val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
 
   995        val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
 
  1098        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
 
   996        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
 
  1099         (*val _ = tracing "lambda_prs"
 
   997        val _ = if not (s = @{const_name "id"}) then
 
  1100           val _ = tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)))
 
   998                   (tracing "lambda_prs";
 
  1101           val _ = tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))*)
 
   999                    tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm)));
 
       
  1000                    tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi)));
 
       
  1001                    tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
 
       
  1002                    tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts)));
 
       
  1003                    tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti))))
 
       
  1004                else ()
 
  1102      in
 
  1005      in
 
  1103        Conv.rewr_conv ti ctrm
 
  1006        Conv.rewr_conv ti ctrm
 
  1104      end
 
  1007      end
 
  1105   | _ => Conv.all_conv ctrm
 
  1008   | _ => Conv.all_conv ctrm
 
  1106 *}
 
  1009 *}
 
  1143     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
 
  1046     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
 
  1144       (* FIXME: shouldn't the definitions already be varified? *)
 
  1047       (* FIXME: shouldn't the definitions already be varified? *)
 
  1145     val thms1 = @{thms all_prs ex_prs} @ defs
 
  1048     val thms1 = @{thms all_prs ex_prs} @ defs
 
  1146     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
  1049     val thms2 = @{thms eq_reflection[OF fun_map.simps]} 
  1147                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
  1050                 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} 
  1148     fun simps thms = HOL_basic_ss addsimps thms addSolver quotient_solver
 
  1051     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
 
  1149       (* FIXME: use of someting smaller than HOL_basic_ss *)
 
       
  1150   in
 
  1052   in
 
  1151     EVERY' [lambda_prs_tac lthy,
 
  1053     EVERY' [lambda_prs_tac lthy,
 
  1152             simp_tac (simps thms1),
 
  1054             simp_tac (simps thms1),
 
  1153             simp_tac (simps thms2),
 
  1055             simp_tac (simps thms2),
 
  1154             TRY o rtac refl]
 
  1056             TRY o rtac refl]
nominal2