equal
deleted
inserted
replaced
848 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
848 fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) |
849 |
849 |
850 (*Apply rules to break down assumptions of the form |
850 (*Apply rules to break down assumptions of the form |
851 Y \<in> parts(insert X H) and Y \<in> analz(insert X H) |
851 Y \<in> parts(insert X H) and Y \<in> analz(insert X H) |
852 *) |
852 *) |
853 val Fake_insert_tac = |
853 fun Fake_insert_tac ctxt = |
854 dresolve_tac [impOfSubs @{thm Fake_analz_insert}, |
854 dresolve_tac ctxt [impOfSubs @{thm Fake_analz_insert}, |
855 impOfSubs @{thm Fake_parts_insert}] THEN' |
855 impOfSubs @{thm Fake_parts_insert}] THEN' |
856 eresolve_tac [asm_rl, @{thm synth.Inj}]; |
856 eresolve_tac ctxt [asm_rl, @{thm synth.Inj}]; |
857 |
857 |
858 fun Fake_insert_simp_tac ctxt i = |
858 fun Fake_insert_simp_tac ctxt i = |
859 REPEAT (Fake_insert_tac i) THEN asm_full_simp_tac ctxt i; |
859 REPEAT (Fake_insert_tac ctxt i) THEN asm_full_simp_tac ctxt i; |
860 |
860 |
861 fun atomic_spy_analz_tac ctxt = |
861 fun atomic_spy_analz_tac ctxt = |
862 SELECT_GOAL |
862 SELECT_GOAL |
863 (Fake_insert_simp_tac ctxt 1 THEN |
863 (Fake_insert_simp_tac ctxt 1 THEN |
864 IF_UNSOLVED |
864 IF_UNSOLVED |
872 [ (*push in occurrences of X...*) |
872 [ (*push in occurrences of X...*) |
873 (REPEAT o CHANGED) |
873 (REPEAT o CHANGED) |
874 (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
874 (res_inst_tac ctxt [(("x", 1), "X")] (insert_commute RS ssubst) 1), |
875 (*...allowing further simplifications*) |
875 (*...allowing further simplifications*) |
876 simp_tac ctxt 1, |
876 simp_tac ctxt 1, |
877 REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), |
877 REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), |
878 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
878 DEPTH_SOLVE (atomic_spy_analz_tac ctxt 1)]) i); |
879 *} |
879 *} |
880 (*>*) |
880 (*>*) |
881 |
881 |
882 |
882 |