Quot/QuotMain.thy
changeset 739 089cf9ffb711
parent 738 7142389632fd
child 740 d151f24427ab
equal deleted inserted replaced
738:7142389632fd 739:089cf9ffb711
   664 thm apply_rsp
   664 thm apply_rsp
   665 
   665 
   666 ML {*
   666 ML {*
   667 val apply_rsp_tac =
   667 val apply_rsp_tac =
   668   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   668   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   669     case ((HOLogic.dest_Trueprop (term_of concl))) of
   669     case (HOLogic.dest_Trueprop (term_of concl)) of
   670       (R2 $ (f $ x) $ (g $ y)) =>
   670       (R2 $ (f $ x) $ (g $ y)) =>
   671         (let
   671         (let
   672            val (asmf, asma) = find_qt_asm (map term_of asms);
   672            val (asmf, asma) = find_qt_asm (map term_of asms);
   673          in
   673          in
   674            if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *)
   674            if (fastype_of asmf) = (fastype_of f) (* why is this test necessary *)
   675            then no_tac 
   675            then no_tac 
   676            else 
   676            else 
   677              let
   677              let
   678                val ty_a = fastype_of x;
   678                val ty_a = fastype_of x
   679                val ty_b = fastype_of asma;
   679                val ty_b = fastype_of asma
   680                val ty_c = range_type (type_of f); (* why type_of, not fast_type? *)
   680                val ty_c = range_type (type_of f) (* why type_of, not fast_type? *)
   681                val thy = ProofContext.theory_of context;
   681                val thy = ProofContext.theory_of context
   682                val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c];
   682                val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]
   683                val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp}
   683                val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y];
   684                val te = solve_quotient_assums context thm
   684                val thm' = Drule.instantiate' ty_inst [] @{thm apply_rsp}
   685                val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; 
   685                val te = solve_quotient_assums context thm'
   686                                                       (* why not instantiate terms 3 lines earlier *)
       
   687                val thm = Drule.instantiate' [] t_inst te
   686                val thm = Drule.instantiate' [] t_inst te
       
   687                     (* why not instantiate terms 3 lines earlier *)
       
   688                     (* \<dots> if done one gets an instantiate type conlict error ??? *)
       
   689                     (* why is necessary to get rid of the quot-assms first ???   *)
   688              in
   690              in
   689                compose_tac (false, thm, 2) 1
   691                compose_tac (false, thm, 2) 1
   690              end
   692              end
   691          end
   693          end
   692         handle ERROR "find_qt_asm: no pair" => no_tac)
   694         handle ERROR "find_qt_asm: no pair" => no_tac)