820 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
820 val (bop_s, _) = Term.dest_Const (Thm.term_of bop); |
821 in |
821 in |
822 if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) |
822 if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t])) |
823 end |
823 end |
824 *} |
824 *} |
825 ML {* |
825 ML Thm.instantiate |
826 fun foo_conv ctxt t = |
826 ML {*@{thm arg_cong2}*} |
|
827 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
|
828 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
|
829 ML {* |
|
830 Toplevel.program (fn () => |
|
831 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
|
832 ) |
|
833 *} |
|
834 |
|
835 ML {* |
|
836 fun foo_conv t = |
827 let |
837 let |
828 val (lhs, rhs) = dest_ceq t; |
838 val (lhs, rhs) = dest_ceq t; |
829 val (bop, _) = dest_cbinop lhs; |
839 val (bop, _) = dest_cbinop lhs; |
830 (* val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of lhs))*) |
840 val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp; |
|
841 val [cmT, crT] = Thm.dest_ctyp cr2; |
831 in |
842 in |
832 @{thm arg_cong2} |
843 Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2} |
833 end |
844 end |
834 *} |
845 *} |
835 ML {* |
846 |
836 fun foo_tac ctxt thm = |
847 ML ORELSE |
|
848 |
|
849 ML {* |
|
850 fun foo_tac n thm = |
837 let |
851 let |
838 val concl = Thm.concl_of thm; |
852 val concl = Thm.cprem_of thm n; |
839 val (_, cconcl) = Thm.dest_comb (Thm.cterm_of @{theory} concl); |
853 val (_, cconcl) = Thm.dest_comb concl; |
840 val (_, cconcl) = Thm.dest_comb cconcl; |
854 val rewr = foo_conv cconcl; |
841 val rewr = foo_conv ctxt cconcl; |
855 val _ = tracing (Display.string_of_thm @{context} rewr) |
842 val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of cconcl)) |
856 val _ = tracing (Display.string_of_thm @{context} thm) |
843 in |
857 in |
844 Seq.single thm |
858 rtac rewr n thm |
845 end |
859 end |
846 *} |
860 handle CTERM _ => Seq.empty |
|
861 *} |
|
862 |
|
863 ML foo_tac |
|
864 ML {* |
|
865 val foo_tac' = |
|
866 FIRST' [ |
|
867 rtac @{thm list_eq_sym}, |
|
868 rtac @{thm cons_preserves}, |
|
869 rtac @{thm mem_respects}, |
|
870 foo_tac, |
|
871 simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp}) |
|
872 ] |
|
873 *} |
|
874 |
847 ML {* Thm.assume @{cprop "0 = 0"} *} |
875 ML {* Thm.assume @{cprop "0 = 0"} *} |
848 |
876 |
|
877 ML simp_tac |
|
878 |
849 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
879 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *} |
850 apply (tactic {* foo_tac @{context} *}) |
880 apply (tactic {* foo_tac' 1 *}) |
|
881 unfolding IN_def INSERT_def |
|
882 apply (tactic {* foo_tac' 1 *}) |
|
883 apply (tactic {* foo_tac' 1 *}) |
|
884 apply (tactic {* foo_tac' 1 *}) |
|
885 apply (tactic {* foo_tac' 1 *}) |
|
886 apply (tactic {* foo_tac' 1 *}) |
|
887 apply (tactic {* foo_tac' 1 *}) |
|
888 apply (tactic {* foo_tac' 1 *}) |
|
889 apply (tactic {* foo_tac' 1 *}) |
|
890 apply (tactic {* foo_tac' 1 *}) |
|
891 apply (tactic {* foo_tac' 1 *}) |
|
892 apply (tactic {* foo_tac' 1 *}) |
|
893 apply (tactic {* foo_tac' 1 *}) |
|
894 done |
851 |
895 |
852 (* |
896 (* |
853 datatype obj1 = |
897 datatype obj1 = |
854 OVAR1 "string" |
898 OVAR1 "string" |
855 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
899 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |