equal
deleted
inserted
replaced
931 ML {*@{thm arg_cong2}*} |
931 ML {*@{thm arg_cong2}*} |
932 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
932 ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *} |
933 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
933 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *} |
934 ML {* |
934 ML {* |
935 Toplevel.program (fn () => |
935 Toplevel.program (fn () => |
936 Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2} |
936 Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2} |
937 ) |
937 ) |
938 *} |
938 *} |
939 |
939 |
940 ML {* |
940 ML {* |
941 fun split_binop_conv t = |
941 fun split_binop_conv t = |
1130 done |
1130 done |
1131 |
1131 |
1132 thm list.induct |
1132 thm list.induct |
1133 |
1133 |
1134 ML {* |
1134 ML {* |
1135 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct})) |
1135 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct})) |
1136 *} |
1136 *} |
1137 ML {* |
1137 ML {* |
1138 val goal = |
1138 val goal = |
1139 Toplevel.program (fn () => |
1139 Toplevel.program (fn () => |
1140 build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1140 build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1142 *} |
1142 *} |
1143 ML {* |
1143 ML {* |
1144 val cgoal = cterm_of @{theory} goal |
1144 val cgoal = cterm_of @{theory} goal |
1145 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1145 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1146 *} |
1146 *} |
1147 ML fset_defs_sym |
1147 |
1148 prove {* (Thm.term_of cgoal2) *} |
1148 prove {* (Thm.term_of cgoal2) *} |
1149 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1149 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1150 apply (tactic {* foo_tac' @{context} 1 *}) |
1150 apply (tactic {* foo_tac' @{context} 1 *}) |
1151 sorry |
1151 sorry |
1152 |
1152 |
1229 |
1229 |
1230 ML {* MRS *} |
1230 ML {* MRS *} |
1231 thm card1_suc |
1231 thm card1_suc |
1232 |
1232 |
1233 ML {* |
1233 ML {* |
1234 val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc})) |
1234 val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc})) |
1235 *} |
1235 *} |
1236 ML {* |
1236 ML {* |
1237 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1237 val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs |
1238 *} |
1238 *} |
1239 ML {* |
1239 ML {* |