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 581 2da4fb1894d2
parent 578 070161f1996a
child 582 a082e2d138ab
equal deleted inserted replaced
580:fc48fe9667f2 581:2da4fb1894d2 
   253 end
 
   253 end
 
   254 
   254 
   255 fun NDT ctxt s tac thm = tac thm  
   255 fun NDT ctxt s tac thm = tac thm  
   256 *}
 
   256 *}
 
   257 
   257 
       
   258 section {* Matching of terms and types *}
 
       
   259 
       
   260 ML {*
 
       
   261 fun matches_typ (ty, ty') =
 
       
   262   case (ty, ty') of
 
       
   263     (_, TVar _) => true
 
       
   264   | (TFree x, TFree x') => x = x'
 
       
   265   | (Type (s, tys), Type (s', tys')) => 
       
   266        s = s' andalso 
       
   267        if (length tys = length tys') 
       
   268        then (List.all matches_typ (tys ~~ tys')) 
       
   269        else false
 
       
   270   | _ => false
 
       
   271 *}
 
       
   272 
       
   273 ML {*
 
       
   274 fun matches_term (trm, trm') = 
       
   275    case (trm, trm') of 
       
   276      (_, Var _) => true
 
       
   277    | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
 
       
   278    | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
 
       
   279    | (Bound i, Bound j) => i = j
 
       
   280    | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
 
       
   281    | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
       
   282    | _ => false
 
       
   283 *}
 
   258 
   284 
   259 section {* Infrastructure for collecting theorems for starting the lifting *}
 
   285 section {* Infrastructure for collecting theorems for starting the lifting *}
 
   260 
   286 
   261 ML {*
 
   287 ML {*
 
   262 fun lookup_quot_data lthy qty =
 
   288 fun lookup_quot_data lthy qty =
 
   342              (* FIXME: check that the types correspond to each other? *)
 
   368              (* FIXME: check that the types correspond to each other? *)
 
   343 end
 
   369 end
 
   344 *}
 
   370 *}
 
   345 
   371 
   346 ML {*
 
   372 ML {*
 
   347 fun matches_typ (ty, ty') =
 
       
   348   case (ty, ty') of
 
       
   349     (_, TVar _) => true
 
       
   350   | (TFree x, TFree x') => x = x'
 
       
   351   | (Type (s, tys), Type (s', tys')) => 
       
   352        s = s' andalso 
       
   353        if (length tys = length tys') 
       
   354        then (List.all matches_typ (tys ~~ tys')) 
       
   355        else false
 
       
   356   | _ => false
 
       
   357 *}
 
       
   358 ML {*
 
       
   359 fun matches_term (trm, trm') = 
       
   360    case (trm, trm') of 
       
   361      (_, Var _) => true
 
       
   362    | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
 
       
   363    | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty')
 
       
   364    | (Bound i, Bound j) => i = j
 
       
   365    | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t')
 
       
   366    | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') 
       
   367    | _ => false
 
       
   368 *}
 
       
   369 
       
   370 ML {*
 
       
   371 val mk_babs = Const (@{const_name Babs}, dummyT)
 
   373 val mk_babs = Const (@{const_name Babs}, dummyT)
 
   372 val mk_ball = Const (@{const_name Ball}, dummyT)
 
   374 val mk_ball = Const (@{const_name Ball}, dummyT)
 
   373 val mk_bex  = Const (@{const_name Bex}, dummyT)
 
   375 val mk_bex  = Const (@{const_name Bex}, dummyT)
 
   374 val mk_resp = Const (@{const_name Respects}, dummyT)
 
   376 val mk_resp = Const (@{const_name Respects}, dummyT)
 
   375 *}
 
   377 *}
 
   490  - Ball (Respects ?E) ?P = All ?P
 
   492  - Ball (Respects ?E) ?P = All ?P
 
   491  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
   493  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
   492 
   494 
   493 *)
 
   495 *)
 
   494 
   496 
   495 (* FIXME: they should be in in the new Isabelle *)
 
       
   496 lemma [mono]: 
       
   497   "(\<And>x. P x \<longrightarrow> Q x) \<Longrightarrow> (Ex P) \<longrightarrow> (Ex Q)"
 
       
   498 by blast
 
       
   499 
       
   500 lemma [mono]: "P \<longrightarrow> Q \<Longrightarrow> \<not>Q \<longrightarrow> \<not>P"
 
       
   501 by auto
 
       
   502 
       
   503 (* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 
   497 (* FIXME: OPTION_equivp, PAIR_equivp, ... *)
 
   504 ML {*
 
   498 ML {*
 
   505 fun equiv_tac rel_eqvs =
 
   499 fun equiv_tac rel_eqvs =
 
   506   REPEAT_ALL_NEW (FIRST' 
   500   REPEAT_ALL_NEW (FIRST' 
   507     [resolve_tac rel_eqvs,
 
   501     [resolve_tac rel_eqvs,
 
   508      rtac @{thm identity_equivp},
 
   502      rtac @{thm identity_equivp},
 
   509      rtac @{thm list_equivp}])
 
   503      rtac @{thm list_equivp}])
 
   510 *}
 
   504 *}
 
       
   505 
       
   506 thm ball_reg_eqv
 
   511 
   507 
   512 ML {*
 
   508 ML {*
 
   513 fun ball_reg_eqv_simproc rel_eqvs ss redex =
 
   509 fun ball_reg_eqv_simproc rel_eqvs ss redex =
 
   514   let
 
   510   let
 
   515     val ctxt = Simplifier.the_context ss
 
   511     val ctxt = Simplifier.the_context ss
 
   605 
   601 
   606       )
 
   602       )
 
   607   | _ => NONE
 
   603   | _ => NONE
 
   608   end
 
   604   end
 
   609 *}
 
   605 *}
 
       
   606 
       
   607 thm ball_reg_eqv_range
 
       
   608 thm bex_reg_eqv_range
 
   610 
   609 
   611 ML {*
 
   610 ML {*
 
   612 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
 
   611 fun bex_reg_eqv_range_simproc rel_eqvs ss redex =
 
   613   let
 
   612   let
 
   614     val ctxt = Simplifier.the_context ss
 
   613     val ctxt = Simplifier.the_context ss
 
   740         then rtrm 
   739         then rtrm 
   741         else mk_repabs lthy (T, T') rtrm
 
   740         else mk_repabs lthy (T, T') rtrm
 
   742 
   741 
   743   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
   742   | (_, Const (@{const_name "op ="}, _)) => rtrm
 
   744 
   743 
   745     (* FIXME: check here that rtrm is the corresponding definition for teh const *)
 
   744     (* FIXME: check here that rtrm is the corresponding definition for the const *)
 
   746   | (_, Const (_, T')) =>
 
   745   | (_, Const (_, T')) =>
 
   747       let
 
   746       let
 
   748         val rty = fastype_of rtrm
 
   747         val rty = fastype_of rtrm
 
   749       in 
   748       in 
   750         if rty = T'                    
   749         if rty = T'                    
   755   | _ => raise (LIFT_MATCH "injection")
 
   754   | _ => raise (LIFT_MATCH "injection")
 
   756 *}
 
   755 *}
 
   757 
   756 
   758 section {* RepAbs Injection Tactic *}
 
   757 section {* RepAbs Injection Tactic *}
 
   759 
   758 
   760 (* Not used anymore *)
 
       
   761 (* FIXME/TODO: do not handle everything *)
 
       
   762 ML {*
 
       
   763 fun instantiate_tac thm = 
       
   764   Subgoal.FOCUS (fn {concl, ...} =>
 
       
   765   let
 
       
   766     val pat = Drule.strip_imp_concl (cprop_of thm)
 
       
   767     val insts = Thm.first_order_match (pat, concl)
 
       
   768   in
 
       
   769     rtac (Drule.instantiate insts thm) 1
 
       
   770   end
 
       
   771   handle _ => no_tac)
 
       
   772 *}
 
       
   773 
       
   774 ML {*
 
   759 ML {*
 
   775 fun quotient_tac ctxt =
 
   760 fun quotient_tac ctxt =
 
   776   REPEAT_ALL_NEW (FIRST'
 
   761   REPEAT_ALL_NEW (FIRST'
 
   777     [rtac @{thm identity_quotient},
 
   762     [rtac @{thm identity_quotient},
 
   778      resolve_tac (quotient_rules_get ctxt)])
 
   763      resolve_tac (quotient_rules_get ctxt)])
 
   780 
   765 
   781 (* solver for the simplifier *)
 
   766 (* solver for the simplifier *)
 
   782 ML {*
 
   767 ML {*
 
   783 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 
   768 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 
   784 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 
   769 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 
       
   770 *}
 
       
   771 
       
   772 ML {*
 
       
   773 fun solve_quotient_assums ctxt thm =
 
       
   774   let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
 
       
   775   thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
 
       
   776   end
 
       
   777   handle _ => error "solve_quotient_assums"
 
       
   778 *}
 
       
   779 
       
   780 (* It proves the Quotient assumptions by calling quotient_tac *)
 
       
   781 ML {*
 
       
   782 fun solve_quotient_assum i ctxt thm =
 
       
   783   let
 
       
   784     val tac =
 
       
   785       (compose_tac (false, thm, i)) THEN_ALL_NEW
 
       
   786       (quotient_tac ctxt);
 
       
   787     val gc = Drule.strip_imp_concl (cprop_of thm);
 
       
   788   in
 
       
   789     Goal.prove_internal [] gc (fn _ => tac 1)
 
       
   790   end
 
       
   791   handle _ => error "solve_quotient_assum"
 
   785 *}
 
   792 *}
 
   786 
   793 
   787 definition
 
   794 definition
 
   788   "QUOT_TRUE x \<equiv> True"
 
   795   "QUOT_TRUE x \<equiv> True"
 
   789 
   796 
   800     | SOME _ => error "find_qt_asm: no pair"
 
   807     | SOME _ => error "find_qt_asm: no pair"
 
   801     | NONE => error "find_qt_asm: no assumption"
 
   808     | NONE => error "find_qt_asm: no assumption"
 
   802   end
 
   809   end
 
   803 *}
 
   810 *}
 
   804 
   811 
   805 (* It proves the Quotient assumptions by calling quotient_tac *)
 
   812 (*
 
   806 ML {*
 
   813 To prove that the regularised theorem implies the abs/rep injected, 
   807 fun solve_quotient_assum i ctxt thm =
 
   814 we try:
 
   808   let
 
   815 
   809     val tac =
 
   816  1) theorems 'trans2' from the appropriate QUOT_TYPE
 
   810       (compose_tac (false, thm, i)) THEN_ALL_NEW
 
   817  2) remove lambdas from both sides: lambda_rsp_tac
 
   811       (quotient_tac ctxt);
 
   818  3) remove Ball/Bex from the right hand side
 
   812     val gc = Drule.strip_imp_concl (cprop_of thm);
 
   819  4) use user-supplied RSP theorems
 
   813   in
 
   820  5) remove rep_abs from the right side
 
   814     Goal.prove_internal [] gc (fn _ => tac 1)
 
   821  6) reflexivity of equality
 
   815   end
 
   822  7) split applications of lifted type (apply_rsp)
 
   816   handle _ => error "solve_quotient_assum"
 
   823  8) split applications of non-lifted type (cong_tac)
 
   817 *}
 
   824  9) apply extentionality
 
   818 
   825  A) reflexivity of the relation
 
   819 ML {*
 
   826  B) assumption
 
   820 fun solve_quotient_assums ctxt thm =
 
   827     (Lambdas under respects may have left us some assumptions)
 
   821   let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
 
   828  C) proving obvious higher order equalities by simplifying fun_rel
 
   822   thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
 
   829     (not sure if it is still needed?)
 
   823   end
 
   830  D) unfolding lambda on one side
 
   824   handle _ => error "solve_quotient_assums"
 
   831  E) simplifying (= ===> =) for simpler respectfulness
 
       
   832 
       
   833 *)
 
       
   834 
       
   835 lemma quot_true_dests:
 
       
   836   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
 
       
   837   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
 
       
   838   and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
 
       
   839   and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
 
       
   840 apply(simp_all add: QUOT_TRUE_def ext)
 
       
   841 done
 
       
   842 
       
   843 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 
       
   844 by (simp add: QUOT_TRUE_def)
 
       
   845 
       
   846 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 
       
   847 by (simp add: QUOT_TRUE_def)
 
       
   848 
       
   849 ML {*
 
       
   850 fun quot_true_conv1 ctxt fnctn ctrm =
 
       
   851   case (term_of ctrm) of
 
       
   852     (Const (@{const_name QUOT_TRUE}, _) $ x) =>
 
       
   853     let
 
       
   854       val fx = fnctn x;
 
       
   855       val thy = ProofContext.theory_of ctxt;
 
       
   856       val cx = cterm_of thy x;
 
       
   857       val cfx = cterm_of thy fx;
 
       
   858       val cxt = ctyp_of thy (fastype_of x);
 
       
   859       val cfxt = ctyp_of thy (fastype_of fx);
 
       
   860       val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
 
       
   861     in
 
       
   862       Conv.rewr_conv thm ctrm
 
       
   863     end
 
       
   864 *}
 
       
   865 
       
   866 ML {*
 
       
   867 fun quot_true_conv ctxt fnctn ctrm =
 
       
   868   case (term_of ctrm) of
 
       
   869     (Const (@{const_name QUOT_TRUE}, _) $ _) =>
 
       
   870       quot_true_conv1 ctxt fnctn ctrm
 
       
   871   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
 
       
   872   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
 
       
   873   | _ => Conv.all_conv ctrm
 
       
   874 *}
 
       
   875 
       
   876 ML {*
 
       
   877 fun quot_true_tac ctxt fnctn = CONVERSION
 
       
   878     ((Conv.params_conv ~1 (fn ctxt =>
 
       
   879        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 
       
   880 *}
 
       
   881 
       
   882 ML {* fun dest_comb (f $ a) = (f, a) *}
 
       
   883 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
 
       
   884 (* TODO: Can this be done easier? *)
 
       
   885 ML {*
 
       
   886 fun unlam t =
 
       
   887   case t of
 
       
   888     (Abs a) => snd (Term.dest_abs a)
 
       
   889   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 
       
   890 *}
 
       
   891 
       
   892 ML {*
 
       
   893 fun dest_fun_type (Type("fun", [T, S])) = (T, S)
 
       
   894   | dest_fun_type _ = error "dest_fun_type"
 
       
   895 *}
 
       
   896 
       
   897 ML {*
 
       
   898 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
   825 *}
 
   899 *}
 
   826 
   900 
   827 ML {*
 
   901 ML {*
 
   828 val apply_rsp_tac =
 
   902 val apply_rsp_tac =
 
   829   Subgoal.FOCUS (fn {concl, asms, context,...} =>
 
   903   Subgoal.FOCUS (fn {concl, asms, context,...} =>
 
   847           end
 
   921           end
 
   848         end
 
   922         end
 
   849         handle ERROR "find_qt_asm: no pair" => no_tac)
 
   923         handle ERROR "find_qt_asm: no pair" => no_tac)
 
   850     | _ => no_tac)
 
   924     | _ => no_tac)
 
   851 *}
 
   925 *}
 
   852 
       
   853 ML {*
 
   926 ML {*
 
   854 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 
   927 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 
   855 *}
 
       
   856 
       
   857 (*
 
       
   858 To prove that the regularised theorem implies the abs/rep injected, 
       
   859 we try:
 
       
   860 
       
   861  1) theorems 'trans2' from the appropriate QUOT_TYPE
 
       
   862  2) remove lambdas from both sides: lambda_rsp_tac
 
       
   863  3) remove Ball/Bex from the right hand side
 
       
   864  4) use user-supplied RSP theorems
 
       
   865  5) remove rep_abs from the right side
 
       
   866  6) reflexivity of equality
 
       
   867  7) split applications of lifted type (apply_rsp)
 
       
   868  8) split applications of non-lifted type (cong_tac)
 
       
   869  9) apply extentionality
 
       
   870  A) reflexivity of the relation
 
       
   871  B) assumption
 
       
   872     (Lambdas under respects may have left us some assumptions)
 
       
   873  C) proving obvious higher order equalities by simplifying fun_rel
 
       
   874     (not sure if it is still needed?)
 
       
   875  D) unfolding lambda on one side
 
       
   876  E) simplifying (= ===> =) for simpler respectfulness
 
       
   877 
       
   878 *)
 
       
   879 
       
   880 lemma quot_true_dests:
 
       
   881   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
 
       
   882   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
 
       
   883   and   QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE  (P x))"
 
       
   884   and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
 
       
   885 apply(simp_all add: QUOT_TRUE_def ext)
 
       
   886 done
 
       
   887 
       
   888 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 
       
   889 by (simp add: QUOT_TRUE_def)
 
       
   890 
       
   891 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 
       
   892 by (simp add: QUOT_TRUE_def)
 
       
   893 
       
   894 ML {*
 
       
   895 fun quot_true_conv1 ctxt fnctn ctrm =
 
       
   896   case (term_of ctrm) of
 
       
   897     (Const (@{const_name QUOT_TRUE}, _) $ x) =>
 
       
   898     let
 
       
   899       val fx = fnctn x;
 
       
   900       val thy = ProofContext.theory_of ctxt;
 
       
   901       val cx = cterm_of thy x;
 
       
   902       val cfx = cterm_of thy fx;
 
       
   903       val cxt = ctyp_of thy (fastype_of x);
 
       
   904       val cfxt = ctyp_of thy (fastype_of fx);
 
       
   905       val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
 
       
   906     in
 
       
   907       Conv.rewr_conv thm ctrm
 
       
   908     end
 
       
   909 *}
 
       
   910 
       
   911 ML {*
 
       
   912 fun quot_true_conv ctxt fnctn ctrm =
 
       
   913   case (term_of ctrm) of
 
       
   914     (Const (@{const_name QUOT_TRUE}, _) $ _) =>
 
       
   915       quot_true_conv1 ctxt fnctn ctrm
 
       
   916   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
 
       
   917   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
 
       
   918   | _ => Conv.all_conv ctrm
 
       
   919 *}
 
       
   920 
       
   921 ML {*
 
       
   922 fun quot_true_tac ctxt fnctn = CONVERSION
 
       
   923     ((Conv.params_conv ~1 (fn ctxt =>
 
       
   924        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 
       
   925 *}
 
       
   926 
       
   927 ML {* fun dest_comb (f $ a) = (f, a) *}
 
       
   928 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}
 
       
   929 (* TODO: Can this be done easier? *)
 
       
   930 ML {*
 
       
   931 fun unlam t =
 
       
   932   case t of
 
       
   933     (Abs a) => snd (Term.dest_abs a)
 
       
   934   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
 
       
   935 *}
 
       
   936 
       
   937 ML {*
 
       
   938 fun dest_fun_type (Type("fun", [T, S])) = (T, S)
 
       
   939   | dest_fun_type _ = error "dest_fun_type"
 
       
   940 *}
 
       
   941 
       
   942 ML {*
 
       
   943 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
 
       
   944 *}
 
   928 *}
 
   945 
   929 
   946 ML {*
 
   930 ML {*
 
   947 fun rep_abs_rsp_tac ctxt =
 
   931 fun rep_abs_rsp_tac ctxt =
 
   948   SUBGOAL (fn (goal, i) =>
 
   932   SUBGOAL (fn (goal, i) =>
 
   966 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 
   950 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
 
   967 (case (bare_concl goal) of
 
   951 (case (bare_concl goal) of
 
   968     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
 
   952     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
 
   969   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
 
   953   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
 
   970       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
   954       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
       
   955 
   971     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   956     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   972 | (Const (@{const_name "op ="},_) $
 
   957 | (Const (@{const_name "op ="},_) $
 
   973     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   958     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   974     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
 
   959     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
 
   975       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
 
   960       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
 
       
   961 
   976     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
 
   962     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
 
   977 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   963 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   978     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   964     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   979     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   965     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   980       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
   966       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
       
   967 
   981     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   968     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
 
   982 | Const (@{const_name "op ="},_) $
 
   969 | Const (@{const_name "op ="},_) $
 
   983     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   970     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   984     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   971     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   985       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
 
   972       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
 
       
   973 
   986     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
 
   974     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
 
   987 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   975 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   988     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   976     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
 
   989     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   977     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
 
   990       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
   978       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
   991 | Const (@{const_name "op ="},_) $ _ $ _ => 
   979 
   992     (* reflexivity of operators arising from Cong_tac *)
 
   980     (* reflexivity of operators arising from Cong_tac *)
 
   993     rtac @{thm refl} ORELSE'
 
   981 | Const (@{const_name "op ="},_) $ _ $ _ 
   994     (resolve_tac trans2 THEN' RANGE [
 
   982       => rtac @{thm refl} ORELSE'
 
   995       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 
   983           (resolve_tac trans2 THEN' RANGE [
 
       
   984             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 
       
   985 
   996 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   986 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   997     (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   987     (Const (@{const_name fun_rel}, _) $ _ $ _) $
 
   998     (Const (@{const_name fun_rel}, _) $ _ $ _)
 
   988     (Const (@{const_name fun_rel}, _) $ _ $ _)
 
   999     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
 
   989     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
 
  1000 | _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
 
   990 
  1001     (* respectfulness of constants; in particular of a simple relation *)
 
   991    (* respectfulness of constants; in particular of a simple relation *)
 
  1002     resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 
   992 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
 
  1003 | _ $ _ $ _ =>
 
   993     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
 
       
   994 
  1004     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
 
   995     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
 
  1005     (* observe ---> *)
 
   996     (* observe ---> *)
 
  1006     rep_abs_rsp_tac ctxt
 
   997 | _ $ _ $ _ 
       
   998     => rep_abs_rsp_tac ctxt
 
       
   999 
  1007 | _ => error "inj_repabs_tac not a relation"
 
  1000 | _ => error "inj_repabs_tac not a relation"
 
  1008 ) i)
 
  1001 ) i)
 
  1009 *}
 
  1002 *}
 
  1010 
  1003 
  1011 ML {*
 
  1004 ML {*
 
  1031 
  1024 
  1032 ML {*
 
  1025 ML {*
 
  1033 fun all_inj_repabs_tac ctxt rel_refl trans2 =
 
  1026 fun all_inj_repabs_tac ctxt rel_refl trans2 =
 
  1034   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 
  1027   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 
  1035 *}
 
  1028 *}
 
  1036 
       
  1037 
       
  1038 
  1029 
  1039 section {* Cleaning of the theorem *}
 
  1030 section {* Cleaning of the theorem *}
 
  1040 
  1031 
  1041 ML {*
 
  1032 ML {*
 
  1042 fun make_inst lhs t =
 
  1033 fun make_inst lhs t =
nominal2