835 (*Apply rules to break down assumptions of the form |
835 (*Apply rules to break down assumptions of the form |
836 Y \<in> parts(insert X H) and Y \<in> analz(insert X H) |
836 Y \<in> parts(insert X H) and Y \<in> analz(insert X H) |
837 *) |
837 *) |
838 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
838 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
839 |
839 |
840 val Fake_insert_tac = |
840 fun Fake_insert_tac ctxt = |
841 dresolve_tac [impOfSubs Fake_analz_insert, |
841 dresolve_tac ctxt [impOfSubs Fake_analz_insert, |
842 impOfSubs Fake_parts_insert] THEN' |
842 impOfSubs Fake_parts_insert] THEN' |
843 eresolve_tac [asm_rl, @{thm synth.Inj}]; |
843 eresolve_tac ctxt [asm_rl, @{thm synth.Inj}]; |
844 |
844 |
845 fun Fake_insert_simp_tac ctxt i = |
845 fun Fake_insert_simp_tac ctxt i = |
846 REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ctxt i; |
846 REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i; |
847 |
847 |
848 fun atomic_spy_analz_tac ctxt = |
848 fun atomic_spy_analz_tac ctxt = |
849 SELECT_GOAL |
849 SELECT_GOAL |
850 (Fake_insert_simp_tac ctxt 1 THEN |
850 (Fake_insert_simp_tac ctxt 1 THEN |
851 IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1)); |
851 IF_UNSOLVED (Blast.depth_tac (ctxt addIs [analz_insertI, impOfSubs analz_subset_parts]) 4 1)); |
857 [ (*push in occurrences of X...*) |
857 [ (*push in occurrences of X...*) |
858 (REPEAT o CHANGED) |
858 (REPEAT o CHANGED) |
859 (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
859 (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
860 (*...allowing further simplifications*) |
860 (*...allowing further simplifications*) |
861 simp_tac ctxt 1, |
861 simp_tac ctxt 1, |
862 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
862 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
863 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
863 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
864 *} |
864 *} |
865 |
865 |
866 text{*By default only @{text o_apply} is built-in. But in the presence of |
866 text{*By default only @{text o_apply} is built-in. But in the presence of |
867 eta-expansion this means that some terms displayed as @{term "f o g"} will be |
867 eta-expansion this means that some terms displayed as @{term "f o g"} will be |